MaxLeafFormal.RSCover14
Source file MaxLeafFormal/RSCover14.lean of the Lean project (how it is built).
import MaxLeafFormal.RSCheck
/-!
# RS closed-form rate: cover 1, chunk 14 (generated)
Generated by `scripts/export_rs_cover.py` (bisection as in
`ancillary/rs_closed_form_interval.py`,
SHA-256 `6ea21466e9a6f7153bafd754cbc8d0cdea78ef1c6f83ec9b25309d6aec87643e`).
500 intervals covering [2193289/5242880, 2194789/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 `2193289/5242880`. -/
def cover14 : List ℚ := [
q 548323 1310720,
q 438659 1048576,
q 1096649 2621440,
q 2193301 5242880,
q 274163 655360,
q 2193307 5242880,
q 219331 524288,
q 2193313 5242880,
q 548329 1310720,
q 2193319 5242880,
q 1096661 2621440,
q 438665 1048576,
q 137083 327680,
q 2193331 5242880,
q 1096667 2621440,
q 2193337 5242880,
q 109667 262144,
q 2193343 5242880,
q 1096673 2621440,
q 2193349 5242880,
q 274169 655360,
q 438671 1048576,
q 1096679 2621440,
q 2193361 5242880,
q 548341 1310720,
q 2193367 5242880,
q 219337 524288,
q 2193373 5242880,
q 68543 163840,
q 2193379 5242880,
q 1096691 2621440,
q 438677 1048576,
q 548347 1310720,
q 2193391 5242880,
q 1096697 2621440,
q 2193397 5242880,
q 54835 131072,
q 2193403 5242880,
q 1096703 2621440,
q 2193409 5242880,
q 548353 1310720,
q 438683 1048576,
q 1096709 2621440,
q 2193421 5242880,
q 137089 327680,
q 2193427 5242880,
q 219343 524288,
q 2193433 5242880,
q 548359 1310720,
q 2193439 5242880,
q 1096721 2621440,
q 438689 1048576,
q 274181 655360,
q 2193451 5242880,
q 1096727 2621440,
q 2193457 5242880,
q 109673 262144,
q 2193463 5242880,
q 1096733 2621440,
q 2193469 5242880,
q 34273 81920,
q 438695 1048576,
q 1096739 2621440,
q 2193481 5242880,
q 548371 1310720,
q 2193487 5242880,
q 219349 524288,
q 2193493 5242880,
q 274187 655360,
q 2193499 5242880,
q 1096751 2621440,
q 438701 1048576,
q 548377 1310720,
q 2193511 5242880,
q 1096757 2621440,
q 2193517 5242880,
q 27419 65536,
q 2193523 5242880,
q 1096763 2621440,
q 2193529 5242880,
q 548383 1310720,
q 438707 1048576,
q 1096769 2621440,
q 2193541 5242880,
q 274193 655360,
q 2193547 5242880,
q 219355 524288,
q 2193553 5242880,
q 548389 1310720,
q 2193559 5242880,
q 1096781 2621440,
q 438713 1048576,
q 68549 163840,
q 2193571 5242880,
q 1096787 2621440,
q 2193577 5242880,
q 109679 262144,
q 2193583 5242880,
q 1096793 2621440,
q 2193589 5242880,
q 274199 655360,
q 438719 1048576,
q 1096799 2621440,
q 2193601 5242880,
q 548401 1310720,
q 2193607 5242880,
q 219361 524288,
q 2193613 5242880,
q 137101 327680,
q 2193619 5242880,
q 1096811 2621440,
q 438725 1048576,
q 548407 1310720,
q 2193631 5242880,
q 1096817 2621440,
q 2193637 5242880,
q 54841 131072,
q 2193643 5242880,
q 1096823 2621440,
q 2193649 5242880,
q 548413 1310720,
q 438731 1048576,
q 1096829 2621440,
q 2193661 5242880,
q 8569 20480,
q 2193667 5242880,
q 219367 524288,
q 2193673 5242880,
q 548419 1310720,
q 2193679 5242880,
q 1096841 2621440,
q 438737 1048576,
q 274211 655360,
q 2193691 5242880,
q 1096847 2621440,
q 2193697 5242880,
q 109685 262144,
q 2193703 5242880,
q 1096853 2621440,
q 2193709 5242880,
q 137107 327680,
q 438743 1048576,
q 1096859 2621440,
q 2193721 5242880,
q 548431 1310720,
q 2193727 5242880,
q 219373 524288,
q 2193733 5242880,
q 274217 655360,
q 2193739 5242880,
q 1096871 2621440,
q 438749 1048576,
q 548437 1310720,
q 2193751 5242880,
q 1096877 2621440,
q 2193757 5242880,
q 13711 32768,
q 2193763 5242880,
q 1096883 2621440,
q 2193769 5242880,
q 548443 1310720,
q 438755 1048576,
q 1096889 2621440,
q 2193781 5242880,
q 274223 655360,
q 2193787 5242880,
q 219379 524288,
q 2193793 5242880,
q 548449 1310720,
q 2193799 5242880,
q 1096901 2621440,
q 438761 1048576,
q 137113 327680,
q 2193811 5242880,
q 1096907 2621440,
q 2193817 5242880,
q 109691 262144,
q 2193823 5242880,
q 1096913 2621440,
q 2193829 5242880,
q 274229 655360,
q 438767 1048576,
q 1096919 2621440,
q 2193841 5242880,
q 548461 1310720,
q 2193847 5242880,
q 219385 524288,
q 2193853 5242880,
q 34279 81920,
q 2193859 5242880,
q 1096931 2621440,
q 438773 1048576,
q 548467 1310720,
q 2193871 5242880,
q 1096937 2621440,
q 2193877 5242880,
q 54847 131072,
q 2193883 5242880,
q 1096943 2621440,
q 2193889 5242880,
q 548473 1310720,
q 438779 1048576,
q 1096949 2621440,
q 2193901 5242880,
q 137119 327680,
q 2193907 5242880,
q 219391 524288,
q 2193913 5242880,
q 548479 1310720,
q 2193919 5242880,
q 1096961 2621440,
q 438785 1048576,
q 274241 655360,
q 2193931 5242880,
q 1096967 2621440,
q 2193937 5242880,
q 109697 262144,
q 2193943 5242880,
q 1096973 2621440,
q 2193949 5242880,
q 68561 163840,
q 438791 1048576,
q 1096979 2621440,
q 2193961 5242880,
q 548491 1310720,
q 2193967 5242880,
q 219397 524288,
q 2193973 5242880,
q 274247 655360,
q 2193979 5242880,
q 1096991 2621440,
q 438797 1048576,
q 548497 1310720,
q 2193991 5242880,
q 1096997 2621440,
q 2193997 5242880,
q 27425 65536,
q 2194003 5242880,
q 1097003 2621440,
q 2194009 5242880,
q 548503 1310720,
q 438803 1048576,
q 1097009 2621440,
q 2194021 5242880,
q 274253 655360,
q 2194027 5242880,
q 219403 524288,
q 2194033 5242880,
q 548509 1310720,
q 2194039 5242880,
q 1097021 2621440,
q 438809 1048576,
q 17141 40960,
q 2194051 5242880,
q 1097027 2621440,
q 2194057 5242880,
q 109703 262144,
q 2194063 5242880,
q 1097033 2621440,
q 2194069 5242880,
q 274259 655360,
q 438815 1048576,
q 1097039 2621440,
q 2194081 5242880,
q 548521 1310720,
q 2194087 5242880,
q 219409 524288,
q 2194093 5242880,
q 137131 327680,
q 2194099 5242880,
q 1097051 2621440,
q 438821 1048576,
q 548527 1310720,
q 2194111 5242880,
q 1097057 2621440,
q 2194117 5242880,
q 54853 131072,
q 2194123 5242880,
q 1097063 2621440,
q 2194129 5242880,
q 548533 1310720,
q 438827 1048576,
q 1097069 2621440,
q 2194141 5242880,
q 68567 163840,
q 2194147 5242880,
q 219415 524288,
q 2194153 5242880,
q 548539 1310720,
q 2194159 5242880,
q 1097081 2621440,
q 438833 1048576,
q 274271 655360,
q 2194171 5242880,
q 1097087 2621440,
q 2194177 5242880,
q 109709 262144,
q 2194183 5242880,
q 1097093 2621440,
q 2194189 5242880,
q 137137 327680,
q 438839 1048576,
q 1097099 2621440,
q 2194201 5242880,
q 548551 1310720,
q 2194207 5242880,
q 219421 524288,
q 2194213 5242880,
q 274277 655360,
q 2194219 5242880,
q 1097111 2621440,
q 438845 1048576,
q 548557 1310720,
q 2194231 5242880,
q 1097117 2621440,
q 2194237 5242880,
q 6857 16384,
q 2194243 5242880,
q 1097123 2621440,
q 2194249 5242880,
q 548563 1310720,
q 438851 1048576,
q 1097129 2621440,
q 2194261 5242880,
q 274283 655360,
q 2194267 5242880,
q 219427 524288,
q 2194273 5242880,
q 548569 1310720,
q 2194279 5242880,
q 1097141 2621440,
q 438857 1048576,
q 137143 327680,
q 2194291 5242880,
q 1097147 2621440,
q 2194297 5242880,
q 109715 262144,
q 2194303 5242880,
q 1097153 2621440,
q 2194309 5242880,
q 274289 655360,
q 438863 1048576,
q 1097159 2621440,
q 2194321 5242880,
q 548581 1310720,
q 2194327 5242880,
q 219433 524288,
q 2194333 5242880,
q 68573 163840,
q 2194339 5242880,
q 1097171 2621440,
q 438869 1048576,
q 548587 1310720,
q 2194351 5242880,
q 1097177 2621440,
q 2194357 5242880,
q 54859 131072,
q 2194363 5242880,
q 1097183 2621440,
q 2194369 5242880,
q 548593 1310720,
q 438875 1048576,
q 1097189 2621440,
q 2194381 5242880,
q 137149 327680,
q 2194387 5242880,
q 219439 524288,
q 2194393 5242880,
q 548599 1310720,
q 2194399 5242880,
q 1097201 2621440,
q 438881 1048576,
q 274301 655360,
q 2194411 5242880,
q 1097207 2621440,
q 2194417 5242880,
q 109721 262144,
q 2194423 5242880,
q 1097213 2621440,
q 2194429 5242880,
q 2143 5120,
q 438887 1048576,
q 1097219 2621440,
q 2194441 5242880,
q 548611 1310720,
q 2194447 5242880,
q 219445 524288,
q 2194453 5242880,
q 274307 655360,
q 2194459 5242880,
q 1097231 2621440,
q 438893 1048576,
q 548617 1310720,
q 2194471 5242880,
q 1097237 2621440,
q 2194477 5242880,
q 27431 65536,
q 2194483 5242880,
q 1097243 2621440,
q 2194489 5242880,
q 548623 1310720,
q 438899 1048576,
q 1097249 2621440,
q 2194501 5242880,
q 274313 655360,
q 2194507 5242880,
q 219451 524288,
q 2194513 5242880,
q 548629 1310720,
q 2194519 5242880,
q 1097261 2621440,
q 438905 1048576,
q 68579 163840,
q 2194531 5242880,
q 1097267 2621440,
q 2194537 5242880,
q 109727 262144,
q 2194543 5242880,
q 1097273 2621440,
q 2194549 5242880,
q 274319 655360,
q 438911 1048576,
q 1097279 2621440,
q 2194561 5242880,
q 548641 1310720,
q 2194567 5242880,
q 219457 524288,
q 2194573 5242880,
q 137161 327680,
q 2194579 5242880,
q 1097291 2621440,
q 438917 1048576,
q 548647 1310720,
q 2194591 5242880,
q 1097297 2621440,
q 2194597 5242880,
q 54865 131072,
q 2194603 5242880,
q 1097303 2621440,
q 2194609 5242880,
q 548653 1310720,
q 438923 1048576,
q 1097309 2621440,
q 2194621 5242880,
q 34291 81920,
q 2194627 5242880,
q 219463 524288,
q 2194633 5242880,
q 548659 1310720,
q 2194639 5242880,
q 1097321 2621440,
q 438929 1048576,
q 274331 655360,
q 2194651 5242880,
q 1097327 2621440,
q 2194657 5242880,
q 109733 262144,
q 2194663 5242880,
q 1097333 2621440,
q 2194669 5242880,
q 137167 327680,
q 438935 1048576,
q 1097339 2621440,
q 2194681 5242880,
q 548671 1310720,
q 2194687 5242880,
q 219469 524288,
q 2194693 5242880,
q 274337 655360,
q 2194699 5242880,
q 1097351 2621440,
q 438941 1048576,
q 548677 1310720,
q 2194711 5242880,
q 1097357 2621440,
q 2194717 5242880,
q 13717 32768,
q 2194723 5242880,
q 1097363 2621440,
q 2194729 5242880,
q 548683 1310720,
q 438947 1048576,
q 1097369 2621440,
q 2194741 5242880,
q 274343 655360,
q 2194747 5242880,
q 219475 524288,
q 2194753 5242880,
q 548689 1310720,
q 2194759 5242880,
q 1097381 2621440,
q 438953 1048576,
q 137173 327680,
q 2194771 5242880,
q 1097387 2621440,
q 2194777 5242880,
q 109739 262144,
q 2194783 5242880,
q 1097393 2621440,
q 2194789 5242880
]
theorem cover14_ok :
checkCover (q 8030906143 10000000000) (q 2194789 5242880) (q 2193289 5242880) cover14 = true := by
decide +kernel
theorem cover14_sound : ∀ σ ∈ Set.Icc (((q 2193289 5242880) : ℚ) : ℝ) (((q 2194789 5242880) : ℚ) : ℝ),
rsF σ ≤ (((q 8030906143 10000000000) : ℚ) : ℝ) :=
checkCover_sound cover14_ok
end MaxLeafFormal.RSRate