MaxLeafFormal.RSCover5
Source file MaxLeafFormal/RSCover5.lean of the Lean project (how it is built).
import MaxLeafFormal.RSCheck
/-!
# RS closed-form rate: cover 1, chunk 5 (generated)
Generated by `scripts/export_rs_cover.py` (bisection as in
`ancillary/rs_closed_form_interval.py`,
SHA-256 `6ea21466e9a6f7153bafd754cbc8d0cdea78ef1c6f83ec9b25309d6aec87643e`).
500 intervals covering [54631/131072, 874675/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 `54631/131072`. -/
def cover5 : List ℚ := [
q 2185243 5242880,
q 1092623 2621440,
q 2185249 5242880,
q 546313 1310720,
q 437051 1048576,
q 1092629 2621440,
q 2185261 5242880,
q 136579 327680,
q 2185267 5242880,
q 218527 524288,
q 2185273 5242880,
q 546319 1310720,
q 2185279 5242880,
q 1092641 2621440,
q 437057 1048576,
q 273161 655360,
q 2185291 5242880,
q 1092647 2621440,
q 2185297 5242880,
q 109265 262144,
q 2185303 5242880,
q 1092653 2621440,
q 2185309 5242880,
q 68291 163840,
q 437063 1048576,
q 1092659 2621440,
q 2185321 5242880,
q 546331 1310720,
q 2185327 5242880,
q 218533 524288,
q 2185333 5242880,
q 273167 655360,
q 2185339 5242880,
q 1092671 2621440,
q 437069 1048576,
q 546337 1310720,
q 2185351 5242880,
q 1092677 2621440,
q 2185357 5242880,
q 27317 65536,
q 2185363 5242880,
q 1092683 2621440,
q 2185369 5242880,
q 546343 1310720,
q 437075 1048576,
q 1092689 2621440,
q 2185381 5242880,
q 273173 655360,
q 2185387 5242880,
q 218539 524288,
q 2185393 5242880,
q 546349 1310720,
q 2185399 5242880,
q 1092701 2621440,
q 437081 1048576,
q 34147 81920,
q 2185411 5242880,
q 1092707 2621440,
q 2185417 5242880,
q 109271 262144,
q 2185423 5242880,
q 1092713 2621440,
q 2185429 5242880,
q 273179 655360,
q 437087 1048576,
q 1092719 2621440,
q 2185441 5242880,
q 546361 1310720,
q 2185447 5242880,
q 218545 524288,
q 2185453 5242880,
q 136591 327680,
q 2185459 5242880,
q 1092731 2621440,
q 437093 1048576,
q 546367 1310720,
q 2185471 5242880,
q 1092737 2621440,
q 2185477 5242880,
q 54637 131072,
q 2185483 5242880,
q 1092743 2621440,
q 2185489 5242880,
q 546373 1310720,
q 437099 1048576,
q 1092749 2621440,
q 2185501 5242880,
q 68297 163840,
q 2185507 5242880,
q 218551 524288,
q 2185513 5242880,
q 546379 1310720,
q 2185519 5242880,
q 1092761 2621440,
q 437105 1048576,
q 273191 655360,
q 2185531 5242880,
q 1092767 2621440,
q 2185537 5242880,
q 109277 262144,
q 2185543 5242880,
q 1092773 2621440,
q 2185549 5242880,
q 136597 327680,
q 437111 1048576,
q 1092779 2621440,
q 2185561 5242880,
q 546391 1310720,
q 2185567 5242880,
q 218557 524288,
q 2185573 5242880,
q 273197 655360,
q 2185579 5242880,
q 1092791 2621440,
q 437117 1048576,
q 546397 1310720,
q 2185591 5242880,
q 1092797 2621440,
q 2185597 5242880,
q 3415 8192,
q 2185603 5242880,
q 1092803 2621440,
q 2185609 5242880,
q 546403 1310720,
q 437123 1048576,
q 1092809 2621440,
q 2185621 5242880,
q 273203 655360,
q 2185627 5242880,
q 218563 524288,
q 2185633 5242880,
q 546409 1310720,
q 2185639 5242880,
q 1092821 2621440,
q 437129 1048576,
q 136603 327680,
q 2185651 5242880,
q 1092827 2621440,
q 2185657 5242880,
q 109283 262144,
q 2185663 5242880,
q 1092833 2621440,
q 2185669 5242880,
q 273209 655360,
q 437135 1048576,
q 1092839 2621440,
q 2185681 5242880,
q 546421 1310720,
q 2185687 5242880,
q 218569 524288,
q 2185693 5242880,
q 68303 163840,
q 2185699 5242880,
q 1092851 2621440,
q 437141 1048576,
q 546427 1310720,
q 2185711 5242880,
q 1092857 2621440,
q 2185717 5242880,
q 54643 131072,
q 2185723 5242880,
q 1092863 2621440,
q 2185729 5242880,
q 546433 1310720,
q 437147 1048576,
q 1092869 2621440,
q 2185741 5242880,
q 136609 327680,
q 2185747 5242880,
q 218575 524288,
q 2185753 5242880,
q 546439 1310720,
q 2185759 5242880,
q 1092881 2621440,
q 437153 1048576,
q 273221 655360,
q 2185771 5242880,
q 1092887 2621440,
q 2185777 5242880,
q 109289 262144,
q 2185783 5242880,
q 1092893 2621440,
q 2185789 5242880,
q 34153 81920,
q 437159 1048576,
q 1092899 2621440,
q 2185801 5242880,
q 546451 1310720,
q 2185807 5242880,
q 218581 524288,
q 2185813 5242880,
q 273227 655360,
q 2185819 5242880,
q 1092911 2621440,
q 437165 1048576,
q 546457 1310720,
q 2185831 5242880,
q 1092917 2621440,
q 2185837 5242880,
q 27323 65536,
q 2185843 5242880,
q 1092923 2621440,
q 2185849 5242880,
q 546463 1310720,
q 437171 1048576,
q 1092929 2621440,
q 2185861 5242880,
q 273233 655360,
q 2185867 5242880,
q 218587 524288,
q 2185873 5242880,
q 546469 1310720,
q 2185879 5242880,
q 1092941 2621440,
q 437177 1048576,
q 68309 163840,
q 2185891 5242880,
q 1092947 2621440,
q 2185897 5242880,
q 109295 262144,
q 2185903 5242880,
q 1092953 2621440,
q 2185909 5242880,
q 273239 655360,
q 437183 1048576,
q 1092959 2621440,
q 2185921 5242880,
q 546481 1310720,
q 2185927 5242880,
q 218593 524288,
q 2185933 5242880,
q 136621 327680,
q 2185939 5242880,
q 1092971 2621440,
q 437189 1048576,
q 546487 1310720,
q 2185951 5242880,
q 1092977 2621440,
q 2185957 5242880,
q 54649 131072,
q 2185963 5242880,
q 1092983 2621440,
q 2185969 5242880,
q 546493 1310720,
q 437195 1048576,
q 1092989 2621440,
q 2185981 5242880,
q 8539 20480,
q 2185987 5242880,
q 218599 524288,
q 2185993 5242880,
q 546499 1310720,
q 2185999 5242880,
q 1093001 2621440,
q 437201 1048576,
q 273251 655360,
q 2186011 5242880,
q 1093007 2621440,
q 2186017 5242880,
q 109301 262144,
q 2186023 5242880,
q 1093013 2621440,
q 2186029 5242880,
q 136627 327680,
q 437207 1048576,
q 1093019 2621440,
q 2186041 5242880,
q 546511 1310720,
q 2186047 5242880,
q 218605 524288,
q 2186053 5242880,
q 273257 655360,
q 2186059 5242880,
q 1093031 2621440,
q 437213 1048576,
q 546517 1310720,
q 2186071 5242880,
q 1093037 2621440,
q 2186077 5242880,
q 13663 32768,
q 2186083 5242880,
q 1093043 2621440,
q 2186089 5242880,
q 546523 1310720,
q 437219 1048576,
q 1093049 2621440,
q 2186101 5242880,
q 273263 655360,
q 2186107 5242880,
q 218611 524288,
q 2186113 5242880,
q 546529 1310720,
q 2186119 5242880,
q 1093061 2621440,
q 437225 1048576,
q 136633 327680,
q 2186131 5242880,
q 1093067 2621440,
q 2186137 5242880,
q 109307 262144,
q 2186143 5242880,
q 1093073 2621440,
q 2186149 5242880,
q 273269 655360,
q 437231 1048576,
q 1093079 2621440,
q 2186161 5242880,
q 546541 1310720,
q 2186167 5242880,
q 218617 524288,
q 2186173 5242880,
q 34159 81920,
q 2186179 5242880,
q 1093091 2621440,
q 437237 1048576,
q 546547 1310720,
q 2186191 5242880,
q 1093097 2621440,
q 2186197 5242880,
q 54655 131072,
q 2186203 5242880,
q 1093103 2621440,
q 2186209 5242880,
q 546553 1310720,
q 437243 1048576,
q 1093109 2621440,
q 2186221 5242880,
q 136639 327680,
q 2186227 5242880,
q 218623 524288,
q 2186233 5242880,
q 546559 1310720,
q 2186239 5242880,
q 1093121 2621440,
q 437249 1048576,
q 273281 655360,
q 2186251 5242880,
q 1093127 2621440,
q 2186257 5242880,
q 109313 262144,
q 2186263 5242880,
q 1093133 2621440,
q 2186269 5242880,
q 68321 163840,
q 437255 1048576,
q 1093139 2621440,
q 2186281 5242880,
q 546571 1310720,
q 2186287 5242880,
q 218629 524288,
q 2186293 5242880,
q 273287 655360,
q 2186299 5242880,
q 1093151 2621440,
q 437261 1048576,
q 546577 1310720,
q 2186311 5242880,
q 1093157 2621440,
q 2186317 5242880,
q 27329 65536,
q 2186323 5242880,
q 1093163 2621440,
q 2186329 5242880,
q 546583 1310720,
q 437267 1048576,
q 1093169 2621440,
q 2186341 5242880,
q 273293 655360,
q 2186347 5242880,
q 218635 524288,
q 2186353 5242880,
q 546589 1310720,
q 2186359 5242880,
q 1093181 2621440,
q 437273 1048576,
q 17081 40960,
q 2186371 5242880,
q 1093187 2621440,
q 2186377 5242880,
q 109319 262144,
q 2186383 5242880,
q 1093193 2621440,
q 2186389 5242880,
q 273299 655360,
q 437279 1048576,
q 1093199 2621440,
q 2186401 5242880,
q 546601 1310720,
q 2186407 5242880,
q 218641 524288,
q 2186413 5242880,
q 136651 327680,
q 2186419 5242880,
q 1093211 2621440,
q 437285 1048576,
q 546607 1310720,
q 2186431 5242880,
q 1093217 2621440,
q 2186437 5242880,
q 54661 131072,
q 2186443 5242880,
q 1093223 2621440,
q 2186449 5242880,
q 546613 1310720,
q 437291 1048576,
q 1093229 2621440,
q 2186461 5242880,
q 68327 163840,
q 2186467 5242880,
q 218647 524288,
q 2186473 5242880,
q 546619 1310720,
q 2186479 5242880,
q 1093241 2621440,
q 437297 1048576,
q 273311 655360,
q 2186491 5242880,
q 1093247 2621440,
q 2186497 5242880,
q 109325 262144,
q 2186503 5242880,
q 1093253 2621440,
q 2186509 5242880,
q 136657 327680,
q 437303 1048576,
q 1093259 2621440,
q 2186521 5242880,
q 546631 1310720,
q 2186527 5242880,
q 218653 524288,
q 2186533 5242880,
q 273317 655360,
q 2186539 5242880,
q 1093271 2621440,
q 437309 1048576,
q 546637 1310720,
q 2186551 5242880,
q 1093277 2621440,
q 2186557 5242880,
q 6833 16384,
q 2186563 5242880,
q 1093283 2621440,
q 2186569 5242880,
q 546643 1310720,
q 437315 1048576,
q 1093289 2621440,
q 2186581 5242880,
q 273323 655360,
q 2186587 5242880,
q 218659 524288,
q 2186593 5242880,
q 546649 1310720,
q 2186599 5242880,
q 1093301 2621440,
q 437321 1048576,
q 136663 327680,
q 2186611 5242880,
q 1093307 2621440,
q 2186617 5242880,
q 109331 262144,
q 2186623 5242880,
q 1093313 2621440,
q 2186629 5242880,
q 273329 655360,
q 437327 1048576,
q 4373273 10485760,
q 1093319 2621440,
q 4373279 10485760,
q 2186641 5242880,
q 874657 2097152,
q 546661 1310720,
q 4373291 10485760,
q 2186647 5242880,
q 4373297 10485760,
q 218665 524288,
q 4373303 10485760,
q 2186653 5242880,
q 4373309 10485760,
q 68333 163840,
q 874663 2097152,
q 2186659 5242880,
q 4373321 10485760,
q 1093331 2621440,
q 4373327 10485760,
q 437333 1048576,
q 4373333 10485760,
q 546667 1310720,
q 4373339 10485760,
q 2186671 5242880,
q 874669 2097152,
q 1093337 2621440,
q 4373351 10485760,
q 2186677 5242880,
q 4373357 10485760,
q 54667 131072,
q 4373363 10485760,
q 2186683 5242880,
q 4373369 10485760,
q 1093343 2621440,
q 874675 2097152
]
theorem cover5_ok :
checkCover (q 8030906143 10000000000) (q 874675 2097152) (q 54631 131072) cover5 = true := by
decide +kernel
theorem cover5_sound : ∀ σ ∈ Set.Icc (((q 54631 131072) : ℚ) : ℝ) (((q 874675 2097152) : ℚ) : ℝ),
rsF σ ≤ (((q 8030906143 10000000000) : ℚ) : ℝ) :=
checkCover_sound cover5_ok
end MaxLeafFormal.RSRate