MaxLeafFormal.RSCover13
Source file MaxLeafFormal/RSCover13.lean of the Lean project (how it is built).
import MaxLeafFormal.RSCheck
/-!
# RS closed-form rate: cover 1, chunk 13 (generated)
Generated by `scripts/export_rs_cover.py` (bisection as in
`ancillary/rs_closed_form_interval.py`,
SHA-256 `6ea21466e9a6f7153bafd754cbc8d0cdea78ef1c6f83ec9b25309d6aec87643e`).
500 intervals covering [876775/2097152, 2193289/5242880] 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 `876775/2097152`. -/
def cover13 : List ℚ := [
q 2191939 5242880,
q 4383881 10485760,
q 1095971 2621440,
q 4383887 10485760,
q 438389 1048576,
q 4383893 10485760,
q 547987 1310720,
q 4383899 10485760,
q 2191951 5242880,
q 876781 2097152,
q 1095977 2621440,
q 4383911 10485760,
q 2191957 5242880,
q 4383917 10485760,
q 54799 131072,
q 4383923 10485760,
q 2191963 5242880,
q 4383929 10485760,
q 1095983 2621440,
q 876787 2097152,
q 2191969 5242880,
q 4383941 10485760,
q 547993 1310720,
q 4383947 10485760,
q 438395 1048576,
q 4383953 10485760,
q 1095989 2621440,
q 4383959 10485760,
q 2191981 5242880,
q 876793 2097152,
q 136999 327680,
q 4383971 10485760,
q 2191987 5242880,
q 4383977 10485760,
q 219199 524288,
q 4383983 10485760,
q 2191993 5242880,
q 4383989 10485760,
q 547999 1310720,
q 876799 2097152,
q 2191999 5242880,
q 4384001 10485760,
q 1096001 2621440,
q 4384007 10485760,
q 438401 1048576,
q 4384013 10485760,
q 274001 655360,
q 4384019 10485760,
q 2192011 5242880,
q 876805 2097152,
q 1096007 2621440,
q 4384031 10485760,
q 2192017 5242880,
q 4384037 10485760,
q 109601 262144,
q 4384043 10485760,
q 2192023 5242880,
q 4384049 10485760,
q 1096013 2621440,
q 876811 2097152,
q 2192029 5242880,
q 4384061 10485760,
q 68501 163840,
q 4384067 10485760,
q 438407 1048576,
q 4384073 10485760,
q 1096019 2621440,
q 4384079 10485760,
q 2192041 5242880,
q 876817 2097152,
q 548011 1310720,
q 4384091 10485760,
q 2192047 5242880,
q 4384097 10485760,
q 219205 524288,
q 4384103 10485760,
q 2192053 5242880,
q 4384109 10485760,
q 274007 655360,
q 876823 2097152,
q 2192059 5242880,
q 4384121 10485760,
q 1096031 2621440,
q 4384127 10485760,
q 438413 1048576,
q 4384133 10485760,
q 548017 1310720,
q 4384139 10485760,
q 2192071 5242880,
q 876829 2097152,
q 1096037 2621440,
q 4384151 10485760,
q 2192077 5242880,
q 4384157 10485760,
q 27401 65536,
q 4384163 10485760,
q 2192083 5242880,
q 4384169 10485760,
q 1096043 2621440,
q 2192089 5242880,
q 548023 1310720,
q 438419 1048576,
q 1096049 2621440,
q 2192101 5242880,
q 274013 655360,
q 2192107 5242880,
q 219211 524288,
q 2192113 5242880,
q 548029 1310720,
q 2192119 5242880,
q 1096061 2621440,
q 438425 1048576,
q 8563 20480,
q 2192131 5242880,
q 1096067 2621440,
q 2192137 5242880,
q 109607 262144,
q 2192143 5242880,
q 1096073 2621440,
q 2192149 5242880,
q 274019 655360,
q 438431 1048576,
q 1096079 2621440,
q 2192161 5242880,
q 548041 1310720,
q 2192167 5242880,
q 219217 524288,
q 2192173 5242880,
q 137011 327680,
q 2192179 5242880,
q 1096091 2621440,
q 438437 1048576,
q 548047 1310720,
q 2192191 5242880,
q 1096097 2621440,
q 2192197 5242880,
q 54805 131072,
q 2192203 5242880,
q 1096103 2621440,
q 2192209 5242880,
q 548053 1310720,
q 438443 1048576,
q 1096109 2621440,
q 2192221 5242880,
q 68507 163840,
q 2192227 5242880,
q 219223 524288,
q 2192233 5242880,
q 548059 1310720,
q 2192239 5242880,
q 1096121 2621440,
q 438449 1048576,
q 274031 655360,
q 2192251 5242880,
q 1096127 2621440,
q 2192257 5242880,
q 109613 262144,
q 2192263 5242880,
q 1096133 2621440,
q 2192269 5242880,
q 137017 327680,
q 438455 1048576,
q 1096139 2621440,
q 2192281 5242880,
q 548071 1310720,
q 2192287 5242880,
q 219229 524288,
q 2192293 5242880,
q 274037 655360,
q 2192299 5242880,
q 1096151 2621440,
q 438461 1048576,
q 548077 1310720,
q 2192311 5242880,
q 1096157 2621440,
q 2192317 5242880,
q 6851 16384,
q 2192323 5242880,
q 1096163 2621440,
q 2192329 5242880,
q 548083 1310720,
q 438467 1048576,
q 1096169 2621440,
q 2192341 5242880,
q 274043 655360,
q 2192347 5242880,
q 219235 524288,
q 2192353 5242880,
q 548089 1310720,
q 2192359 5242880,
q 1096181 2621440,
q 438473 1048576,
q 137023 327680,
q 2192371 5242880,
q 1096187 2621440,
q 2192377 5242880,
q 109619 262144,
q 2192383 5242880,
q 1096193 2621440,
q 2192389 5242880,
q 274049 655360,
q 438479 1048576,
q 1096199 2621440,
q 2192401 5242880,
q 548101 1310720,
q 2192407 5242880,
q 219241 524288,
q 2192413 5242880,
q 68513 163840,
q 2192419 5242880,
q 1096211 2621440,
q 438485 1048576,
q 548107 1310720,
q 2192431 5242880,
q 1096217 2621440,
q 2192437 5242880,
q 54811 131072,
q 2192443 5242880,
q 1096223 2621440,
q 2192449 5242880,
q 548113 1310720,
q 438491 1048576,
q 1096229 2621440,
q 2192461 5242880,
q 137029 327680,
q 2192467 5242880,
q 219247 524288,
q 2192473 5242880,
q 548119 1310720,
q 2192479 5242880,
q 1096241 2621440,
q 438497 1048576,
q 274061 655360,
q 2192491 5242880,
q 1096247 2621440,
q 2192497 5242880,
q 109625 262144,
q 2192503 5242880,
q 1096253 2621440,
q 2192509 5242880,
q 17129 40960,
q 438503 1048576,
q 1096259 2621440,
q 2192521 5242880,
q 548131 1310720,
q 2192527 5242880,
q 219253 524288,
q 2192533 5242880,
q 274067 655360,
q 2192539 5242880,
q 1096271 2621440,
q 438509 1048576,
q 548137 1310720,
q 2192551 5242880,
q 1096277 2621440,
q 2192557 5242880,
q 27407 65536,
q 2192563 5242880,
q 1096283 2621440,
q 2192569 5242880,
q 548143 1310720,
q 438515 1048576,
q 1096289 2621440,
q 2192581 5242880,
q 274073 655360,
q 2192587 5242880,
q 219259 524288,
q 2192593 5242880,
q 548149 1310720,
q 2192599 5242880,
q 1096301 2621440,
q 438521 1048576,
q 68519 163840,
q 2192611 5242880,
q 1096307 2621440,
q 2192617 5242880,
q 109631 262144,
q 2192623 5242880,
q 1096313 2621440,
q 2192629 5242880,
q 274079 655360,
q 438527 1048576,
q 1096319 2621440,
q 2192641 5242880,
q 548161 1310720,
q 2192647 5242880,
q 219265 524288,
q 2192653 5242880,
q 137041 327680,
q 2192659 5242880,
q 1096331 2621440,
q 438533 1048576,
q 548167 1310720,
q 2192671 5242880,
q 1096337 2621440,
q 2192677 5242880,
q 54817 131072,
q 2192683 5242880,
q 1096343 2621440,
q 2192689 5242880,
q 548173 1310720,
q 438539 1048576,
q 1096349 2621440,
q 2192701 5242880,
q 34261 81920,
q 2192707 5242880,
q 219271 524288,
q 2192713 5242880,
q 548179 1310720,
q 2192719 5242880,
q 1096361 2621440,
q 438545 1048576,
q 274091 655360,
q 2192731 5242880,
q 1096367 2621440,
q 2192737 5242880,
q 109637 262144,
q 2192743 5242880,
q 1096373 2621440,
q 2192749 5242880,
q 137047 327680,
q 438551 1048576,
q 1096379 2621440,
q 2192761 5242880,
q 548191 1310720,
q 2192767 5242880,
q 219277 524288,
q 2192773 5242880,
q 274097 655360,
q 2192779 5242880,
q 1096391 2621440,
q 438557 1048576,
q 548197 1310720,
q 2192791 5242880,
q 1096397 2621440,
q 2192797 5242880,
q 13705 32768,
q 2192803 5242880,
q 1096403 2621440,
q 2192809 5242880,
q 548203 1310720,
q 438563 1048576,
q 1096409 2621440,
q 2192821 5242880,
q 274103 655360,
q 2192827 5242880,
q 219283 524288,
q 2192833 5242880,
q 548209 1310720,
q 2192839 5242880,
q 1096421 2621440,
q 438569 1048576,
q 137053 327680,
q 2192851 5242880,
q 1096427 2621440,
q 2192857 5242880,
q 109643 262144,
q 2192863 5242880,
q 1096433 2621440,
q 2192869 5242880,
q 274109 655360,
q 438575 1048576,
q 1096439 2621440,
q 2192881 5242880,
q 548221 1310720,
q 2192887 5242880,
q 219289 524288,
q 2192893 5242880,
q 4283 10240,
q 2192899 5242880,
q 1096451 2621440,
q 438581 1048576,
q 548227 1310720,
q 2192911 5242880,
q 1096457 2621440,
q 2192917 5242880,
q 54823 131072,
q 2192923 5242880,
q 1096463 2621440,
q 2192929 5242880,
q 548233 1310720,
q 438587 1048576,
q 1096469 2621440,
q 2192941 5242880,
q 137059 327680,
q 2192947 5242880,
q 219295 524288,
q 2192953 5242880,
q 548239 1310720,
q 2192959 5242880,
q 1096481 2621440,
q 438593 1048576,
q 274121 655360,
q 2192971 5242880,
q 1096487 2621440,
q 2192977 5242880,
q 109649 262144,
q 2192983 5242880,
q 1096493 2621440,
q 2192989 5242880,
q 68531 163840,
q 438599 1048576,
q 1096499 2621440,
q 2193001 5242880,
q 548251 1310720,
q 2193007 5242880,
q 219301 524288,
q 2193013 5242880,
q 274127 655360,
q 2193019 5242880,
q 1096511 2621440,
q 438605 1048576,
q 548257 1310720,
q 2193031 5242880,
q 1096517 2621440,
q 2193037 5242880,
q 27413 65536,
q 2193043 5242880,
q 1096523 2621440,
q 2193049 5242880,
q 548263 1310720,
q 438611 1048576,
q 1096529 2621440,
q 2193061 5242880,
q 274133 655360,
q 2193067 5242880,
q 219307 524288,
q 2193073 5242880,
q 548269 1310720,
q 2193079 5242880,
q 1096541 2621440,
q 438617 1048576,
q 34267 81920,
q 2193091 5242880,
q 1096547 2621440,
q 2193097 5242880,
q 109655 262144,
q 2193103 5242880,
q 1096553 2621440,
q 2193109 5242880,
q 274139 655360,
q 438623 1048576,
q 1096559 2621440,
q 2193121 5242880,
q 548281 1310720,
q 2193127 5242880,
q 219313 524288,
q 2193133 5242880,
q 137071 327680,
q 2193139 5242880,
q 1096571 2621440,
q 438629 1048576,
q 548287 1310720,
q 2193151 5242880,
q 1096577 2621440,
q 2193157 5242880,
q 54829 131072,
q 2193163 5242880,
q 1096583 2621440,
q 2193169 5242880,
q 548293 1310720,
q 438635 1048576,
q 1096589 2621440,
q 2193181 5242880,
q 68537 163840,
q 2193187 5242880,
q 219319 524288,
q 2193193 5242880,
q 548299 1310720,
q 2193199 5242880,
q 1096601 2621440,
q 438641 1048576,
q 274151 655360,
q 2193211 5242880,
q 1096607 2621440,
q 2193217 5242880,
q 109661 262144,
q 2193223 5242880,
q 1096613 2621440,
q 2193229 5242880,
q 137077 327680,
q 438647 1048576,
q 1096619 2621440,
q 2193241 5242880,
q 548311 1310720,
q 2193247 5242880,
q 219325 524288,
q 2193253 5242880,
q 274157 655360,
q 2193259 5242880,
q 1096631 2621440,
q 438653 1048576,
q 548317 1310720,
q 2193271 5242880,
q 1096637 2621440,
q 2193277 5242880,
q 3427 8192,
q 2193283 5242880,
q 1096643 2621440,
q 2193289 5242880
]
theorem cover13_ok :
checkCover (q 8030906143 10000000000) (q 2193289 5242880) (q 876775 2097152) cover13 = true := by
decide +kernel
theorem cover13_sound : ∀ σ ∈ Set.Icc (((q 876775 2097152) : ℚ) : ℝ) (((q 2193289 5242880) : ℚ) : ℝ),
rsF σ ≤ (((q 8030906143 10000000000) : ℚ) : ℝ) :=
checkCover_sound cover13_ok
end MaxLeafFormal.RSRate