MaxLeafFormal.RSCover6
Source file MaxLeafFormal/RSCover6.lean of the Lean project (how it is built).
import MaxLeafFormal.RSCheck
/-!
# RS closed-form rate: cover 1, chunk 6 (generated)
Generated by `scripts/export_rs_cover.py` (bisection as in
`ancillary/rs_closed_form_interval.py`,
SHA-256 `6ea21466e9a6f7153bafd754cbc8d0cdea78ef1c6f83ec9b25309d6aec87643e`).
500 intervals covering [874675/2097152, 874975/2097152] 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 `874675/2097152`. -/
def cover6 : List ℚ := [
q 2186689 5242880,
q 4373381 10485760,
q 546673 1310720,
q 4373387 10485760,
q 437339 1048576,
q 4373393 10485760,
q 1093349 2621440,
q 4373399 10485760,
q 2186701 5242880,
q 874681 2097152,
q 136669 327680,
q 4373411 10485760,
q 2186707 5242880,
q 4373417 10485760,
q 218671 524288,
q 4373423 10485760,
q 2186713 5242880,
q 4373429 10485760,
q 546679 1310720,
q 874687 2097152,
q 2186719 5242880,
q 4373441 10485760,
q 1093361 2621440,
q 4373447 10485760,
q 437345 1048576,
q 4373453 10485760,
q 273341 655360,
q 4373459 10485760,
q 2186731 5242880,
q 874693 2097152,
q 1093367 2621440,
q 4373471 10485760,
q 2186737 5242880,
q 4373477 10485760,
q 109337 262144,
q 4373483 10485760,
q 2186743 5242880,
q 4373489 10485760,
q 1093373 2621440,
q 874699 2097152,
q 2186749 5242880,
q 4373501 10485760,
q 4271 10240,
q 4373507 10485760,
q 437351 1048576,
q 4373513 10485760,
q 1093379 2621440,
q 4373519 10485760,
q 2186761 5242880,
q 874705 2097152,
q 546691 1310720,
q 4373531 10485760,
q 2186767 5242880,
q 4373537 10485760,
q 218677 524288,
q 4373543 10485760,
q 2186773 5242880,
q 4373549 10485760,
q 273347 655360,
q 874711 2097152,
q 2186779 5242880,
q 4373561 10485760,
q 1093391 2621440,
q 4373567 10485760,
q 437357 1048576,
q 4373573 10485760,
q 546697 1310720,
q 4373579 10485760,
q 2186791 5242880,
q 874717 2097152,
q 1093397 2621440,
q 4373591 10485760,
q 2186797 5242880,
q 4373597 10485760,
q 27335 65536,
q 4373603 10485760,
q 2186803 5242880,
q 4373609 10485760,
q 1093403 2621440,
q 874723 2097152,
q 2186809 5242880,
q 4373621 10485760,
q 546703 1310720,
q 4373627 10485760,
q 437363 1048576,
q 4373633 10485760,
q 1093409 2621440,
q 4373639 10485760,
q 2186821 5242880,
q 874729 2097152,
q 273353 655360,
q 4373651 10485760,
q 2186827 5242880,
q 4373657 10485760,
q 218683 524288,
q 4373663 10485760,
q 2186833 5242880,
q 4373669 10485760,
q 546709 1310720,
q 874735 2097152,
q 2186839 5242880,
q 4373681 10485760,
q 1093421 2621440,
q 4373687 10485760,
q 437369 1048576,
q 4373693 10485760,
q 68339 163840,
q 4373699 10485760,
q 2186851 5242880,
q 874741 2097152,
q 1093427 2621440,
q 4373711 10485760,
q 2186857 5242880,
q 4373717 10485760,
q 109343 262144,
q 4373723 10485760,
q 2186863 5242880,
q 4373729 10485760,
q 1093433 2621440,
q 874747 2097152,
q 2186869 5242880,
q 4373741 10485760,
q 273359 655360,
q 4373747 10485760,
q 437375 1048576,
q 4373753 10485760,
q 1093439 2621440,
q 4373759 10485760,
q 2186881 5242880,
q 874753 2097152,
q 546721 1310720,
q 4373771 10485760,
q 2186887 5242880,
q 4373777 10485760,
q 218689 524288,
q 4373783 10485760,
q 2186893 5242880,
q 4373789 10485760,
q 136681 327680,
q 874759 2097152,
q 2186899 5242880,
q 4373801 10485760,
q 1093451 2621440,
q 4373807 10485760,
q 437381 1048576,
q 4373813 10485760,
q 546727 1310720,
q 4373819 10485760,
q 2186911 5242880,
q 874765 2097152,
q 1093457 2621440,
q 4373831 10485760,
q 2186917 5242880,
q 4373837 10485760,
q 54673 131072,
q 4373843 10485760,
q 2186923 5242880,
q 4373849 10485760,
q 1093463 2621440,
q 874771 2097152,
q 2186929 5242880,
q 4373861 10485760,
q 546733 1310720,
q 4373867 10485760,
q 437387 1048576,
q 4373873 10485760,
q 1093469 2621440,
q 4373879 10485760,
q 2186941 5242880,
q 874777 2097152,
q 34171 81920,
q 4373891 10485760,
q 2186947 5242880,
q 4373897 10485760,
q 218695 524288,
q 4373903 10485760,
q 2186953 5242880,
q 4373909 10485760,
q 546739 1310720,
q 874783 2097152,
q 2186959 5242880,
q 4373921 10485760,
q 1093481 2621440,
q 4373927 10485760,
q 437393 1048576,
q 4373933 10485760,
q 273371 655360,
q 4373939 10485760,
q 2186971 5242880,
q 874789 2097152,
q 1093487 2621440,
q 4373951 10485760,
q 2186977 5242880,
q 4373957 10485760,
q 109349 262144,
q 4373963 10485760,
q 2186983 5242880,
q 4373969 10485760,
q 1093493 2621440,
q 874795 2097152,
q 2186989 5242880,
q 4373981 10485760,
q 136687 327680,
q 4373987 10485760,
q 437399 1048576,
q 4373993 10485760,
q 1093499 2621440,
q 4373999 10485760,
q 2187001 5242880,
q 874801 2097152,
q 546751 1310720,
q 4374011 10485760,
q 2187007 5242880,
q 4374017 10485760,
q 218701 524288,
q 4374023 10485760,
q 2187013 5242880,
q 4374029 10485760,
q 273377 655360,
q 874807 2097152,
q 2187019 5242880,
q 4374041 10485760,
q 1093511 2621440,
q 4374047 10485760,
q 437405 1048576,
q 4374053 10485760,
q 546757 1310720,
q 4374059 10485760,
q 2187031 5242880,
q 874813 2097152,
q 1093517 2621440,
q 4374071 10485760,
q 2187037 5242880,
q 4374077 10485760,
q 13669 32768,
q 4374083 10485760,
q 2187043 5242880,
q 4374089 10485760,
q 1093523 2621440,
q 874819 2097152,
q 2187049 5242880,
q 4374101 10485760,
q 546763 1310720,
q 4374107 10485760,
q 437411 1048576,
q 4374113 10485760,
q 1093529 2621440,
q 4374119 10485760,
q 2187061 5242880,
q 874825 2097152,
q 273383 655360,
q 4374131 10485760,
q 2187067 5242880,
q 4374137 10485760,
q 218707 524288,
q 4374143 10485760,
q 2187073 5242880,
q 4374149 10485760,
q 546769 1310720,
q 874831 2097152,
q 2187079 5242880,
q 4374161 10485760,
q 1093541 2621440,
q 4374167 10485760,
q 437417 1048576,
q 4374173 10485760,
q 136693 327680,
q 4374179 10485760,
q 2187091 5242880,
q 874837 2097152,
q 1093547 2621440,
q 4374191 10485760,
q 2187097 5242880,
q 4374197 10485760,
q 109355 262144,
q 4374203 10485760,
q 2187103 5242880,
q 4374209 10485760,
q 1093553 2621440,
q 874843 2097152,
q 2187109 5242880,
q 4374221 10485760,
q 273389 655360,
q 4374227 10485760,
q 437423 1048576,
q 4374233 10485760,
q 1093559 2621440,
q 4374239 10485760,
q 2187121 5242880,
q 874849 2097152,
q 546781 1310720,
q 4374251 10485760,
q 2187127 5242880,
q 4374257 10485760,
q 218713 524288,
q 4374263 10485760,
q 2187133 5242880,
q 4374269 10485760,
q 17087 40960,
q 874855 2097152,
q 2187139 5242880,
q 4374281 10485760,
q 1093571 2621440,
q 4374287 10485760,
q 437429 1048576,
q 4374293 10485760,
q 546787 1310720,
q 4374299 10485760,
q 2187151 5242880,
q 874861 2097152,
q 1093577 2621440,
q 4374311 10485760,
q 2187157 5242880,
q 4374317 10485760,
q 54679 131072,
q 4374323 10485760,
q 2187163 5242880,
q 4374329 10485760,
q 1093583 2621440,
q 874867 2097152,
q 2187169 5242880,
q 4374341 10485760,
q 546793 1310720,
q 4374347 10485760,
q 437435 1048576,
q 4374353 10485760,
q 1093589 2621440,
q 4374359 10485760,
q 2187181 5242880,
q 874873 2097152,
q 136699 327680,
q 4374371 10485760,
q 2187187 5242880,
q 4374377 10485760,
q 218719 524288,
q 4374383 10485760,
q 2187193 5242880,
q 4374389 10485760,
q 546799 1310720,
q 874879 2097152,
q 2187199 5242880,
q 4374401 10485760,
q 1093601 2621440,
q 4374407 10485760,
q 437441 1048576,
q 4374413 10485760,
q 273401 655360,
q 4374419 10485760,
q 2187211 5242880,
q 874885 2097152,
q 1093607 2621440,
q 4374431 10485760,
q 2187217 5242880,
q 4374437 10485760,
q 109361 262144,
q 4374443 10485760,
q 2187223 5242880,
q 4374449 10485760,
q 1093613 2621440,
q 874891 2097152,
q 2187229 5242880,
q 4374461 10485760,
q 68351 163840,
q 4374467 10485760,
q 437447 1048576,
q 4374473 10485760,
q 1093619 2621440,
q 4374479 10485760,
q 2187241 5242880,
q 874897 2097152,
q 546811 1310720,
q 4374491 10485760,
q 2187247 5242880,
q 4374497 10485760,
q 218725 524288,
q 4374503 10485760,
q 2187253 5242880,
q 4374509 10485760,
q 273407 655360,
q 874903 2097152,
q 2187259 5242880,
q 4374521 10485760,
q 1093631 2621440,
q 4374527 10485760,
q 437453 1048576,
q 4374533 10485760,
q 546817 1310720,
q 4374539 10485760,
q 2187271 5242880,
q 874909 2097152,
q 1093637 2621440,
q 4374551 10485760,
q 2187277 5242880,
q 4374557 10485760,
q 27341 65536,
q 4374563 10485760,
q 2187283 5242880,
q 4374569 10485760,
q 1093643 2621440,
q 874915 2097152,
q 2187289 5242880,
q 4374581 10485760,
q 546823 1310720,
q 4374587 10485760,
q 437459 1048576,
q 4374593 10485760,
q 1093649 2621440,
q 4374599 10485760,
q 2187301 5242880,
q 874921 2097152,
q 273413 655360,
q 4374611 10485760,
q 2187307 5242880,
q 4374617 10485760,
q 218731 524288,
q 4374623 10485760,
q 2187313 5242880,
q 4374629 10485760,
q 546829 1310720,
q 874927 2097152,
q 2187319 5242880,
q 4374641 10485760,
q 1093661 2621440,
q 4374647 10485760,
q 437465 1048576,
q 4374653 10485760,
q 34177 81920,
q 4374659 10485760,
q 2187331 5242880,
q 874933 2097152,
q 1093667 2621440,
q 4374671 10485760,
q 2187337 5242880,
q 4374677 10485760,
q 109367 262144,
q 4374683 10485760,
q 2187343 5242880,
q 4374689 10485760,
q 1093673 2621440,
q 874939 2097152,
q 2187349 5242880,
q 4374701 10485760,
q 273419 655360,
q 4374707 10485760,
q 437471 1048576,
q 4374713 10485760,
q 1093679 2621440,
q 4374719 10485760,
q 2187361 5242880,
q 874945 2097152,
q 546841 1310720,
q 4374731 10485760,
q 2187367 5242880,
q 4374737 10485760,
q 218737 524288,
q 4374743 10485760,
q 2187373 5242880,
q 4374749 10485760,
q 136711 327680,
q 874951 2097152,
q 2187379 5242880,
q 4374761 10485760,
q 1093691 2621440,
q 4374767 10485760,
q 437477 1048576,
q 4374773 10485760,
q 546847 1310720,
q 4374779 10485760,
q 2187391 5242880,
q 874957 2097152,
q 1093697 2621440,
q 4374791 10485760,
q 2187397 5242880,
q 4374797 10485760,
q 54685 131072,
q 4374803 10485760,
q 2187403 5242880,
q 4374809 10485760,
q 1093703 2621440,
q 874963 2097152,
q 2187409 5242880,
q 4374821 10485760,
q 546853 1310720,
q 4374827 10485760,
q 437483 1048576,
q 4374833 10485760,
q 1093709 2621440,
q 4374839 10485760,
q 2187421 5242880,
q 874969 2097152,
q 68357 163840,
q 4374851 10485760,
q 2187427 5242880,
q 4374857 10485760,
q 218743 524288,
q 4374863 10485760,
q 2187433 5242880,
q 4374869 10485760,
q 546859 1310720,
q 874975 2097152
]
theorem cover6_ok :
checkCover (q 8030906143 10000000000) (q 874975 2097152) (q 874675 2097152) cover6 = true := by
decide +kernel
theorem cover6_sound : ∀ σ ∈ Set.Icc (((q 874675 2097152) : ℚ) : ℝ) (((q 874975 2097152) : ℚ) : ℝ),
rsF σ ≤ (((q 8030906143 10000000000) : ℚ) : ℝ) :=
checkCover_sound cover6_ok
end MaxLeafFormal.RSRate