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