import MaxLeafFormal.RSCheck /-! # RS closed-form rate: cover 1, chunk 3 (generated) Generated by `scripts/export_rs_cover.py` (bisection as in `ancillary/rs_closed_form_interval.py`, SHA-256 `6ea21466e9a6f7153bafd754cbc8d0cdea78ef1c6f83ec9b25309d6aec87643e`). 500 intervals covering [109055/262144, 109187/262144] 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 `109055/262144`. -/ def cover3 : List ℚ := [ q 1090553 2621440, q 272639 655360, q 1090559 2621440, q 545281 1310720, q 218113 524288, q 136321 327680, q 1090571 2621440, q 545287 1310720, q 1090577 2621440, q 54529 131072, q 1090583 2621440, q 545293 1310720, q 1090589 2621440, q 34081 81920, q 218119 524288, q 545299 1310720, q 1090601 2621440, q 272651 655360, q 1090607 2621440, q 109061 262144, q 1090613 2621440, q 136327 327680, q 1090619 2621440, q 545311 1310720, q 218125 524288, q 272657 655360, q 1090631 2621440, q 545317 1310720, q 1090637 2621440, q 13633 32768, q 1090643 2621440, q 545323 1310720, q 1090649 2621440, q 272663 655360, q 218131 524288, q 545329 1310720, q 1090661 2621440, q 136333 327680, q 1090667 2621440, q 109067 262144, q 1090673 2621440, q 272669 655360, q 1090679 2621440, q 545341 1310720, q 218137 524288, q 8521 20480, q 1090691 2621440, q 545347 1310720, q 1090697 2621440, q 54535 131072, q 1090703 2621440, q 545353 1310720, q 1090709 2621440, q 136339 327680, q 218143 524288, q 545359 1310720, q 1090721 2621440, q 272681 655360, q 1090727 2621440, q 109073 262144, q 1090733 2621440, q 68171 163840, q 1090739 2621440, q 545371 1310720, q 218149 524288, q 272687 655360, q 1090751 2621440, q 545377 1310720, q 1090757 2621440, q 27269 65536, q 1090763 2621440, q 545383 1310720, q 1090769 2621440, q 272693 655360, q 218155 524288, q 545389 1310720, q 1090781 2621440, q 34087 81920, q 1090787 2621440, q 109079 262144, q 1090793 2621440, q 272699 655360, q 1090799 2621440, q 545401 1310720, q 218161 524288, q 136351 327680, q 1090811 2621440, q 545407 1310720, q 1090817 2621440, q 54541 131072, q 1090823 2621440, q 545413 1310720, q 1090829 2621440, q 68177 163840, q 218167 524288, q 545419 1310720, q 1090841 2621440, q 272711 655360, q 1090847 2621440, q 109085 262144, q 1090853 2621440, q 136357 327680, q 1090859 2621440, q 545431 1310720, q 218173 524288, q 272717 655360, q 1090871 2621440, q 545437 1310720, q 1090877 2621440, q 3409 8192, q 1090883 2621440, q 545443 1310720, q 1090889 2621440, q 272723 655360, q 218179 524288, q 545449 1310720, q 1090901 2621440, q 136363 327680, q 1090907 2621440, q 109091 262144, q 1090913 2621440, q 272729 655360, q 1090919 2621440, q 545461 1310720, q 218185 524288, q 68183 163840, q 1090931 2621440, q 545467 1310720, q 1090937 2621440, q 54547 131072, q 1090943 2621440, q 545473 1310720, q 1090949 2621440, q 136369 327680, q 218191 524288, q 545479 1310720, q 1090961 2621440, q 272741 655360, q 1090967 2621440, q 109097 262144, q 1090973 2621440, q 34093 81920, q 1090979 2621440, q 545491 1310720, q 218197 524288, q 272747 655360, q 1090991 2621440, q 545497 1310720, q 1090997 2621440, q 27275 65536, q 1091003 2621440, q 545503 1310720, q 1091009 2621440, q 272753 655360, q 218203 524288, q 545509 1310720, q 1091021 2621440, q 68189 163840, q 1091027 2621440, q 109103 262144, q 1091033 2621440, q 272759 655360, q 1091039 2621440, q 545521 1310720, q 218209 524288, q 136381 327680, q 1091051 2621440, q 545527 1310720, q 1091057 2621440, q 54553 131072, q 1091063 2621440, q 545533 1310720, q 1091069 2621440, q 2131 5120, q 218215 524288, q 545539 1310720, q 1091081 2621440, q 272771 655360, q 1091087 2621440, q 109109 262144, q 1091093 2621440, q 136387 327680, q 1091099 2621440, q 545551 1310720, q 218221 524288, q 272777 655360, q 1091111 2621440, q 545557 1310720, q 1091117 2621440, q 13639 32768, q 1091123 2621440, q 545563 1310720, q 1091129 2621440, q 272783 655360, q 218227 524288, q 545569 1310720, q 1091141 2621440, q 136393 327680, q 1091147 2621440, q 109115 262144, q 1091153 2621440, q 272789 655360, q 1091159 2621440, q 545581 1310720, q 218233 524288, q 34099 81920, q 1091171 2621440, q 545587 1310720, q 1091177 2621440, q 54559 131072, q 1091183 2621440, q 545593 1310720, q 1091189 2621440, q 136399 327680, q 218239 524288, q 545599 1310720, q 1091201 2621440, q 272801 655360, q 1091207 2621440, q 109121 262144, q 1091213 2621440, q 68201 163840, q 1091219 2621440, q 545611 1310720, q 218245 524288, q 272807 655360, q 1091231 2621440, q 545617 1310720, q 1091237 2621440, q 27281 65536, q 1091243 2621440, q 545623 1310720, q 1091249 2621440, q 272813 655360, q 218251 524288, q 545629 1310720, q 1091261 2621440, q 17051 40960, q 1091267 2621440, q 109127 262144, q 1091273 2621440, q 272819 655360, q 1091279 2621440, q 545641 1310720, q 218257 524288, q 136411 327680, q 1091291 2621440, q 545647 1310720, q 1091297 2621440, q 54565 131072, q 1091303 2621440, q 545653 1310720, q 1091309 2621440, q 68207 163840, q 218263 524288, q 545659 1310720, q 1091321 2621440, q 272831 655360, q 1091327 2621440, q 109133 262144, q 1091333 2621440, q 136417 327680, q 1091339 2621440, q 545671 1310720, q 218269 524288, q 272837 655360, q 1091351 2621440, q 545677 1310720, q 1091357 2621440, q 6821 16384, q 1091363 2621440, q 545683 1310720, q 1091369 2621440, q 272843 655360, q 218275 524288, q 545689 1310720, q 1091381 2621440, q 136423 327680, q 1091387 2621440, q 109139 262144, q 1091393 2621440, q 272849 655360, q 1091399 2621440, q 545701 1310720, q 218281 524288, q 68213 163840, q 1091411 2621440, q 545707 1310720, q 1091417 2621440, q 54571 131072, q 1091423 2621440, q 545713 1310720, q 1091429 2621440, q 136429 327680, q 218287 524288, q 545719 1310720, q 1091441 2621440, q 272861 655360, q 1091447 2621440, q 109145 262144, q 1091453 2621440, q 8527 20480, q 1091459 2621440, q 545731 1310720, q 218293 524288, q 272867 655360, q 1091471 2621440, q 545737 1310720, q 1091477 2621440, q 27287 65536, q 1091483 2621440, q 545743 1310720, q 1091489 2621440, q 272873 655360, q 218299 524288, q 545749 1310720, q 1091501 2621440, q 68219 163840, q 1091507 2621440, q 109151 262144, q 1091513 2621440, q 272879 655360, q 1091519 2621440, q 545761 1310720, q 218305 524288, q 136441 327680, q 1091531 2621440, q 545767 1310720, q 1091537 2621440, q 54577 131072, q 1091543 2621440, q 545773 1310720, q 1091549 2621440, q 34111 81920, q 218311 524288, q 545779 1310720, q 1091561 2621440, q 272891 655360, q 1091567 2621440, q 109157 262144, q 1091573 2621440, q 136447 327680, q 1091579 2621440, q 545791 1310720, q 218317 524288, q 272897 655360, q 1091591 2621440, q 545797 1310720, q 1091597 2621440, q 13645 32768, q 1091603 2621440, q 545803 1310720, q 1091609 2621440, q 272903 655360, q 218323 524288, q 545809 1310720, q 1091621 2621440, q 136453 327680, q 1091627 2621440, q 109163 262144, q 1091633 2621440, q 272909 655360, q 1091639 2621440, q 545821 1310720, q 218329 524288, q 17057 40960, q 1091651 2621440, q 545827 1310720, q 1091657 2621440, q 54583 131072, q 1091663 2621440, q 545833 1310720, q 1091669 2621440, q 136459 327680, q 218335 524288, q 545839 1310720, q 1091681 2621440, q 272921 655360, q 1091687 2621440, q 109169 262144, q 2183383 5242880, q 1091693 2621440, q 2183389 5242880, q 68231 163840, q 436679 1048576, q 1091699 2621440, q 2183401 5242880, q 545851 1310720, q 2183407 5242880, q 218341 524288, q 2183413 5242880, q 272927 655360, q 2183419 5242880, q 1091711 2621440, q 436685 1048576, q 545857 1310720, q 2183431 5242880, q 1091717 2621440, q 2183437 5242880, q 27293 65536, q 2183443 5242880, q 1091723 2621440, q 2183449 5242880, q 545863 1310720, q 436691 1048576, q 1091729 2621440, q 2183461 5242880, q 272933 655360, q 2183467 5242880, q 218347 524288, q 2183473 5242880, q 545869 1310720, q 2183479 5242880, q 1091741 2621440, q 436697 1048576, q 34117 81920, q 2183491 5242880, q 1091747 2621440, q 2183497 5242880, q 109175 262144, q 2183503 5242880, q 1091753 2621440, q 2183509 5242880, q 272939 655360, q 436703 1048576, q 1091759 2621440, q 2183521 5242880, q 545881 1310720, q 2183527 5242880, q 218353 524288, q 2183533 5242880, q 136471 327680, q 2183539 5242880, q 1091771 2621440, q 436709 1048576, q 545887 1310720, q 2183551 5242880, q 1091777 2621440, q 2183557 5242880, q 54589 131072, q 2183563 5242880, q 1091783 2621440, q 2183569 5242880, q 545893 1310720, q 436715 1048576, q 1091789 2621440, q 2183581 5242880, q 68237 163840, q 2183587 5242880, q 218359 524288, q 2183593 5242880, q 545899 1310720, q 2183599 5242880, q 1091801 2621440, q 436721 1048576, q 272951 655360, q 2183611 5242880, q 1091807 2621440, q 2183617 5242880, q 109181 262144, q 2183623 5242880, q 1091813 2621440, q 2183629 5242880, q 136477 327680, q 436727 1048576, q 1091819 2621440, q 2183641 5242880, q 545911 1310720, q 2183647 5242880, q 218365 524288, q 2183653 5242880, q 272957 655360, q 2183659 5242880, q 1091831 2621440, q 436733 1048576, q 545917 1310720, q 2183671 5242880, q 1091837 2621440, q 2183677 5242880, q 853 2048, q 2183683 5242880, q 1091843 2621440, q 2183689 5242880, q 545923 1310720, q 436739 1048576, q 1091849 2621440, q 2183701 5242880, q 272963 655360, q 2183707 5242880, q 218371 524288, q 2183713 5242880, q 545929 1310720, q 2183719 5242880, q 1091861 2621440, q 436745 1048576, q 136483 327680, q 2183731 5242880, q 1091867 2621440, q 2183737 5242880, q 109187 262144 ] theorem cover3_ok : checkCover (q 8030906143 10000000000) (q 109187 262144) (q 109055 262144) cover3 = true := by decide +kernel theorem cover3_sound : ∀ σ ∈ Set.Icc (((q 109055 262144) : ℚ) : ℝ) (((q 109187 262144) : ℚ) : ℝ), rsF σ ≤ (((q 8030906143 10000000000) : ℚ) : ℝ) := checkCover_sound cover3_ok end MaxLeafFormal.RSRate