MaxLeafFormal.RSCover18
Source file MaxLeafFormal/RSCover18.lean of the Lean project (how it is built).
import MaxLeafFormal.RSCheck
/-!
# RS closed-form rate: cover 1, chunk 18 (generated)
Generated by `scripts/export_rs_cover.py` (bisection as in
`ancillary/rs_closed_form_interval.py`,
SHA-256 `6ea21466e9a6f7153bafd754cbc8d0cdea78ef1c6f83ec9b25309d6aec87643e`).
500 intervals covering [69131/163840, 2281/5120] 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 `69131/163840`. -/
def cover18 : List ℚ := [
q 27653 65536,
q 34567 81920,
q 138271 327680,
q 69137 163840,
q 138277 327680,
q 3457 8192,
q 138283 327680,
q 69143 163840,
q 138289 327680,
q 34573 81920,
q 27659 65536,
q 69149 163840,
q 138301 327680,
q 2161 5120,
q 138307 327680,
q 13831 32768,
q 138313 327680,
q 34579 81920,
q 138319 327680,
q 69161 163840,
q 27665 65536,
q 17291 40960,
q 138331 327680,
q 69167 163840,
q 138337 327680,
q 6917 16384,
q 138343 327680,
q 69173 163840,
q 138349 327680,
q 8647 20480,
q 27671 65536,
q 69179 163840,
q 138361 327680,
q 34591 81920,
q 138367 327680,
q 13837 32768,
q 138373 327680,
q 17297 40960,
q 138379 327680,
q 69191 163840,
q 27677 65536,
q 34597 81920,
q 138391 327680,
q 69197 163840,
q 138397 327680,
q 865 2048,
q 138403 327680,
q 69203 163840,
q 138409 327680,
q 34603 81920,
q 27683 65536,
q 69209 163840,
q 138421 327680,
q 17303 40960,
q 138427 327680,
q 13843 32768,
q 138433 327680,
q 34609 81920,
q 138439 327680,
q 69221 163840,
q 27689 65536,
q 8653 20480,
q 138451 327680,
q 69227 163840,
q 138457 327680,
q 6923 16384,
q 138463 327680,
q 69233 163840,
q 138469 327680,
q 17309 40960,
q 27695 65536,
q 69239 163840,
q 138481 327680,
q 34621 81920,
q 138487 327680,
q 13849 32768,
q 138493 327680,
q 541 1280,
q 138499 327680,
q 69251 163840,
q 27701 65536,
q 34627 81920,
q 138511 327680,
q 69257 163840,
q 138517 327680,
q 3463 8192,
q 138523 327680,
q 69263 163840,
q 138529 327680,
q 34633 81920,
q 27707 65536,
q 69269 163840,
q 138541 327680,
q 8659 20480,
q 138547 327680,
q 13855 32768,
q 138553 327680,
q 34639 81920,
q 138559 327680,
q 69281 163840,
q 27713 65536,
q 17321 40960,
q 138571 327680,
q 69287 163840,
q 138577 327680,
q 6929 16384,
q 138583 327680,
q 69293 163840,
q 138589 327680,
q 4331 10240,
q 27719 65536,
q 69299 163840,
q 138601 327680,
q 34651 81920,
q 138607 327680,
q 13861 32768,
q 138613 327680,
q 17327 40960,
q 138619 327680,
q 69311 163840,
q 27725 65536,
q 34657 81920,
q 138631 327680,
q 69317 163840,
q 138637 327680,
q 1733 4096,
q 138643 327680,
q 69323 163840,
q 138649 327680,
q 34663 81920,
q 27731 65536,
q 69329 163840,
q 138661 327680,
q 17333 40960,
q 138667 327680,
q 13867 32768,
q 138673 327680,
q 34669 81920,
q 138679 327680,
q 69341 163840,
q 27737 65536,
q 2167 5120,
q 138691 327680,
q 69347 163840,
q 138697 327680,
q 6935 16384,
q 69353 163840,
q 17339 40960,
q 69359 163840,
q 34681 81920,
q 13873 32768,
q 8671 20480,
q 69371 163840,
q 34687 81920,
q 69377 163840,
q 3469 8192,
q 69383 163840,
q 34693 81920,
q 69389 163840,
q 4337 10240,
q 13879 32768,
q 34699 81920,
q 69401 163840,
q 17351 40960,
q 69407 163840,
q 6941 16384,
q 69413 163840,
q 8677 20480,
q 69419 163840,
q 34711 81920,
q 13885 32768,
q 17357 40960,
q 69431 163840,
q 34717 81920,
q 69437 163840,
q 217 512,
q 69443 163840,
q 34723 81920,
q 69449 163840,
q 17363 40960,
q 13891 32768,
q 34729 81920,
q 69461 163840,
q 8683 20480,
q 69467 163840,
q 6947 16384,
q 69473 163840,
q 17369 40960,
q 69479 163840,
q 34741 81920,
q 13897 32768,
q 4343 10240,
q 69491 163840,
q 34747 81920,
q 69497 163840,
q 3475 8192,
q 69503 163840,
q 34753 81920,
q 69509 163840,
q 8689 20480,
q 13903 32768,
q 34759 81920,
q 69521 163840,
q 17381 40960,
q 69527 163840,
q 6953 16384,
q 69533 163840,
q 2173 5120,
q 69539 163840,
q 34771 81920,
q 13909 32768,
q 17387 40960,
q 69551 163840,
q 34777 81920,
q 69557 163840,
q 1739 4096,
q 69563 163840,
q 34783 81920,
q 69569 163840,
q 17393 40960,
q 13915 32768,
q 34789 81920,
q 69581 163840,
q 4349 10240,
q 69587 163840,
q 6959 16384,
q 69593 163840,
q 17399 40960,
q 69599 163840,
q 34801 81920,
q 13921 32768,
q 8701 20480,
q 69611 163840,
q 34807 81920,
q 69617 163840,
q 3481 8192,
q 69623 163840,
q 34813 81920,
q 69629 163840,
q 17 40,
q 13927 32768,
q 34819 81920,
q 69641 163840,
q 17411 40960,
q 69647 163840,
q 6965 16384,
q 69653 163840,
q 8707 20480,
q 69659 163840,
q 34831 81920,
q 13933 32768,
q 17417 40960,
q 69671 163840,
q 34837 81920,
q 69677 163840,
q 871 2048,
q 69683 163840,
q 34843 81920,
q 69689 163840,
q 17423 40960,
q 13939 32768,
q 34849 81920,
q 69701 163840,
q 8713 20480,
q 69707 163840,
q 6971 16384,
q 69713 163840,
q 17429 40960,
q 69719 163840,
q 34861 81920,
q 13945 32768,
q 2179 5120,
q 69731 163840,
q 34867 81920,
q 69737 163840,
q 3487 8192,
q 69743 163840,
q 34873 81920,
q 8719 20480,
q 34879 81920,
q 17441 40960,
q 6977 16384,
q 4361 10240,
q 34891 81920,
q 17447 40960,
q 34897 81920,
q 1745 4096,
q 34903 81920,
q 17453 40960,
q 34909 81920,
q 1091 2560,
q 6983 16384,
q 17459 40960,
q 34921 81920,
q 8731 20480,
q 34927 81920,
q 3493 8192,
q 34933 81920,
q 4367 10240,
q 34939 81920,
q 17471 40960,
q 6989 16384,
q 8737 20480,
q 34951 81920,
q 17477 40960,
q 34957 81920,
q 437 1024,
q 34963 81920,
q 17483 40960,
q 34969 81920,
q 8743 20480,
q 6995 16384,
q 17489 40960,
q 34981 81920,
q 4373 10240,
q 34987 81920,
q 3499 8192,
q 34993 81920,
q 8749 20480,
q 34999 81920,
q 17501 40960,
q 7001 16384,
q 547 1280,
q 35011 81920,
q 17507 40960,
q 35017 81920,
q 1751 4096,
q 35023 81920,
q 17513 40960,
q 35029 81920,
q 4379 10240,
q 7007 16384,
q 17519 40960,
q 35041 81920,
q 8761 20480,
q 35047 81920,
q 3505 8192,
q 35053 81920,
q 2191 5120,
q 35059 81920,
q 17531 40960,
q 7013 16384,
q 8767 20480,
q 35071 81920,
q 17537 40960,
q 35077 81920,
q 877 2048,
q 35083 81920,
q 17543 40960,
q 35089 81920,
q 8773 20480,
q 7019 16384,
q 17549 40960,
q 35101 81920,
q 1097 2560,
q 35107 81920,
q 3511 8192,
q 35113 81920,
q 8779 20480,
q 35119 81920,
q 17561 40960,
q 7025 16384,
q 4391 10240,
q 35131 81920,
q 17567 40960,
q 35137 81920,
q 1757 4096,
q 35143 81920,
q 17573 40960,
q 35149 81920,
q 2197 5120,
q 17579 40960,
q 8791 20480,
q 3517 8192,
q 4397 10240,
q 17591 40960,
q 8797 20480,
q 17597 40960,
q 55 128,
q 17603 40960,
q 8803 20480,
q 17609 40960,
q 4403 10240,
q 3523 8192,
q 8809 20480,
q 17621 40960,
q 2203 5120,
q 17627 40960,
q 1763 4096,
q 17633 40960,
q 4409 10240,
q 17639 40960,
q 8821 20480,
q 3529 8192,
q 1103 2560,
q 17651 40960,
q 8827 20480,
q 17657 40960,
q 883 2048,
q 17663 40960,
q 8833 20480,
q 17669 40960,
q 2209 5120,
q 3535 8192,
q 8839 20480,
q 17681 40960,
q 4421 10240,
q 17687 40960,
q 1769 4096,
q 17693 40960,
q 553 1280,
q 17699 40960,
q 8851 20480,
q 3541 8192,
q 4427 10240,
q 17711 40960,
q 8857 20480,
q 17717 40960,
q 443 1024,
q 17723 40960,
q 8863 20480,
q 17729 40960,
q 4433 10240,
q 3547 8192,
q 8869 20480,
q 17741 40960,
q 1109 2560,
q 17747 40960,
q 1775 4096,
q 17753 40960,
q 4439 10240,
q 17759 40960,
q 8881 20480,
q 3553 8192,
q 2221 5120,
q 17771 40960,
q 8887 20480,
q 889 2048,
q 8893 20480,
q 139 320,
q 8899 20480,
q 4451 10240,
q 1781 4096,
q 2227 5120,
q 8911 20480,
q 4457 10240,
q 8917 20480,
q 223 512,
q 8923 20480,
q 4463 10240,
q 8929 20480,
q 2233 5120,
q 1787 4096,
q 4469 10240,
q 8941 20480,
q 559 1280,
q 8947 20480,
q 895 2048,
q 8953 20480,
q 2239 5120,
q 8959 20480,
q 4481 10240,
q 1793 4096,
q 1121 2560,
q 8971 20480,
q 4487 10240,
q 8977 20480,
q 449 1024,
q 8983 20480,
q 4493 10240,
q 8989 20480,
q 281 640,
q 1799 4096,
q 4499 10240,
q 9001 20480,
q 2251 5120,
q 9007 20480,
q 901 2048,
q 9013 20480,
q 1127 2560,
q 9019 20480,
q 4511 10240,
q 1805 4096,
q 2257 5120,
q 4517 10240,
q 113 256,
q 4523 10240,
q 2263 5120,
q 4529 10240,
q 1133 2560,
q 907 2048,
q 2269 5120,
q 4541 10240,
q 71 160,
q 4547 10240,
q 455 1024,
q 4553 10240,
q 1139 2560,
q 4559 10240,
q 2281 5120
]
theorem cover18_ok :
checkCover (q 8030906143 10000000000) (q 2281 5120) (q 69131 163840) cover18 = true := by
decide +kernel
theorem cover18_sound : ∀ σ ∈ Set.Icc (((q 69131 163840) : ℚ) : ℝ) (((q 2281 5120) : ℚ) : ℝ),
rsF σ ≤ (((q 8030906143 10000000000) : ℚ) : ℝ) :=
checkCover_sound cover18_ok
end MaxLeafFormal.RSRate