MaxLeafFormal.RSCover4
Source file MaxLeafFormal/RSCover4.lean of the Lean project (how it is built).
import MaxLeafFormal.RSCheck
/-!
# RS closed-form rate: cover 1, chunk 4 (generated)
Generated by `scripts/export_rs_cover.py` (bisection as in
`ancillary/rs_closed_form_interval.py`,
SHA-256 `6ea21466e9a6f7153bafd754cbc8d0cdea78ef1c6f83ec9b25309d6aec87643e`).
500 intervals covering [109187/262144, 54631/131072] for the target 8030906143/10000000000.
Do not edit by hand. The data are not trusted: `decide +kernel` re-checks every interval.
-/
set_option maxRecDepth 100000
namespace MaxLeafFormal.RSRate
/-- The right ends of the intervals, starting from `109187/262144`. -/
def cover4 : List ℚ := [
q 2183743 5242880,
q 1091873 2621440,
q 2183749 5242880,
q 272969 655360,
q 436751 1048576,
q 1091879 2621440,
q 2183761 5242880,
q 545941 1310720,
q 2183767 5242880,
q 218377 524288,
q 2183773 5242880,
q 68243 163840,
q 2183779 5242880,
q 1091891 2621440,
q 436757 1048576,
q 545947 1310720,
q 2183791 5242880,
q 1091897 2621440,
q 2183797 5242880,
q 54595 131072,
q 2183803 5242880,
q 1091903 2621440,
q 2183809 5242880,
q 545953 1310720,
q 436763 1048576,
q 1091909 2621440,
q 2183821 5242880,
q 136489 327680,
q 2183827 5242880,
q 218383 524288,
q 2183833 5242880,
q 545959 1310720,
q 2183839 5242880,
q 1091921 2621440,
q 436769 1048576,
q 272981 655360,
q 2183851 5242880,
q 1091927 2621440,
q 2183857 5242880,
q 109193 262144,
q 2183863 5242880,
q 1091933 2621440,
q 2183869 5242880,
q 34123 81920,
q 436775 1048576,
q 1091939 2621440,
q 2183881 5242880,
q 545971 1310720,
q 2183887 5242880,
q 218389 524288,
q 2183893 5242880,
q 272987 655360,
q 2183899 5242880,
q 1091951 2621440,
q 436781 1048576,
q 545977 1310720,
q 2183911 5242880,
q 1091957 2621440,
q 2183917 5242880,
q 27299 65536,
q 2183923 5242880,
q 1091963 2621440,
q 2183929 5242880,
q 545983 1310720,
q 436787 1048576,
q 1091969 2621440,
q 2183941 5242880,
q 272993 655360,
q 2183947 5242880,
q 218395 524288,
q 2183953 5242880,
q 545989 1310720,
q 2183959 5242880,
q 1091981 2621440,
q 436793 1048576,
q 68249 163840,
q 2183971 5242880,
q 1091987 2621440,
q 2183977 5242880,
q 109199 262144,
q 2183983 5242880,
q 1091993 2621440,
q 2183989 5242880,
q 272999 655360,
q 436799 1048576,
q 1091999 2621440,
q 2184001 5242880,
q 546001 1310720,
q 2184007 5242880,
q 218401 524288,
q 2184013 5242880,
q 136501 327680,
q 2184019 5242880,
q 1092011 2621440,
q 436805 1048576,
q 546007 1310720,
q 2184031 5242880,
q 1092017 2621440,
q 2184037 5242880,
q 54601 131072,
q 2184043 5242880,
q 1092023 2621440,
q 2184049 5242880,
q 546013 1310720,
q 436811 1048576,
q 1092029 2621440,
q 2184061 5242880,
q 17063 40960,
q 2184067 5242880,
q 218407 524288,
q 2184073 5242880,
q 546019 1310720,
q 2184079 5242880,
q 1092041 2621440,
q 436817 1048576,
q 273011 655360,
q 2184091 5242880,
q 1092047 2621440,
q 2184097 5242880,
q 109205 262144,
q 2184103 5242880,
q 1092053 2621440,
q 2184109 5242880,
q 136507 327680,
q 436823 1048576,
q 1092059 2621440,
q 2184121 5242880,
q 546031 1310720,
q 2184127 5242880,
q 218413 524288,
q 2184133 5242880,
q 273017 655360,
q 2184139 5242880,
q 1092071 2621440,
q 436829 1048576,
q 546037 1310720,
q 2184151 5242880,
q 1092077 2621440,
q 2184157 5242880,
q 13651 32768,
q 2184163 5242880,
q 1092083 2621440,
q 2184169 5242880,
q 546043 1310720,
q 436835 1048576,
q 1092089 2621440,
q 2184181 5242880,
q 273023 655360,
q 2184187 5242880,
q 218419 524288,
q 2184193 5242880,
q 546049 1310720,
q 2184199 5242880,
q 1092101 2621440,
q 436841 1048576,
q 136513 327680,
q 2184211 5242880,
q 1092107 2621440,
q 2184217 5242880,
q 109211 262144,
q 2184223 5242880,
q 1092113 2621440,
q 2184229 5242880,
q 273029 655360,
q 436847 1048576,
q 1092119 2621440,
q 2184241 5242880,
q 546061 1310720,
q 2184247 5242880,
q 218425 524288,
q 2184253 5242880,
q 34129 81920,
q 2184259 5242880,
q 1092131 2621440,
q 436853 1048576,
q 546067 1310720,
q 2184271 5242880,
q 1092137 2621440,
q 2184277 5242880,
q 54607 131072,
q 2184283 5242880,
q 1092143 2621440,
q 2184289 5242880,
q 546073 1310720,
q 436859 1048576,
q 1092149 2621440,
q 2184301 5242880,
q 136519 327680,
q 2184307 5242880,
q 218431 524288,
q 2184313 5242880,
q 546079 1310720,
q 2184319 5242880,
q 1092161 2621440,
q 436865 1048576,
q 273041 655360,
q 2184331 5242880,
q 1092167 2621440,
q 2184337 5242880,
q 109217 262144,
q 2184343 5242880,
q 1092173 2621440,
q 2184349 5242880,
q 68261 163840,
q 436871 1048576,
q 1092179 2621440,
q 2184361 5242880,
q 546091 1310720,
q 2184367 5242880,
q 218437 524288,
q 2184373 5242880,
q 273047 655360,
q 2184379 5242880,
q 1092191 2621440,
q 436877 1048576,
q 546097 1310720,
q 2184391 5242880,
q 1092197 2621440,
q 2184397 5242880,
q 27305 65536,
q 2184403 5242880,
q 1092203 2621440,
q 2184409 5242880,
q 546103 1310720,
q 436883 1048576,
q 1092209 2621440,
q 2184421 5242880,
q 273053 655360,
q 2184427 5242880,
q 218443 524288,
q 2184433 5242880,
q 546109 1310720,
q 2184439 5242880,
q 1092221 2621440,
q 436889 1048576,
q 8533 20480,
q 2184451 5242880,
q 1092227 2621440,
q 2184457 5242880,
q 109223 262144,
q 2184463 5242880,
q 1092233 2621440,
q 2184469 5242880,
q 273059 655360,
q 436895 1048576,
q 1092239 2621440,
q 2184481 5242880,
q 546121 1310720,
q 2184487 5242880,
q 218449 524288,
q 2184493 5242880,
q 136531 327680,
q 2184499 5242880,
q 1092251 2621440,
q 436901 1048576,
q 546127 1310720,
q 2184511 5242880,
q 1092257 2621440,
q 2184517 5242880,
q 54613 131072,
q 2184523 5242880,
q 1092263 2621440,
q 2184529 5242880,
q 546133 1310720,
q 436907 1048576,
q 1092269 2621440,
q 2184541 5242880,
q 68267 163840,
q 2184547 5242880,
q 218455 524288,
q 2184553 5242880,
q 546139 1310720,
q 2184559 5242880,
q 1092281 2621440,
q 436913 1048576,
q 273071 655360,
q 2184571 5242880,
q 1092287 2621440,
q 2184577 5242880,
q 109229 262144,
q 2184583 5242880,
q 1092293 2621440,
q 2184589 5242880,
q 136537 327680,
q 436919 1048576,
q 1092299 2621440,
q 2184601 5242880,
q 546151 1310720,
q 2184607 5242880,
q 218461 524288,
q 2184613 5242880,
q 273077 655360,
q 2184619 5242880,
q 1092311 2621440,
q 436925 1048576,
q 546157 1310720,
q 2184631 5242880,
q 1092317 2621440,
q 2184637 5242880,
q 6827 16384,
q 2184643 5242880,
q 1092323 2621440,
q 2184649 5242880,
q 546163 1310720,
q 436931 1048576,
q 1092329 2621440,
q 2184661 5242880,
q 273083 655360,
q 2184667 5242880,
q 218467 524288,
q 2184673 5242880,
q 546169 1310720,
q 2184679 5242880,
q 1092341 2621440,
q 436937 1048576,
q 136543 327680,
q 2184691 5242880,
q 1092347 2621440,
q 2184697 5242880,
q 109235 262144,
q 2184703 5242880,
q 1092353 2621440,
q 2184709 5242880,
q 273089 655360,
q 436943 1048576,
q 1092359 2621440,
q 2184721 5242880,
q 546181 1310720,
q 2184727 5242880,
q 218473 524288,
q 2184733 5242880,
q 68273 163840,
q 2184739 5242880,
q 1092371 2621440,
q 436949 1048576,
q 546187 1310720,
q 2184751 5242880,
q 1092377 2621440,
q 2184757 5242880,
q 54619 131072,
q 2184763 5242880,
q 1092383 2621440,
q 2184769 5242880,
q 546193 1310720,
q 436955 1048576,
q 1092389 2621440,
q 2184781 5242880,
q 136549 327680,
q 2184787 5242880,
q 218479 524288,
q 2184793 5242880,
q 546199 1310720,
q 2184799 5242880,
q 1092401 2621440,
q 436961 1048576,
q 273101 655360,
q 2184811 5242880,
q 1092407 2621440,
q 2184817 5242880,
q 109241 262144,
q 2184823 5242880,
q 1092413 2621440,
q 2184829 5242880,
q 17069 40960,
q 436967 1048576,
q 1092419 2621440,
q 2184841 5242880,
q 546211 1310720,
q 2184847 5242880,
q 218485 524288,
q 2184853 5242880,
q 273107 655360,
q 2184859 5242880,
q 1092431 2621440,
q 436973 1048576,
q 546217 1310720,
q 2184871 5242880,
q 1092437 2621440,
q 2184877 5242880,
q 27311 65536,
q 2184883 5242880,
q 1092443 2621440,
q 2184889 5242880,
q 546223 1310720,
q 436979 1048576,
q 1092449 2621440,
q 2184901 5242880,
q 273113 655360,
q 2184907 5242880,
q 218491 524288,
q 2184913 5242880,
q 546229 1310720,
q 2184919 5242880,
q 1092461 2621440,
q 436985 1048576,
q 68279 163840,
q 2184931 5242880,
q 1092467 2621440,
q 2184937 5242880,
q 109247 262144,
q 2184943 5242880,
q 1092473 2621440,
q 2184949 5242880,
q 273119 655360,
q 436991 1048576,
q 1092479 2621440,
q 2184961 5242880,
q 546241 1310720,
q 2184967 5242880,
q 218497 524288,
q 2184973 5242880,
q 136561 327680,
q 2184979 5242880,
q 1092491 2621440,
q 436997 1048576,
q 546247 1310720,
q 2184991 5242880,
q 1092497 2621440,
q 2184997 5242880,
q 54625 131072,
q 2185003 5242880,
q 1092503 2621440,
q 2185009 5242880,
q 546253 1310720,
q 437003 1048576,
q 1092509 2621440,
q 2185021 5242880,
q 34141 81920,
q 2185027 5242880,
q 218503 524288,
q 2185033 5242880,
q 546259 1310720,
q 2185039 5242880,
q 1092521 2621440,
q 437009 1048576,
q 273131 655360,
q 2185051 5242880,
q 1092527 2621440,
q 2185057 5242880,
q 109253 262144,
q 2185063 5242880,
q 1092533 2621440,
q 2185069 5242880,
q 136567 327680,
q 437015 1048576,
q 1092539 2621440,
q 2185081 5242880,
q 546271 1310720,
q 2185087 5242880,
q 218509 524288,
q 2185093 5242880,
q 273137 655360,
q 2185099 5242880,
q 1092551 2621440,
q 437021 1048576,
q 546277 1310720,
q 2185111 5242880,
q 1092557 2621440,
q 2185117 5242880,
q 13657 32768,
q 2185123 5242880,
q 1092563 2621440,
q 2185129 5242880,
q 546283 1310720,
q 437027 1048576,
q 1092569 2621440,
q 2185141 5242880,
q 273143 655360,
q 2185147 5242880,
q 218515 524288,
q 2185153 5242880,
q 546289 1310720,
q 2185159 5242880,
q 1092581 2621440,
q 437033 1048576,
q 136573 327680,
q 2185171 5242880,
q 1092587 2621440,
q 2185177 5242880,
q 109259 262144,
q 2185183 5242880,
q 1092593 2621440,
q 2185189 5242880,
q 273149 655360,
q 437039 1048576,
q 1092599 2621440,
q 2185201 5242880,
q 546301 1310720,
q 2185207 5242880,
q 218521 524288,
q 2185213 5242880,
q 1067 2560,
q 2185219 5242880,
q 1092611 2621440,
q 437045 1048576,
q 546307 1310720,
q 2185231 5242880,
q 1092617 2621440,
q 2185237 5242880,
q 54631 131072
]
theorem cover4_ok :
checkCover (q 8030906143 10000000000) (q 54631 131072) (q 109187 262144) cover4 = true := by
decide +kernel
theorem cover4_sound : ∀ σ ∈ Set.Icc (((q 109187 262144) : ℚ) : ℝ) (((q 54631 131072) : ℚ) : ℝ),
rsF σ ≤ (((q 8030906143 10000000000) : ℚ) : ℝ) :=
checkCover_sound cover4_ok
end MaxLeafFormal.RSRate