MaxLeafFormal.RSCover2
Source file MaxLeafFormal/RSCover2.lean of the Lean project (how it is built).
import MaxLeafFormal.RSCheck
/-!
# RS closed-form rate: cover 1, chunk 2 (generated)
Generated by `scripts/export_rs_cover.py` (bisection as in
`ancillary/rs_closed_form_interval.py`,
SHA-256 `6ea21466e9a6f7153bafd754cbc8d0cdea78ef1c6f83ec9b25309d6aec87643e`).
500 intervals covering [272057/655360, 109055/262144] 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 `272057/655360`. -/
def cover2 : List ℚ := [
q 544117 1310720,
q 13603 32768,
q 544123 1310720,
q 272063 655360,
q 544129 1310720,
q 136033 327680,
q 108827 262144,
q 272069 655360,
q 544141 1310720,
q 34009 81920,
q 544147 1310720,
q 54415 131072,
q 544153 1310720,
q 136039 327680,
q 544159 1310720,
q 272081 655360,
q 108833 262144,
q 68021 163840,
q 544171 1310720,
q 272087 655360,
q 544177 1310720,
q 27209 65536,
q 544183 1310720,
q 272093 655360,
q 544189 1310720,
q 8503 20480,
q 108839 262144,
q 272099 655360,
q 544201 1310720,
q 136051 327680,
q 544207 1310720,
q 54421 131072,
q 544213 1310720,
q 68027 163840,
q 544219 1310720,
q 272111 655360,
q 108845 262144,
q 136057 327680,
q 544231 1310720,
q 272117 655360,
q 544237 1310720,
q 6803 16384,
q 544243 1310720,
q 272123 655360,
q 544249 1310720,
q 136063 327680,
q 108851 262144,
q 272129 655360,
q 544261 1310720,
q 68033 163840,
q 544267 1310720,
q 54427 131072,
q 544273 1310720,
q 136069 327680,
q 544279 1310720,
q 272141 655360,
q 108857 262144,
q 17009 40960,
q 544291 1310720,
q 272147 655360,
q 544297 1310720,
q 27215 65536,
q 544303 1310720,
q 272153 655360,
q 544309 1310720,
q 68039 163840,
q 108863 262144,
q 272159 655360,
q 544321 1310720,
q 136081 327680,
q 544327 1310720,
q 54433 131072,
q 544333 1310720,
q 34021 81920,
q 544339 1310720,
q 272171 655360,
q 108869 262144,
q 136087 327680,
q 544351 1310720,
q 272177 655360,
q 544357 1310720,
q 13609 32768,
q 544363 1310720,
q 272183 655360,
q 544369 1310720,
q 136093 327680,
q 108875 262144,
q 272189 655360,
q 544381 1310720,
q 4253 10240,
q 544387 1310720,
q 54439 131072,
q 544393 1310720,
q 136099 327680,
q 544399 1310720,
q 272201 655360,
q 108881 262144,
q 68051 163840,
q 544411 1310720,
q 272207 655360,
q 544417 1310720,
q 27221 65536,
q 544423 1310720,
q 272213 655360,
q 544429 1310720,
q 34027 81920,
q 108887 262144,
q 272219 655360,
q 544441 1310720,
q 136111 327680,
q 544447 1310720,
q 54445 131072,
q 544453 1310720,
q 68057 163840,
q 544459 1310720,
q 272231 655360,
q 108893 262144,
q 136117 327680,
q 544471 1310720,
q 272237 655360,
q 544477 1310720,
q 3403 8192,
q 544483 1310720,
q 272243 655360,
q 544489 1310720,
q 136123 327680,
q 108899 262144,
q 272249 655360,
q 544501 1310720,
q 68063 163840,
q 544507 1310720,
q 54451 131072,
q 544513 1310720,
q 136129 327680,
q 544519 1310720,
q 272261 655360,
q 108905 262144,
q 34033 81920,
q 544531 1310720,
q 272267 655360,
q 544537 1310720,
q 27227 65536,
q 544543 1310720,
q 272273 655360,
q 544549 1310720,
q 68069 163840,
q 108911 262144,
q 272279 655360,
q 544561 1310720,
q 136141 327680,
q 544567 1310720,
q 54457 131072,
q 544573 1310720,
q 8509 20480,
q 544579 1310720,
q 272291 655360,
q 108917 262144,
q 136147 327680,
q 544591 1310720,
q 272297 655360,
q 544597 1310720,
q 13615 32768,
q 544603 1310720,
q 272303 655360,
q 544609 1310720,
q 136153 327680,
q 108923 262144,
q 272309 655360,
q 544621 1310720,
q 34039 81920,
q 544627 1310720,
q 54463 131072,
q 544633 1310720,
q 136159 327680,
q 544639 1310720,
q 272321 655360,
q 108929 262144,
q 68081 163840,
q 544651 1310720,
q 272327 655360,
q 544657 1310720,
q 27233 65536,
q 544663 1310720,
q 272333 655360,
q 544669 1310720,
q 17021 40960,
q 108935 262144,
q 272339 655360,
q 544681 1310720,
q 136171 327680,
q 544687 1310720,
q 54469 131072,
q 544693 1310720,
q 68087 163840,
q 544699 1310720,
q 272351 655360,
q 108941 262144,
q 136177 327680,
q 544711 1310720,
q 272357 655360,
q 544717 1310720,
q 6809 16384,
q 544723 1310720,
q 272363 655360,
q 544729 1310720,
q 136183 327680,
q 108947 262144,
q 272369 655360,
q 544741 1310720,
q 68093 163840,
q 544747 1310720,
q 54475 131072,
q 544753 1310720,
q 136189 327680,
q 544759 1310720,
q 272381 655360,
q 108953 262144,
q 133 320,
q 544771 1310720,
q 272387 655360,
q 544777 1310720,
q 27239 65536,
q 544783 1310720,
q 272393 655360,
q 544789 1310720,
q 68099 163840,
q 108959 262144,
q 272399 655360,
q 544801 1310720,
q 136201 327680,
q 544807 1310720,
q 54481 131072,
q 544813 1310720,
q 34051 81920,
q 544819 1310720,
q 272411 655360,
q 108965 262144,
q 136207 327680,
q 544831 1310720,
q 272417 655360,
q 544837 1310720,
q 13621 32768,
q 544843 1310720,
q 272423 655360,
q 544849 1310720,
q 136213 327680,
q 108971 262144,
q 272429 655360,
q 544861 1310720,
q 17027 40960,
q 544867 1310720,
q 54487 131072,
q 544873 1310720,
q 136219 327680,
q 544879 1310720,
q 272441 655360,
q 108977 262144,
q 68111 163840,
q 544891 1310720,
q 272447 655360,
q 544897 1310720,
q 27245 65536,
q 544903 1310720,
q 272453 655360,
q 544909 1310720,
q 34057 81920,
q 108983 262144,
q 272459 655360,
q 544921 1310720,
q 136231 327680,
q 544927 1310720,
q 54493 131072,
q 544933 1310720,
q 68117 163840,
q 217975 524288,
q 544939 1310720,
q 1089881 2621440,
q 272471 655360,
q 1089887 2621440,
q 108989 262144,
q 1089893 2621440,
q 136237 327680,
q 1089899 2621440,
q 544951 1310720,
q 217981 524288,
q 272477 655360,
q 1089911 2621440,
q 544957 1310720,
q 1089917 2621440,
q 1703 4096,
q 1089923 2621440,
q 544963 1310720,
q 1089929 2621440,
q 272483 655360,
q 217987 524288,
q 544969 1310720,
q 1089941 2621440,
q 136243 327680,
q 1089947 2621440,
q 108995 262144,
q 1089953 2621440,
q 272489 655360,
q 1089959 2621440,
q 544981 1310720,
q 217993 524288,
q 68123 163840,
q 1089971 2621440,
q 544987 1310720,
q 1089977 2621440,
q 54499 131072,
q 1089983 2621440,
q 544993 1310720,
q 1089989 2621440,
q 136249 327680,
q 217999 524288,
q 544999 1310720,
q 1090001 2621440,
q 272501 655360,
q 1090007 2621440,
q 109001 262144,
q 1090013 2621440,
q 34063 81920,
q 1090019 2621440,
q 545011 1310720,
q 218005 524288,
q 272507 655360,
q 1090031 2621440,
q 545017 1310720,
q 1090037 2621440,
q 27251 65536,
q 1090043 2621440,
q 545023 1310720,
q 1090049 2621440,
q 272513 655360,
q 218011 524288,
q 545029 1310720,
q 1090061 2621440,
q 68129 163840,
q 1090067 2621440,
q 109007 262144,
q 1090073 2621440,
q 272519 655360,
q 1090079 2621440,
q 545041 1310720,
q 218017 524288,
q 136261 327680,
q 1090091 2621440,
q 545047 1310720,
q 1090097 2621440,
q 54505 131072,
q 1090103 2621440,
q 545053 1310720,
q 1090109 2621440,
q 17033 40960,
q 218023 524288,
q 545059 1310720,
q 1090121 2621440,
q 272531 655360,
q 1090127 2621440,
q 109013 262144,
q 1090133 2621440,
q 136267 327680,
q 1090139 2621440,
q 545071 1310720,
q 218029 524288,
q 272537 655360,
q 1090151 2621440,
q 545077 1310720,
q 1090157 2621440,
q 13627 32768,
q 1090163 2621440,
q 545083 1310720,
q 1090169 2621440,
q 272543 655360,
q 218035 524288,
q 545089 1310720,
q 1090181 2621440,
q 136273 327680,
q 1090187 2621440,
q 109019 262144,
q 1090193 2621440,
q 272549 655360,
q 1090199 2621440,
q 545101 1310720,
q 218041 524288,
q 34069 81920,
q 1090211 2621440,
q 545107 1310720,
q 1090217 2621440,
q 54511 131072,
q 1090223 2621440,
q 545113 1310720,
q 1090229 2621440,
q 136279 327680,
q 218047 524288,
q 545119 1310720,
q 1090241 2621440,
q 272561 655360,
q 1090247 2621440,
q 109025 262144,
q 1090253 2621440,
q 68141 163840,
q 1090259 2621440,
q 545131 1310720,
q 218053 524288,
q 272567 655360,
q 1090271 2621440,
q 545137 1310720,
q 1090277 2621440,
q 27257 65536,
q 1090283 2621440,
q 545143 1310720,
q 1090289 2621440,
q 272573 655360,
q 218059 524288,
q 545149 1310720,
q 1090301 2621440,
q 4259 10240,
q 1090307 2621440,
q 109031 262144,
q 1090313 2621440,
q 272579 655360,
q 1090319 2621440,
q 545161 1310720,
q 218065 524288,
q 136291 327680,
q 1090331 2621440,
q 545167 1310720,
q 1090337 2621440,
q 54517 131072,
q 1090343 2621440,
q 545173 1310720,
q 1090349 2621440,
q 68147 163840,
q 218071 524288,
q 545179 1310720,
q 1090361 2621440,
q 272591 655360,
q 1090367 2621440,
q 109037 262144,
q 1090373 2621440,
q 136297 327680,
q 1090379 2621440,
q 545191 1310720,
q 218077 524288,
q 272597 655360,
q 1090391 2621440,
q 545197 1310720,
q 1090397 2621440,
q 6815 16384,
q 1090403 2621440,
q 545203 1310720,
q 1090409 2621440,
q 272603 655360,
q 218083 524288,
q 545209 1310720,
q 1090421 2621440,
q 136303 327680,
q 1090427 2621440,
q 109043 262144,
q 1090433 2621440,
q 272609 655360,
q 1090439 2621440,
q 545221 1310720,
q 218089 524288,
q 68153 163840,
q 1090451 2621440,
q 545227 1310720,
q 1090457 2621440,
q 54523 131072,
q 1090463 2621440,
q 545233 1310720,
q 1090469 2621440,
q 136309 327680,
q 218095 524288,
q 545239 1310720,
q 1090481 2621440,
q 272621 655360,
q 1090487 2621440,
q 109049 262144,
q 1090493 2621440,
q 17039 40960,
q 1090499 2621440,
q 545251 1310720,
q 218101 524288,
q 272627 655360,
q 1090511 2621440,
q 545257 1310720,
q 1090517 2621440,
q 27263 65536,
q 1090523 2621440,
q 545263 1310720,
q 1090529 2621440,
q 272633 655360,
q 218107 524288,
q 545269 1310720,
q 1090541 2621440,
q 68159 163840,
q 1090547 2621440,
q 109055 262144
]
theorem cover2_ok :
checkCover (q 8030906143 10000000000) (q 109055 262144) (q 272057 655360) cover2 = true := by
decide +kernel
theorem cover2_sound : ∀ σ ∈ Set.Icc (((q 272057 655360) : ℚ) : ℝ) (((q 109055 262144) : ℚ) : ℝ),
rsF σ ≤ (((q 8030906143 10000000000) : ℚ) : ℝ) :=
checkCover_sound cover2_ok
end MaxLeafFormal.RSRate