MaxLeafFormal.RSCover0
Source file MaxLeafFormal/RSCover0.lean of the Lean project (how it is built).
import MaxLeafFormal.RSCheck
/-!
# RS closed-form rate: cover 1, chunk 0 (generated)
Generated by `scripts/export_rs_cover.py` (bisection as in
`ancillary/rs_closed_form_interval.py`,
SHA-256 `6ea21466e9a6f7153bafd754cbc8d0cdea78ef1c6f83ec9b25309d6aec87643e`).
500 intervals covering [1/5, 67601/163840] 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 `1/5`. -/
def cover0 : List ℚ := [
q 7 32,
q 19 80,
q 41 160,
q 17 64,
q 11 40,
q 91 320,
q 47 160,
q 191 640,
q 97 320,
q 197 640,
q 5 16,
q 203 640,
q 103 320,
q 209 640,
q 53 160,
q 427 1280,
q 43 128,
q 433 1280,
q 109 320,
q 439 1280,
q 221 640,
q 89 256,
q 7 20,
q 451 1280,
q 227 640,
q 911 2560,
q 457 1280,
q 917 2560,
q 23 64,
q 923 2560,
q 463 1280,
q 929 2560,
q 233 640,
q 187 512,
q 469 1280,
q 941 2560,
q 59 160,
q 947 2560,
q 95 256,
q 953 2560,
q 1909 5120,
q 239 640,
q 383 1024,
q 959 2560,
q 1921 5120,
q 481 1280,
q 1927 5120,
q 193 512,
q 1933 5120,
q 121 320,
q 1939 5120,
q 971 2560,
q 389 1024,
q 487 1280,
q 1951 5120,
q 977 2560,
q 1957 5120,
q 49 128,
q 1963 5120,
q 983 2560,
q 1969 5120,
q 493 1280,
q 395 1024,
q 3953 10240,
q 989 2560,
q 3959 10240,
q 1981 5120,
q 793 2048,
q 31 80,
q 3971 10240,
q 1987 5120,
q 3977 10240,
q 199 512,
q 3983 10240,
q 1993 5120,
q 3989 10240,
q 499 1280,
q 799 2048,
q 1999 5120,
q 4001 10240,
q 1001 2560,
q 4007 10240,
q 401 1024,
q 4013 10240,
q 251 640,
q 4019 10240,
q 2011 5120,
q 805 2048,
q 1007 2560,
q 4031 10240,
q 2017 5120,
q 4037 10240,
q 101 256,
q 4043 10240,
q 8089 20480,
q 2023 5120,
q 1619 4096,
q 4049 10240,
q 8101 20480,
q 1013 2560,
q 8107 20480,
q 811 2048,
q 8113 20480,
q 2029 5120,
q 8119 20480,
q 4061 10240,
q 1625 4096,
q 127 320,
q 8131 20480,
q 4067 10240,
q 8137 20480,
q 407 1024,
q 8143 20480,
q 4073 10240,
q 8149 20480,
q 1019 2560,
q 1631 4096,
q 4079 10240,
q 8161 20480,
q 2041 5120,
q 8167 20480,
q 817 2048,
q 8173 20480,
q 511 1280,
q 8179 20480,
q 4091 10240,
q 1637 4096,
q 2047 5120,
q 8191 20480,
q 4097 10240,
q 8197 20480,
q 205 512,
q 8203 20480,
q 4103 10240,
q 8209 20480,
q 2053 5120,
q 1643 4096,
q 4109 10240,
q 8221 20480,
q 3289 8192,
q 257 640,
q 16451 40960,
q 8227 20480,
q 16457 40960,
q 823 2048,
q 16463 40960,
q 8233 20480,
q 16469 40960,
q 2059 5120,
q 3295 8192,
q 8239 20480,
q 16481 40960,
q 4121 10240,
q 16487 40960,
q 1649 4096,
q 16493 40960,
q 1031 2560,
q 16499 40960,
q 8251 20480,
q 3301 8192,
q 4127 10240,
q 16511 40960,
q 8257 20480,
q 16517 40960,
q 413 1024,
q 16523 40960,
q 8263 20480,
q 16529 40960,
q 4133 10240,
q 3307 8192,
q 8269 20480,
q 16541 40960,
q 517 1280,
q 16547 40960,
q 1655 4096,
q 16553 40960,
q 4139 10240,
q 16559 40960,
q 8281 20480,
q 3313 8192,
q 2071 5120,
q 16571 40960,
q 8287 20480,
q 16577 40960,
q 829 2048,
q 16583 40960,
q 8293 20480,
q 16589 40960,
q 1037 2560,
q 3319 8192,
q 8299 20480,
q 16601 40960,
q 4151 10240,
q 16607 40960,
q 1661 4096,
q 16613 40960,
q 2077 5120,
q 16619 40960,
q 8311 20480,
q 3325 8192,
q 4157 10240,
q 16631 40960,
q 8317 20480,
q 16637 40960,
q 33277 81920,
q 13 32,
q 33283 81920,
q 16643 40960,
q 33289 81920,
q 8323 20480,
q 6659 16384,
q 16649 40960,
q 33301 81920,
q 4163 10240,
q 33307 81920,
q 3331 8192,
q 33313 81920,
q 8329 20480,
q 33319 81920,
q 16661 40960,
q 6665 16384,
q 2083 5120,
q 33331 81920,
q 16667 40960,
q 33337 81920,
q 1667 4096,
q 33343 81920,
q 16673 40960,
q 33349 81920,
q 4169 10240,
q 6671 16384,
q 16679 40960,
q 33361 81920,
q 8341 20480,
q 33367 81920,
q 3337 8192,
q 33373 81920,
q 1043 2560,
q 33379 81920,
q 16691 40960,
q 6677 16384,
q 8347 20480,
q 33391 81920,
q 16697 40960,
q 33397 81920,
q 835 2048,
q 33403 81920,
q 16703 40960,
q 33409 81920,
q 8353 20480,
q 6683 16384,
q 16709 40960,
q 33421 81920,
q 2089 5120,
q 33427 81920,
q 3343 8192,
q 33433 81920,
q 8359 20480,
q 33439 81920,
q 16721 40960,
q 6689 16384,
q 4181 10240,
q 33451 81920,
q 16727 40960,
q 33457 81920,
q 1673 4096,
q 33463 81920,
q 16733 40960,
q 33469 81920,
q 523 1280,
q 6695 16384,
q 16739 40960,
q 33481 81920,
q 8371 20480,
q 33487 81920,
q 3349 8192,
q 33493 81920,
q 4187 10240,
q 33499 81920,
q 16751 40960,
q 6701 16384,
q 8377 20480,
q 33511 81920,
q 16757 40960,
q 33517 81920,
q 419 1024,
q 33523 81920,
q 16763 40960,
q 33529 81920,
q 8383 20480,
q 6707 16384,
q 16769 40960,
q 33541 81920,
q 4193 10240,
q 33547 81920,
q 3355 8192,
q 67103 163840,
q 33553 81920,
q 67109 163840,
q 8389 20480,
q 13423 32768,
q 33559 81920,
q 67121 163840,
q 16781 40960,
q 67127 163840,
q 6713 16384,
q 67133 163840,
q 1049 2560,
q 67139 163840,
q 33571 81920,
q 13429 32768,
q 16787 40960,
q 67151 163840,
q 33577 81920,
q 67157 163840,
q 1679 4096,
q 67163 163840,
q 33583 81920,
q 67169 163840,
q 16793 40960,
q 13435 32768,
q 33589 81920,
q 67181 163840,
q 4199 10240,
q 67187 163840,
q 6719 16384,
q 67193 163840,
q 16799 40960,
q 67199 163840,
q 33601 81920,
q 13441 32768,
q 8401 20480,
q 67211 163840,
q 33607 81920,
q 67217 163840,
q 3361 8192,
q 67223 163840,
q 33613 81920,
q 67229 163840,
q 2101 5120,
q 13447 32768,
q 33619 81920,
q 67241 163840,
q 16811 40960,
q 67247 163840,
q 6725 16384,
q 67253 163840,
q 8407 20480,
q 67259 163840,
q 33631 81920,
q 13453 32768,
q 16817 40960,
q 67271 163840,
q 33637 81920,
q 67277 163840,
q 841 2048,
q 67283 163840,
q 33643 81920,
q 67289 163840,
q 16823 40960,
q 13459 32768,
q 33649 81920,
q 67301 163840,
q 8413 20480,
q 67307 163840,
q 6731 16384,
q 67313 163840,
q 16829 40960,
q 67319 163840,
q 33661 81920,
q 13465 32768,
q 263 640,
q 67331 163840,
q 33667 81920,
q 67337 163840,
q 3367 8192,
q 67343 163840,
q 33673 81920,
q 67349 163840,
q 8419 20480,
q 13471 32768,
q 33679 81920,
q 67361 163840,
q 16841 40960,
q 67367 163840,
q 6737 16384,
q 67373 163840,
q 4211 10240,
q 67379 163840,
q 33691 81920,
q 13477 32768,
q 16847 40960,
q 67391 163840,
q 33697 81920,
q 67397 163840,
q 1685 4096,
q 67403 163840,
q 33703 81920,
q 67409 163840,
q 16853 40960,
q 13483 32768,
q 33709 81920,
q 67421 163840,
q 2107 5120,
q 67427 163840,
q 6743 16384,
q 67433 163840,
q 16859 40960,
q 67439 163840,
q 33721 81920,
q 13489 32768,
q 8431 20480,
q 67451 163840,
q 33727 81920,
q 67457 163840,
q 3373 8192,
q 67463 163840,
q 33733 81920,
q 67469 163840,
q 4217 10240,
q 13495 32768,
q 33739 81920,
q 67481 163840,
q 16871 40960,
q 67487 163840,
q 6749 16384,
q 134983 327680,
q 67493 163840,
q 134989 327680,
q 8437 20480,
q 26999 65536,
q 67499 163840,
q 135001 327680,
q 33751 81920,
q 135007 327680,
q 13501 32768,
q 135013 327680,
q 16877 40960,
q 135019 327680,
q 67511 163840,
q 27005 65536,
q 33757 81920,
q 135031 327680,
q 67517 163840,
q 135037 327680,
q 211 512,
q 135043 327680,
q 67523 163840,
q 135049 327680,
q 33763 81920,
q 27011 65536,
q 67529 163840,
q 135061 327680,
q 16883 40960,
q 135067 327680,
q 13507 32768,
q 135073 327680,
q 33769 81920,
q 135079 327680,
q 67541 163840,
q 27017 65536,
q 8443 20480,
q 135091 327680,
q 67547 163840,
q 135097 327680,
q 6755 16384,
q 135103 327680,
q 67553 163840,
q 135109 327680,
q 16889 40960,
q 27023 65536,
q 67559 163840,
q 135121 327680,
q 33781 81920,
q 135127 327680,
q 13513 32768,
q 135133 327680,
q 4223 10240,
q 135139 327680,
q 67571 163840,
q 27029 65536,
q 33787 81920,
q 135151 327680,
q 67577 163840,
q 135157 327680,
q 3379 8192,
q 135163 327680,
q 67583 163840,
q 135169 327680,
q 33793 81920,
q 27035 65536,
q 67589 163840,
q 135181 327680,
q 8449 20480,
q 135187 327680,
q 13519 32768,
q 135193 327680,
q 33799 81920,
q 135199 327680,
q 67601 163840
]
theorem cover0_ok :
checkCover (q 8030906143 10000000000) (q 67601 163840) (q 1 5) cover0 = true := by
decide +kernel
theorem cover0_sound : ∀ σ ∈ Set.Icc (((q 1 5) : ℚ) : ℝ) (((q 67601 163840) : ℚ) : ℝ),
rsF σ ≤ (((q 8030906143 10000000000) : ℚ) : ℝ) :=
checkCover_sound cover0_ok
end MaxLeafFormal.RSRate