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