MaxLeafFormal.RSCover8
Source file MaxLeafFormal/RSCover8.lean of the Lean project (how it is built).
import MaxLeafFormal.RSCheck
/-!
# RS closed-form rate: cover 1, chunk 8 (generated)
Generated by `scripts/export_rs_cover.py` (bisection as in
`ancillary/rs_closed_form_interval.py`,
SHA-256 `6ea21466e9a6f7153bafd754cbc8d0cdea78ef1c6f83ec9b25309d6aec87643e`).
500 intervals covering [875275/2097152, 875575/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 `875275/2097152`. -/
def cover8 : List ℚ := [
q 2188189 5242880,
q 4376381 10485760,
q 68381 163840,
q 4376387 10485760,
q 437639 1048576,
q 4376393 10485760,
q 1094099 2621440,
q 4376399 10485760,
q 2188201 5242880,
q 875281 2097152,
q 547051 1310720,
q 4376411 10485760,
q 2188207 5242880,
q 4376417 10485760,
q 218821 524288,
q 4376423 10485760,
q 2188213 5242880,
q 4376429 10485760,
q 273527 655360,
q 875287 2097152,
q 2188219 5242880,
q 4376441 10485760,
q 1094111 2621440,
q 4376447 10485760,
q 437645 1048576,
q 4376453 10485760,
q 547057 1310720,
q 4376459 10485760,
q 2188231 5242880,
q 875293 2097152,
q 1094117 2621440,
q 4376471 10485760,
q 2188237 5242880,
q 4376477 10485760,
q 27353 65536,
q 4376483 10485760,
q 2188243 5242880,
q 4376489 10485760,
q 1094123 2621440,
q 875299 2097152,
q 2188249 5242880,
q 4376501 10485760,
q 547063 1310720,
q 4376507 10485760,
q 437651 1048576,
q 4376513 10485760,
q 1094129 2621440,
q 4376519 10485760,
q 2188261 5242880,
q 875305 2097152,
q 273533 655360,
q 4376531 10485760,
q 2188267 5242880,
q 4376537 10485760,
q 218827 524288,
q 4376543 10485760,
q 2188273 5242880,
q 4376549 10485760,
q 547069 1310720,
q 875311 2097152,
q 2188279 5242880,
q 4376561 10485760,
q 1094141 2621440,
q 4376567 10485760,
q 437657 1048576,
q 4376573 10485760,
q 2137 5120,
q 4376579 10485760,
q 2188291 5242880,
q 875317 2097152,
q 1094147 2621440,
q 4376591 10485760,
q 2188297 5242880,
q 4376597 10485760,
q 109415 262144,
q 4376603 10485760,
q 2188303 5242880,
q 4376609 10485760,
q 1094153 2621440,
q 875323 2097152,
q 2188309 5242880,
q 4376621 10485760,
q 273539 655360,
q 4376627 10485760,
q 437663 1048576,
q 4376633 10485760,
q 1094159 2621440,
q 4376639 10485760,
q 2188321 5242880,
q 875329 2097152,
q 547081 1310720,
q 4376651 10485760,
q 2188327 5242880,
q 4376657 10485760,
q 218833 524288,
q 4376663 10485760,
q 2188333 5242880,
q 4376669 10485760,
q 136771 327680,
q 875335 2097152,
q 2188339 5242880,
q 4376681 10485760,
q 1094171 2621440,
q 4376687 10485760,
q 437669 1048576,
q 4376693 10485760,
q 547087 1310720,
q 4376699 10485760,
q 2188351 5242880,
q 875341 2097152,
q 1094177 2621440,
q 4376711 10485760,
q 2188357 5242880,
q 4376717 10485760,
q 54709 131072,
q 4376723 10485760,
q 2188363 5242880,
q 4376729 10485760,
q 1094183 2621440,
q 875347 2097152,
q 2188369 5242880,
q 4376741 10485760,
q 547093 1310720,
q 4376747 10485760,
q 437675 1048576,
q 4376753 10485760,
q 1094189 2621440,
q 4376759 10485760,
q 2188381 5242880,
q 875353 2097152,
q 68387 163840,
q 4376771 10485760,
q 2188387 5242880,
q 4376777 10485760,
q 218839 524288,
q 4376783 10485760,
q 2188393 5242880,
q 4376789 10485760,
q 547099 1310720,
q 875359 2097152,
q 2188399 5242880,
q 4376801 10485760,
q 1094201 2621440,
q 4376807 10485760,
q 437681 1048576,
q 4376813 10485760,
q 273551 655360,
q 4376819 10485760,
q 2188411 5242880,
q 875365 2097152,
q 1094207 2621440,
q 4376831 10485760,
q 2188417 5242880,
q 4376837 10485760,
q 109421 262144,
q 4376843 10485760,
q 2188423 5242880,
q 4376849 10485760,
q 1094213 2621440,
q 875371 2097152,
q 2188429 5242880,
q 4376861 10485760,
q 136777 327680,
q 4376867 10485760,
q 437687 1048576,
q 4376873 10485760,
q 1094219 2621440,
q 4376879 10485760,
q 2188441 5242880,
q 875377 2097152,
q 547111 1310720,
q 4376891 10485760,
q 2188447 5242880,
q 4376897 10485760,
q 218845 524288,
q 4376903 10485760,
q 2188453 5242880,
q 4376909 10485760,
q 273557 655360,
q 875383 2097152,
q 2188459 5242880,
q 4376921 10485760,
q 1094231 2621440,
q 4376927 10485760,
q 437693 1048576,
q 4376933 10485760,
q 547117 1310720,
q 4376939 10485760,
q 2188471 5242880,
q 875389 2097152,
q 1094237 2621440,
q 4376951 10485760,
q 2188477 5242880,
q 4376957 10485760,
q 6839 16384,
q 4376963 10485760,
q 2188483 5242880,
q 4376969 10485760,
q 1094243 2621440,
q 875395 2097152,
q 2188489 5242880,
q 4376981 10485760,
q 547123 1310720,
q 4376987 10485760,
q 437699 1048576,
q 4376993 10485760,
q 1094249 2621440,
q 4376999 10485760,
q 2188501 5242880,
q 875401 2097152,
q 273563 655360,
q 4377011 10485760,
q 2188507 5242880,
q 4377017 10485760,
q 218851 524288,
q 4377023 10485760,
q 2188513 5242880,
q 4377029 10485760,
q 547129 1310720,
q 875407 2097152,
q 2188519 5242880,
q 4377041 10485760,
q 1094261 2621440,
q 4377047 10485760,
q 437705 1048576,
q 4377053 10485760,
q 136783 327680,
q 4377059 10485760,
q 2188531 5242880,
q 875413 2097152,
q 1094267 2621440,
q 4377071 10485760,
q 2188537 5242880,
q 4377077 10485760,
q 109427 262144,
q 4377083 10485760,
q 2188543 5242880,
q 4377089 10485760,
q 1094273 2621440,
q 875419 2097152,
q 2188549 5242880,
q 4377101 10485760,
q 273569 655360,
q 4377107 10485760,
q 437711 1048576,
q 4377113 10485760,
q 1094279 2621440,
q 4377119 10485760,
q 2188561 5242880,
q 875425 2097152,
q 547141 1310720,
q 4377131 10485760,
q 2188567 5242880,
q 4377137 10485760,
q 218857 524288,
q 4377143 10485760,
q 2188573 5242880,
q 4377149 10485760,
q 68393 163840,
q 875431 2097152,
q 2188579 5242880,
q 4377161 10485760,
q 1094291 2621440,
q 4377167 10485760,
q 437717 1048576,
q 4377173 10485760,
q 547147 1310720,
q 4377179 10485760,
q 2188591 5242880,
q 875437 2097152,
q 1094297 2621440,
q 4377191 10485760,
q 2188597 5242880,
q 4377197 10485760,
q 54715 131072,
q 4377203 10485760,
q 2188603 5242880,
q 4377209 10485760,
q 1094303 2621440,
q 875443 2097152,
q 2188609 5242880,
q 4377221 10485760,
q 547153 1310720,
q 4377227 10485760,
q 437723 1048576,
q 4377233 10485760,
q 1094309 2621440,
q 4377239 10485760,
q 2188621 5242880,
q 875449 2097152,
q 136789 327680,
q 4377251 10485760,
q 2188627 5242880,
q 4377257 10485760,
q 218863 524288,
q 4377263 10485760,
q 2188633 5242880,
q 4377269 10485760,
q 547159 1310720,
q 875455 2097152,
q 2188639 5242880,
q 4377281 10485760,
q 1094321 2621440,
q 4377287 10485760,
q 437729 1048576,
q 4377293 10485760,
q 273581 655360,
q 4377299 10485760,
q 2188651 5242880,
q 875461 2097152,
q 1094327 2621440,
q 4377311 10485760,
q 2188657 5242880,
q 4377317 10485760,
q 109433 262144,
q 4377323 10485760,
q 2188663 5242880,
q 4377329 10485760,
q 1094333 2621440,
q 875467 2097152,
q 2188669 5242880,
q 4377341 10485760,
q 17099 40960,
q 4377347 10485760,
q 437735 1048576,
q 4377353 10485760,
q 1094339 2621440,
q 4377359 10485760,
q 2188681 5242880,
q 875473 2097152,
q 547171 1310720,
q 4377371 10485760,
q 2188687 5242880,
q 4377377 10485760,
q 218869 524288,
q 4377383 10485760,
q 2188693 5242880,
q 4377389 10485760,
q 273587 655360,
q 875479 2097152,
q 2188699 5242880,
q 4377401 10485760,
q 1094351 2621440,
q 4377407 10485760,
q 437741 1048576,
q 4377413 10485760,
q 547177 1310720,
q 4377419 10485760,
q 2188711 5242880,
q 875485 2097152,
q 1094357 2621440,
q 4377431 10485760,
q 2188717 5242880,
q 4377437 10485760,
q 27359 65536,
q 4377443 10485760,
q 2188723 5242880,
q 4377449 10485760,
q 1094363 2621440,
q 875491 2097152,
q 2188729 5242880,
q 4377461 10485760,
q 547183 1310720,
q 4377467 10485760,
q 437747 1048576,
q 4377473 10485760,
q 1094369 2621440,
q 4377479 10485760,
q 2188741 5242880,
q 875497 2097152,
q 273593 655360,
q 4377491 10485760,
q 2188747 5242880,
q 4377497 10485760,
q 218875 524288,
q 4377503 10485760,
q 2188753 5242880,
q 4377509 10485760,
q 547189 1310720,
q 875503 2097152,
q 2188759 5242880,
q 4377521 10485760,
q 1094381 2621440,
q 4377527 10485760,
q 437753 1048576,
q 4377533 10485760,
q 68399 163840,
q 4377539 10485760,
q 2188771 5242880,
q 875509 2097152,
q 1094387 2621440,
q 4377551 10485760,
q 2188777 5242880,
q 4377557 10485760,
q 109439 262144,
q 4377563 10485760,
q 2188783 5242880,
q 4377569 10485760,
q 1094393 2621440,
q 875515 2097152,
q 2188789 5242880,
q 4377581 10485760,
q 273599 655360,
q 4377587 10485760,
q 437759 1048576,
q 4377593 10485760,
q 1094399 2621440,
q 4377599 10485760,
q 2188801 5242880,
q 875521 2097152,
q 547201 1310720,
q 4377611 10485760,
q 2188807 5242880,
q 4377617 10485760,
q 218881 524288,
q 4377623 10485760,
q 2188813 5242880,
q 4377629 10485760,
q 136801 327680,
q 875527 2097152,
q 2188819 5242880,
q 4377641 10485760,
q 1094411 2621440,
q 4377647 10485760,
q 437765 1048576,
q 4377653 10485760,
q 547207 1310720,
q 4377659 10485760,
q 2188831 5242880,
q 875533 2097152,
q 1094417 2621440,
q 4377671 10485760,
q 2188837 5242880,
q 4377677 10485760,
q 54721 131072,
q 4377683 10485760,
q 2188843 5242880,
q 4377689 10485760,
q 1094423 2621440,
q 875539 2097152,
q 2188849 5242880,
q 4377701 10485760,
q 547213 1310720,
q 4377707 10485760,
q 437771 1048576,
q 4377713 10485760,
q 1094429 2621440,
q 4377719 10485760,
q 2188861 5242880,
q 875545 2097152,
q 34201 81920,
q 4377731 10485760,
q 2188867 5242880,
q 4377737 10485760,
q 218887 524288,
q 4377743 10485760,
q 2188873 5242880,
q 4377749 10485760,
q 547219 1310720,
q 875551 2097152,
q 2188879 5242880,
q 4377761 10485760,
q 1094441 2621440,
q 4377767 10485760,
q 437777 1048576,
q 4377773 10485760,
q 273611 655360,
q 4377779 10485760,
q 2188891 5242880,
q 875557 2097152,
q 1094447 2621440,
q 4377791 10485760,
q 2188897 5242880,
q 4377797 10485760,
q 109445 262144,
q 4377803 10485760,
q 2188903 5242880,
q 4377809 10485760,
q 1094453 2621440,
q 875563 2097152,
q 2188909 5242880,
q 4377821 10485760,
q 136807 327680,
q 4377827 10485760,
q 437783 1048576,
q 4377833 10485760,
q 1094459 2621440,
q 4377839 10485760,
q 2188921 5242880,
q 875569 2097152,
q 547231 1310720,
q 4377851 10485760,
q 2188927 5242880,
q 4377857 10485760,
q 218893 524288,
q 4377863 10485760,
q 2188933 5242880,
q 4377869 10485760,
q 273617 655360,
q 875575 2097152
]
theorem cover8_ok :
checkCover (q 8030906143 10000000000) (q 875575 2097152) (q 875275 2097152) cover8 = true := by
decide +kernel
theorem cover8_sound : ∀ σ ∈ Set.Icc (((q 875275 2097152) : ℚ) : ℝ) (((q 875575 2097152) : ℚ) : ℝ),
rsF σ ≤ (((q 8030906143 10000000000) : ℚ) : ℝ) :=
checkCover_sound cover8_ok
end MaxLeafFormal.RSRate