MaxLeafFormal.RSCover16
Source file MaxLeafFormal/RSCover16.lean of the Lean project (how it is built).
import MaxLeafFormal.RSCheck
/-!
# RS closed-form rate: cover 1, chunk 16 (generated)
Generated by `scripts/export_rs_cover.py` (bisection as in
`ancillary/rs_closed_form_interval.py`,
SHA-256 `6ea21466e9a6f7153bafd754cbc8d0cdea78ef1c6f83ec9b25309d6aec87643e`).
500 intervals covering [1098617/2621440, 550369/1310720] 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 `1098617/2621440`. -/
def cover16 : List ℚ := [
q 54931 131072,
q 1098623 2621440,
q 549313 1310720,
q 1098629 2621440,
q 137329 327680,
q 219727 524288,
q 549319 1310720,
q 1098641 2621440,
q 274661 655360,
q 1098647 2621440,
q 109865 262144,
q 1098653 2621440,
q 34333 81920,
q 1098659 2621440,
q 549331 1310720,
q 219733 524288,
q 274667 655360,
q 1098671 2621440,
q 549337 1310720,
q 1098677 2621440,
q 27467 65536,
q 1098683 2621440,
q 549343 1310720,
q 1098689 2621440,
q 274673 655360,
q 219739 524288,
q 549349 1310720,
q 1098701 2621440,
q 68669 163840,
q 1098707 2621440,
q 109871 262144,
q 1098713 2621440,
q 274679 655360,
q 1098719 2621440,
q 549361 1310720,
q 219745 524288,
q 137341 327680,
q 1098731 2621440,
q 549367 1310720,
q 1098737 2621440,
q 54937 131072,
q 1098743 2621440,
q 549373 1310720,
q 1098749 2621440,
q 1073 2560,
q 219751 524288,
q 549379 1310720,
q 1098761 2621440,
q 274691 655360,
q 1098767 2621440,
q 109877 262144,
q 1098773 2621440,
q 137347 327680,
q 1098779 2621440,
q 549391 1310720,
q 219757 524288,
q 274697 655360,
q 1098791 2621440,
q 549397 1310720,
q 1098797 2621440,
q 13735 32768,
q 1098803 2621440,
q 549403 1310720,
q 1098809 2621440,
q 274703 655360,
q 219763 524288,
q 549409 1310720,
q 1098821 2621440,
q 137353 327680,
q 1098827 2621440,
q 109883 262144,
q 1098833 2621440,
q 274709 655360,
q 1098839 2621440,
q 549421 1310720,
q 219769 524288,
q 34339 81920,
q 1098851 2621440,
q 549427 1310720,
q 1098857 2621440,
q 54943 131072,
q 1098863 2621440,
q 549433 1310720,
q 1098869 2621440,
q 137359 327680,
q 219775 524288,
q 549439 1310720,
q 1098881 2621440,
q 274721 655360,
q 1098887 2621440,
q 109889 262144,
q 1098893 2621440,
q 68681 163840,
q 1098899 2621440,
q 549451 1310720,
q 219781 524288,
q 274727 655360,
q 1098911 2621440,
q 549457 1310720,
q 1098917 2621440,
q 27473 65536,
q 1098923 2621440,
q 549463 1310720,
q 1098929 2621440,
q 274733 655360,
q 219787 524288,
q 549469 1310720,
q 1098941 2621440,
q 17171 40960,
q 1098947 2621440,
q 109895 262144,
q 1098953 2621440,
q 274739 655360,
q 1098959 2621440,
q 549481 1310720,
q 219793 524288,
q 137371 327680,
q 1098971 2621440,
q 549487 1310720,
q 1098977 2621440,
q 54949 131072,
q 1098983 2621440,
q 549493 1310720,
q 1098989 2621440,
q 68687 163840,
q 219799 524288,
q 549499 1310720,
q 1099001 2621440,
q 274751 655360,
q 1099007 2621440,
q 109901 262144,
q 1099013 2621440,
q 137377 327680,
q 1099019 2621440,
q 549511 1310720,
q 219805 524288,
q 274757 655360,
q 1099031 2621440,
q 549517 1310720,
q 1099037 2621440,
q 6869 16384,
q 1099043 2621440,
q 549523 1310720,
q 1099049 2621440,
q 274763 655360,
q 219811 524288,
q 549529 1310720,
q 1099061 2621440,
q 137383 327680,
q 1099067 2621440,
q 109907 262144,
q 1099073 2621440,
q 274769 655360,
q 1099079 2621440,
q 549541 1310720,
q 219817 524288,
q 68693 163840,
q 1099091 2621440,
q 549547 1310720,
q 1099097 2621440,
q 54955 131072,
q 1099103 2621440,
q 549553 1310720,
q 1099109 2621440,
q 137389 327680,
q 219823 524288,
q 549559 1310720,
q 1099121 2621440,
q 274781 655360,
q 1099127 2621440,
q 109913 262144,
q 1099133 2621440,
q 8587 20480,
q 1099139 2621440,
q 549571 1310720,
q 219829 524288,
q 274787 655360,
q 1099151 2621440,
q 549577 1310720,
q 1099157 2621440,
q 27479 65536,
q 1099163 2621440,
q 549583 1310720,
q 1099169 2621440,
q 274793 655360,
q 219835 524288,
q 549589 1310720,
q 1099181 2621440,
q 68699 163840,
q 1099187 2621440,
q 109919 262144,
q 1099193 2621440,
q 274799 655360,
q 1099199 2621440,
q 549601 1310720,
q 219841 524288,
q 137401 327680,
q 1099211 2621440,
q 549607 1310720,
q 1099217 2621440,
q 54961 131072,
q 1099223 2621440,
q 549613 1310720,
q 1099229 2621440,
q 34351 81920,
q 219847 524288,
q 549619 1310720,
q 1099241 2621440,
q 274811 655360,
q 1099247 2621440,
q 109925 262144,
q 1099253 2621440,
q 137407 327680,
q 1099259 2621440,
q 549631 1310720,
q 219853 524288,
q 274817 655360,
q 1099271 2621440,
q 549637 1310720,
q 1099277 2621440,
q 13741 32768,
q 1099283 2621440,
q 549643 1310720,
q 1099289 2621440,
q 274823 655360,
q 219859 524288,
q 549649 1310720,
q 1099301 2621440,
q 137413 327680,
q 1099307 2621440,
q 109931 262144,
q 1099313 2621440,
q 274829 655360,
q 1099319 2621440,
q 549661 1310720,
q 219865 524288,
q 17177 40960,
q 1099331 2621440,
q 549667 1310720,
q 1099337 2621440,
q 54967 131072,
q 1099343 2621440,
q 549673 1310720,
q 1099349 2621440,
q 137419 327680,
q 219871 524288,
q 549679 1310720,
q 1099361 2621440,
q 274841 655360,
q 1099367 2621440,
q 109937 262144,
q 1099373 2621440,
q 68711 163840,
q 1099379 2621440,
q 549691 1310720,
q 219877 524288,
q 274847 655360,
q 1099391 2621440,
q 549697 1310720,
q 1099397 2621440,
q 27485 65536,
q 1099403 2621440,
q 549703 1310720,
q 1099409 2621440,
q 274853 655360,
q 219883 524288,
q 549709 1310720,
q 1099421 2621440,
q 34357 81920,
q 1099427 2621440,
q 109943 262144,
q 1099433 2621440,
q 274859 655360,
q 1099439 2621440,
q 549721 1310720,
q 219889 524288,
q 137431 327680,
q 1099451 2621440,
q 549727 1310720,
q 1099457 2621440,
q 54973 131072,
q 1099463 2621440,
q 549733 1310720,
q 1099469 2621440,
q 68717 163840,
q 219895 524288,
q 549739 1310720,
q 1099481 2621440,
q 274871 655360,
q 1099487 2621440,
q 109949 262144,
q 1099493 2621440,
q 137437 327680,
q 549751 1310720,
q 274877 655360,
q 549757 1310720,
q 859 2048,
q 549763 1310720,
q 274883 655360,
q 549769 1310720,
q 137443 327680,
q 109955 262144,
q 274889 655360,
q 549781 1310720,
q 68723 163840,
q 549787 1310720,
q 54979 131072,
q 549793 1310720,
q 137449 327680,
q 549799 1310720,
q 274901 655360,
q 109961 262144,
q 34363 81920,
q 549811 1310720,
q 274907 655360,
q 549817 1310720,
q 27491 65536,
q 549823 1310720,
q 274913 655360,
q 549829 1310720,
q 68729 163840,
q 109967 262144,
q 274919 655360,
q 549841 1310720,
q 137461 327680,
q 549847 1310720,
q 54985 131072,
q 549853 1310720,
q 17183 40960,
q 549859 1310720,
q 274931 655360,
q 109973 262144,
q 137467 327680,
q 549871 1310720,
q 274937 655360,
q 549877 1310720,
q 13747 32768,
q 549883 1310720,
q 274943 655360,
q 549889 1310720,
q 137473 327680,
q 109979 262144,
q 274949 655360,
q 549901 1310720,
q 34369 81920,
q 549907 1310720,
q 54991 131072,
q 549913 1310720,
q 137479 327680,
q 549919 1310720,
q 274961 655360,
q 109985 262144,
q 68741 163840,
q 549931 1310720,
q 274967 655360,
q 549937 1310720,
q 27497 65536,
q 549943 1310720,
q 274973 655360,
q 549949 1310720,
q 8593 20480,
q 109991 262144,
q 274979 655360,
q 549961 1310720,
q 137491 327680,
q 549967 1310720,
q 54997 131072,
q 549973 1310720,
q 68747 163840,
q 549979 1310720,
q 274991 655360,
q 109997 262144,
q 137497 327680,
q 549991 1310720,
q 274997 655360,
q 549997 1310720,
q 6875 16384,
q 550003 1310720,
q 275003 655360,
q 550009 1310720,
q 137503 327680,
q 110003 262144,
q 275009 655360,
q 550021 1310720,
q 68753 163840,
q 550027 1310720,
q 55003 131072,
q 550033 1310720,
q 137509 327680,
q 550039 1310720,
q 275021 655360,
q 110009 262144,
q 17189 40960,
q 550051 1310720,
q 275027 655360,
q 550057 1310720,
q 27503 65536,
q 550063 1310720,
q 275033 655360,
q 550069 1310720,
q 68759 163840,
q 110015 262144,
q 275039 655360,
q 550081 1310720,
q 137521 327680,
q 550087 1310720,
q 55009 131072,
q 550093 1310720,
q 34381 81920,
q 550099 1310720,
q 275051 655360,
q 110021 262144,
q 137527 327680,
q 550111 1310720,
q 275057 655360,
q 550117 1310720,
q 13753 32768,
q 550123 1310720,
q 275063 655360,
q 550129 1310720,
q 137533 327680,
q 110027 262144,
q 275069 655360,
q 550141 1310720,
q 2149 5120,
q 550147 1310720,
q 55015 131072,
q 550153 1310720,
q 137539 327680,
q 550159 1310720,
q 275081 655360,
q 110033 262144,
q 68771 163840,
q 550171 1310720,
q 275087 655360,
q 550177 1310720,
q 27509 65536,
q 550183 1310720,
q 275093 655360,
q 550189 1310720,
q 34387 81920,
q 110039 262144,
q 275099 655360,
q 550201 1310720,
q 137551 327680,
q 550207 1310720,
q 55021 131072,
q 550213 1310720,
q 68777 163840,
q 550219 1310720,
q 275111 655360,
q 110045 262144,
q 137557 327680,
q 550231 1310720,
q 275117 655360,
q 550237 1310720,
q 3439 8192,
q 550243 1310720,
q 275123 655360,
q 550249 1310720,
q 137563 327680,
q 110051 262144,
q 275129 655360,
q 550261 1310720,
q 68783 163840,
q 550267 1310720,
q 55027 131072,
q 550273 1310720,
q 137569 327680,
q 550279 1310720,
q 275141 655360,
q 110057 262144,
q 34393 81920,
q 550291 1310720,
q 275147 655360,
q 550297 1310720,
q 27515 65536,
q 550303 1310720,
q 275153 655360,
q 550309 1310720,
q 68789 163840,
q 110063 262144,
q 275159 655360,
q 550321 1310720,
q 137581 327680,
q 550327 1310720,
q 55033 131072,
q 550333 1310720,
q 8599 20480,
q 550339 1310720,
q 275171 655360,
q 110069 262144,
q 137587 327680,
q 550351 1310720,
q 275177 655360,
q 550357 1310720,
q 13759 32768,
q 550363 1310720,
q 275183 655360,
q 550369 1310720
]
theorem cover16_ok :
checkCover (q 8030906143 10000000000) (q 550369 1310720) (q 1098617 2621440) cover16 = true := by
decide +kernel
theorem cover16_sound : ∀ σ ∈ Set.Icc (((q 1098617 2621440) : ℚ) : ℝ) (((q 550369 1310720) : ℚ) : ℝ),
rsF σ ≤ (((q 8030906143 10000000000) : ℚ) : ℝ) :=
checkCover_sound cover16_ok
end MaxLeafFormal.RSRate