import MaxLeafFormal.RSCheck /-! # RS closed-form rate: cover 1, chunk 15 (generated) Generated by `scripts/export_rs_cover.py` (bisection as in `ancillary/rs_closed_form_interval.py`, SHA-256 `6ea21466e9a6f7153bafd754cbc8d0cdea78ef1c6f83ec9b25309d6aec87643e`). 500 intervals covering [2194789/5242880, 1098617/2621440] 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 `2194789/5242880`. -/ def cover15 : List ℚ := [ q 274349 655360, q 438959 1048576, q 1097399 2621440, q 2194801 5242880, q 548701 1310720, q 2194807 5242880, q 219481 524288, q 2194813 5242880, q 17147 40960, q 2194819 5242880, q 1097411 2621440, q 438965 1048576, q 548707 1310720, q 2194831 5242880, q 1097417 2621440, q 2194837 5242880, q 54871 131072, q 2194843 5242880, q 1097423 2621440, q 2194849 5242880, q 548713 1310720, q 438971 1048576, q 1097429 2621440, q 2194861 5242880, q 137179 327680, q 2194867 5242880, q 219487 524288, q 2194873 5242880, q 548719 1310720, q 2194879 5242880, q 1097441 2621440, q 438977 1048576, q 274361 655360, q 2194891 5242880, q 1097447 2621440, q 2194897 5242880, q 109745 262144, q 2194903 5242880, q 1097453 2621440, q 2194909 5242880, q 68591 163840, q 438983 1048576, q 1097459 2621440, q 2194921 5242880, q 548731 1310720, q 2194927 5242880, q 219493 524288, q 2194933 5242880, q 274367 655360, q 2194939 5242880, q 1097471 2621440, q 438989 1048576, q 548737 1310720, q 2194951 5242880, q 1097477 2621440, q 2194957 5242880, q 27437 65536, q 2194963 5242880, q 1097483 2621440, q 2194969 5242880, q 548743 1310720, q 438995 1048576, q 1097489 2621440, q 2194981 5242880, q 274373 655360, q 2194987 5242880, q 219499 524288, q 2194993 5242880, q 548749 1310720, q 2194999 5242880, q 1097501 2621440, q 439001 1048576, q 34297 81920, q 2195011 5242880, q 1097507 2621440, q 2195017 5242880, q 109751 262144, q 2195023 5242880, q 1097513 2621440, q 2195029 5242880, q 274379 655360, q 439007 1048576, q 1097519 2621440, q 2195041 5242880, q 548761 1310720, q 2195047 5242880, q 219505 524288, q 2195053 5242880, q 137191 327680, q 2195059 5242880, q 1097531 2621440, q 439013 1048576, q 548767 1310720, q 2195071 5242880, q 1097537 2621440, q 2195077 5242880, q 54877 131072, q 2195083 5242880, q 1097543 2621440, q 2195089 5242880, q 548773 1310720, q 439019 1048576, q 1097549 2621440, q 2195101 5242880, q 68597 163840, q 2195107 5242880, q 219511 524288, q 2195113 5242880, q 548779 1310720, q 2195119 5242880, q 1097561 2621440, q 439025 1048576, q 274391 655360, q 2195131 5242880, q 1097567 2621440, q 2195137 5242880, q 109757 262144, q 2195143 5242880, q 1097573 2621440, q 2195149 5242880, q 137197 327680, q 439031 1048576, q 1097579 2621440, q 2195161 5242880, q 548791 1310720, q 2195167 5242880, q 219517 524288, q 2195173 5242880, q 274397 655360, q 2195179 5242880, q 1097591 2621440, q 439037 1048576, q 548797 1310720, q 2195191 5242880, q 1097597 2621440, q 2195197 5242880, q 1715 4096, q 2195203 5242880, q 1097603 2621440, q 2195209 5242880, q 548803 1310720, q 439043 1048576, q 1097609 2621440, q 2195221 5242880, q 274403 655360, q 2195227 5242880, q 219523 524288, q 2195233 5242880, q 548809 1310720, q 2195239 5242880, q 1097621 2621440, q 439049 1048576, q 137203 327680, q 2195251 5242880, q 1097627 2621440, q 2195257 5242880, q 109763 262144, q 2195263 5242880, q 1097633 2621440, q 2195269 5242880, q 274409 655360, q 439055 1048576, q 1097639 2621440, q 2195281 5242880, q 548821 1310720, q 2195287 5242880, q 219529 524288, q 2195293 5242880, q 68603 163840, q 2195299 5242880, q 1097651 2621440, q 439061 1048576, q 548827 1310720, q 2195311 5242880, q 1097657 2621440, q 2195317 5242880, q 54883 131072, q 2195323 5242880, q 1097663 2621440, q 2195329 5242880, q 548833 1310720, q 439067 1048576, q 1097669 2621440, q 2195341 5242880, q 137209 327680, q 219535 524288, q 548839 1310720, q 1097681 2621440, q 274421 655360, q 1097687 2621440, q 109769 262144, q 1097693 2621440, q 34303 81920, q 1097699 2621440, q 548851 1310720, q 219541 524288, q 274427 655360, q 1097711 2621440, q 548857 1310720, q 1097717 2621440, q 27443 65536, q 1097723 2621440, q 548863 1310720, q 1097729 2621440, q 274433 655360, q 219547 524288, q 548869 1310720, q 1097741 2621440, q 68609 163840, q 1097747 2621440, q 109775 262144, q 1097753 2621440, q 274439 655360, q 1097759 2621440, q 548881 1310720, q 219553 524288, q 137221 327680, q 1097771 2621440, q 548887 1310720, q 1097777 2621440, q 54889 131072, q 1097783 2621440, q 548893 1310720, q 1097789 2621440, q 17153 40960, q 219559 524288, q 548899 1310720, q 1097801 2621440, q 274451 655360, q 1097807 2621440, q 109781 262144, q 1097813 2621440, q 137227 327680, q 1097819 2621440, q 548911 1310720, q 219565 524288, q 274457 655360, q 1097831 2621440, q 548917 1310720, q 1097837 2621440, q 13723 32768, q 1097843 2621440, q 548923 1310720, q 1097849 2621440, q 274463 655360, q 219571 524288, q 548929 1310720, q 1097861 2621440, q 137233 327680, q 1097867 2621440, q 109787 262144, q 1097873 2621440, q 274469 655360, q 1097879 2621440, q 548941 1310720, q 219577 524288, q 34309 81920, q 1097891 2621440, q 548947 1310720, q 1097897 2621440, q 54895 131072, q 1097903 2621440, q 548953 1310720, q 1097909 2621440, q 137239 327680, q 219583 524288, q 548959 1310720, q 1097921 2621440, q 274481 655360, q 1097927 2621440, q 109793 262144, q 1097933 2621440, q 68621 163840, q 1097939 2621440, q 548971 1310720, q 219589 524288, q 274487 655360, q 1097951 2621440, q 548977 1310720, q 1097957 2621440, q 27449 65536, q 1097963 2621440, q 548983 1310720, q 1097969 2621440, q 274493 655360, q 219595 524288, q 548989 1310720, q 1097981 2621440, q 4289 10240, q 1097987 2621440, q 109799 262144, q 1097993 2621440, q 274499 655360, q 1097999 2621440, q 549001 1310720, q 219601 524288, q 137251 327680, q 1098011 2621440, q 549007 1310720, q 1098017 2621440, q 54901 131072, q 1098023 2621440, q 549013 1310720, q 1098029 2621440, q 68627 163840, q 219607 524288, q 549019 1310720, q 1098041 2621440, q 274511 655360, q 1098047 2621440, q 109805 262144, q 1098053 2621440, q 137257 327680, q 1098059 2621440, q 549031 1310720, q 219613 524288, q 274517 655360, q 1098071 2621440, q 549037 1310720, q 1098077 2621440, q 6863 16384, q 1098083 2621440, q 549043 1310720, q 1098089 2621440, q 274523 655360, q 219619 524288, q 549049 1310720, q 1098101 2621440, q 137263 327680, q 1098107 2621440, q 109811 262144, q 1098113 2621440, q 274529 655360, q 1098119 2621440, q 549061 1310720, q 219625 524288, q 68633 163840, q 1098131 2621440, q 549067 1310720, q 1098137 2621440, q 54907 131072, q 1098143 2621440, q 549073 1310720, q 1098149 2621440, q 137269 327680, q 219631 524288, q 549079 1310720, q 1098161 2621440, q 274541 655360, q 1098167 2621440, q 109817 262144, q 1098173 2621440, q 17159 40960, q 1098179 2621440, q 549091 1310720, q 219637 524288, q 274547 655360, q 1098191 2621440, q 549097 1310720, q 1098197 2621440, q 27455 65536, q 1098203 2621440, q 549103 1310720, q 1098209 2621440, q 274553 655360, q 219643 524288, q 549109 1310720, q 1098221 2621440, q 68639 163840, q 1098227 2621440, q 109823 262144, q 1098233 2621440, q 274559 655360, q 1098239 2621440, q 549121 1310720, q 219649 524288, q 137281 327680, q 1098251 2621440, q 549127 1310720, q 1098257 2621440, q 54913 131072, q 1098263 2621440, q 549133 1310720, q 1098269 2621440, q 34321 81920, q 219655 524288, q 549139 1310720, q 1098281 2621440, q 274571 655360, q 1098287 2621440, q 109829 262144, q 1098293 2621440, q 137287 327680, q 1098299 2621440, q 549151 1310720, q 219661 524288, q 274577 655360, q 1098311 2621440, q 549157 1310720, q 1098317 2621440, q 13729 32768, q 1098323 2621440, q 549163 1310720, q 1098329 2621440, q 274583 655360, q 219667 524288, q 549169 1310720, q 1098341 2621440, q 137293 327680, q 1098347 2621440, q 109835 262144, q 1098353 2621440, q 274589 655360, q 1098359 2621440, q 549181 1310720, q 219673 524288, q 8581 20480, q 1098371 2621440, q 549187 1310720, q 1098377 2621440, q 54919 131072, q 1098383 2621440, q 549193 1310720, q 1098389 2621440, q 137299 327680, q 219679 524288, q 549199 1310720, q 1098401 2621440, q 274601 655360, q 1098407 2621440, q 109841 262144, q 1098413 2621440, q 68651 163840, q 1098419 2621440, q 549211 1310720, q 219685 524288, q 274607 655360, q 1098431 2621440, q 549217 1310720, q 1098437 2621440, q 27461 65536, q 1098443 2621440, q 549223 1310720, q 1098449 2621440, q 274613 655360, q 219691 524288, q 549229 1310720, q 1098461 2621440, q 34327 81920, q 1098467 2621440, q 109847 262144, q 1098473 2621440, q 274619 655360, q 1098479 2621440, q 549241 1310720, q 219697 524288, q 137311 327680, q 1098491 2621440, q 549247 1310720, q 1098497 2621440, q 54925 131072, q 1098503 2621440, q 549253 1310720, q 1098509 2621440, q 68657 163840, q 219703 524288, q 549259 1310720, q 1098521 2621440, q 274631 655360, q 1098527 2621440, q 109853 262144, q 1098533 2621440, q 137317 327680, q 1098539 2621440, q 549271 1310720, q 219709 524288, q 274637 655360, q 1098551 2621440, q 549277 1310720, q 1098557 2621440, q 3433 8192, q 1098563 2621440, q 549283 1310720, q 1098569 2621440, q 274643 655360, q 219715 524288, q 549289 1310720, q 1098581 2621440, q 137323 327680, q 1098587 2621440, q 109859 262144, q 1098593 2621440, q 274649 655360, q 1098599 2621440, q 549301 1310720, q 219721 524288, q 68663 163840, q 1098611 2621440, q 549307 1310720, q 1098617 2621440 ] theorem cover15_ok : checkCover (q 8030906143 10000000000) (q 1098617 2621440) (q 2194789 5242880) cover15 = true := by decide +kernel theorem cover15_sound : ∀ σ ∈ Set.Icc (((q 2194789 5242880) : ℚ) : ℝ) (((q 1098617 2621440) : ℚ) : ℝ), rsF σ ≤ (((q 8030906143 10000000000) : ℚ) : ℝ) := checkCover_sound cover15_ok end MaxLeafFormal.RSRate