MaxLeafFormal.RSCover10
Source file MaxLeafFormal/RSCover10.lean of the Lean project (how it is built).
import MaxLeafFormal.RSCheck
/-!
# RS closed-form rate: cover 1, chunk 10 (generated)
Generated by `scripts/export_rs_cover.py` (bisection as in
`ancillary/rs_closed_form_interval.py`,
SHA-256 `6ea21466e9a6f7153bafd754cbc8d0cdea78ef1c6f83ec9b25309d6aec87643e`).
500 intervals covering [875875/2097152, 876175/2097152] 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 `875875/2097152`. -/
def cover10 : List ℚ := [
q 2189689 5242880,
q 4379381 10485760,
q 547423 1310720,
q 4379387 10485760,
q 437939 1048576,
q 4379393 10485760,
q 1094849 2621440,
q 4379399 10485760,
q 2189701 5242880,
q 875881 2097152,
q 273713 655360,
q 4379411 10485760,
q 2189707 5242880,
q 4379417 10485760,
q 218971 524288,
q 4379423 10485760,
q 2189713 5242880,
q 4379429 10485760,
q 547429 1310720,
q 875887 2097152,
q 2189719 5242880,
q 4379441 10485760,
q 1094861 2621440,
q 4379447 10485760,
q 437945 1048576,
q 4379453 10485760,
q 68429 163840,
q 4379459 10485760,
q 2189731 5242880,
q 875893 2097152,
q 1094867 2621440,
q 4379471 10485760,
q 2189737 5242880,
q 4379477 10485760,
q 109487 262144,
q 4379483 10485760,
q 2189743 5242880,
q 4379489 10485760,
q 1094873 2621440,
q 875899 2097152,
q 2189749 5242880,
q 4379501 10485760,
q 273719 655360,
q 4379507 10485760,
q 437951 1048576,
q 4379513 10485760,
q 1094879 2621440,
q 4379519 10485760,
q 2189761 5242880,
q 875905 2097152,
q 547441 1310720,
q 4379531 10485760,
q 2189767 5242880,
q 4379537 10485760,
q 218977 524288,
q 4379543 10485760,
q 2189773 5242880,
q 4379549 10485760,
q 136861 327680,
q 875911 2097152,
q 2189779 5242880,
q 4379561 10485760,
q 1094891 2621440,
q 4379567 10485760,
q 437957 1048576,
q 4379573 10485760,
q 547447 1310720,
q 4379579 10485760,
q 2189791 5242880,
q 875917 2097152,
q 1094897 2621440,
q 4379591 10485760,
q 2189797 5242880,
q 4379597 10485760,
q 54745 131072,
q 4379603 10485760,
q 2189803 5242880,
q 4379609 10485760,
q 1094903 2621440,
q 875923 2097152,
q 2189809 5242880,
q 4379621 10485760,
q 547453 1310720,
q 4379627 10485760,
q 437963 1048576,
q 4379633 10485760,
q 1094909 2621440,
q 4379639 10485760,
q 2189821 5242880,
q 875929 2097152,
q 4277 10240,
q 4379651 10485760,
q 2189827 5242880,
q 4379657 10485760,
q 218983 524288,
q 4379663 10485760,
q 2189833 5242880,
q 4379669 10485760,
q 547459 1310720,
q 875935 2097152,
q 2189839 5242880,
q 4379681 10485760,
q 1094921 2621440,
q 4379687 10485760,
q 437969 1048576,
q 4379693 10485760,
q 273731 655360,
q 4379699 10485760,
q 2189851 5242880,
q 875941 2097152,
q 1094927 2621440,
q 4379711 10485760,
q 2189857 5242880,
q 4379717 10485760,
q 109493 262144,
q 4379723 10485760,
q 2189863 5242880,
q 4379729 10485760,
q 1094933 2621440,
q 875947 2097152,
q 2189869 5242880,
q 4379741 10485760,
q 136867 327680,
q 4379747 10485760,
q 437975 1048576,
q 4379753 10485760,
q 1094939 2621440,
q 4379759 10485760,
q 2189881 5242880,
q 875953 2097152,
q 547471 1310720,
q 4379771 10485760,
q 2189887 5242880,
q 4379777 10485760,
q 218989 524288,
q 4379783 10485760,
q 2189893 5242880,
q 4379789 10485760,
q 273737 655360,
q 875959 2097152,
q 2189899 5242880,
q 4379801 10485760,
q 1094951 2621440,
q 4379807 10485760,
q 437981 1048576,
q 4379813 10485760,
q 547477 1310720,
q 4379819 10485760,
q 2189911 5242880,
q 875965 2097152,
q 1094957 2621440,
q 4379831 10485760,
q 2189917 5242880,
q 4379837 10485760,
q 13687 32768,
q 4379843 10485760,
q 2189923 5242880,
q 4379849 10485760,
q 1094963 2621440,
q 875971 2097152,
q 2189929 5242880,
q 4379861 10485760,
q 547483 1310720,
q 4379867 10485760,
q 437987 1048576,
q 4379873 10485760,
q 1094969 2621440,
q 4379879 10485760,
q 2189941 5242880,
q 875977 2097152,
q 273743 655360,
q 4379891 10485760,
q 2189947 5242880,
q 4379897 10485760,
q 218995 524288,
q 4379903 10485760,
q 2189953 5242880,
q 4379909 10485760,
q 547489 1310720,
q 875983 2097152,
q 2189959 5242880,
q 4379921 10485760,
q 1094981 2621440,
q 4379927 10485760,
q 437993 1048576,
q 4379933 10485760,
q 136873 327680,
q 4379939 10485760,
q 2189971 5242880,
q 875989 2097152,
q 1094987 2621440,
q 4379951 10485760,
q 2189977 5242880,
q 4379957 10485760,
q 109499 262144,
q 4379963 10485760,
q 2189983 5242880,
q 4379969 10485760,
q 1094993 2621440,
q 875995 2097152,
q 2189989 5242880,
q 4379981 10485760,
q 273749 655360,
q 4379987 10485760,
q 437999 1048576,
q 4379993 10485760,
q 1094999 2621440,
q 4379999 10485760,
q 2190001 5242880,
q 876001 2097152,
q 547501 1310720,
q 4380011 10485760,
q 2190007 5242880,
q 4380017 10485760,
q 219001 524288,
q 4380023 10485760,
q 2190013 5242880,
q 4380029 10485760,
q 34219 81920,
q 876007 2097152,
q 2190019 5242880,
q 4380041 10485760,
q 1095011 2621440,
q 4380047 10485760,
q 438005 1048576,
q 4380053 10485760,
q 547507 1310720,
q 4380059 10485760,
q 2190031 5242880,
q 876013 2097152,
q 1095017 2621440,
q 4380071 10485760,
q 2190037 5242880,
q 4380077 10485760,
q 54751 131072,
q 4380083 10485760,
q 2190043 5242880,
q 4380089 10485760,
q 1095023 2621440,
q 876019 2097152,
q 2190049 5242880,
q 4380101 10485760,
q 547513 1310720,
q 4380107 10485760,
q 438011 1048576,
q 4380113 10485760,
q 1095029 2621440,
q 4380119 10485760,
q 2190061 5242880,
q 876025 2097152,
q 136879 327680,
q 4380131 10485760,
q 2190067 5242880,
q 4380137 10485760,
q 219007 524288,
q 4380143 10485760,
q 2190073 5242880,
q 4380149 10485760,
q 547519 1310720,
q 876031 2097152,
q 2190079 5242880,
q 4380161 10485760,
q 1095041 2621440,
q 4380167 10485760,
q 438017 1048576,
q 4380173 10485760,
q 273761 655360,
q 4380179 10485760,
q 2190091 5242880,
q 876037 2097152,
q 1095047 2621440,
q 4380191 10485760,
q 2190097 5242880,
q 4380197 10485760,
q 109505 262144,
q 4380203 10485760,
q 2190103 5242880,
q 4380209 10485760,
q 1095053 2621440,
q 876043 2097152,
q 2190109 5242880,
q 4380221 10485760,
q 68441 163840,
q 4380227 10485760,
q 438023 1048576,
q 4380233 10485760,
q 1095059 2621440,
q 4380239 10485760,
q 2190121 5242880,
q 876049 2097152,
q 547531 1310720,
q 4380251 10485760,
q 2190127 5242880,
q 4380257 10485760,
q 219013 524288,
q 4380263 10485760,
q 2190133 5242880,
q 4380269 10485760,
q 273767 655360,
q 876055 2097152,
q 2190139 5242880,
q 4380281 10485760,
q 1095071 2621440,
q 4380287 10485760,
q 438029 1048576,
q 4380293 10485760,
q 547537 1310720,
q 4380299 10485760,
q 2190151 5242880,
q 876061 2097152,
q 1095077 2621440,
q 4380311 10485760,
q 2190157 5242880,
q 4380317 10485760,
q 27377 65536,
q 4380323 10485760,
q 2190163 5242880,
q 4380329 10485760,
q 1095083 2621440,
q 876067 2097152,
q 2190169 5242880,
q 4380341 10485760,
q 547543 1310720,
q 4380347 10485760,
q 438035 1048576,
q 4380353 10485760,
q 1095089 2621440,
q 4380359 10485760,
q 2190181 5242880,
q 876073 2097152,
q 273773 655360,
q 4380371 10485760,
q 2190187 5242880,
q 4380377 10485760,
q 219019 524288,
q 4380383 10485760,
q 2190193 5242880,
q 4380389 10485760,
q 547549 1310720,
q 876079 2097152,
q 2190199 5242880,
q 4380401 10485760,
q 1095101 2621440,
q 4380407 10485760,
q 438041 1048576,
q 4380413 10485760,
q 17111 40960,
q 4380419 10485760,
q 2190211 5242880,
q 876085 2097152,
q 1095107 2621440,
q 4380431 10485760,
q 2190217 5242880,
q 4380437 10485760,
q 109511 262144,
q 4380443 10485760,
q 2190223 5242880,
q 4380449 10485760,
q 1095113 2621440,
q 876091 2097152,
q 2190229 5242880,
q 4380461 10485760,
q 273779 655360,
q 4380467 10485760,
q 438047 1048576,
q 4380473 10485760,
q 1095119 2621440,
q 4380479 10485760,
q 2190241 5242880,
q 876097 2097152,
q 547561 1310720,
q 4380491 10485760,
q 2190247 5242880,
q 4380497 10485760,
q 219025 524288,
q 4380503 10485760,
q 2190253 5242880,
q 4380509 10485760,
q 136891 327680,
q 876103 2097152,
q 2190259 5242880,
q 4380521 10485760,
q 1095131 2621440,
q 4380527 10485760,
q 438053 1048576,
q 4380533 10485760,
q 547567 1310720,
q 4380539 10485760,
q 2190271 5242880,
q 876109 2097152,
q 1095137 2621440,
q 4380551 10485760,
q 2190277 5242880,
q 4380557 10485760,
q 54757 131072,
q 4380563 10485760,
q 2190283 5242880,
q 4380569 10485760,
q 1095143 2621440,
q 876115 2097152,
q 2190289 5242880,
q 4380581 10485760,
q 547573 1310720,
q 4380587 10485760,
q 438059 1048576,
q 4380593 10485760,
q 1095149 2621440,
q 4380599 10485760,
q 2190301 5242880,
q 876121 2097152,
q 68447 163840,
q 4380611 10485760,
q 2190307 5242880,
q 4380617 10485760,
q 219031 524288,
q 4380623 10485760,
q 2190313 5242880,
q 4380629 10485760,
q 547579 1310720,
q 876127 2097152,
q 2190319 5242880,
q 4380641 10485760,
q 1095161 2621440,
q 4380647 10485760,
q 438065 1048576,
q 4380653 10485760,
q 273791 655360,
q 4380659 10485760,
q 2190331 5242880,
q 876133 2097152,
q 1095167 2621440,
q 4380671 10485760,
q 2190337 5242880,
q 4380677 10485760,
q 109517 262144,
q 4380683 10485760,
q 2190343 5242880,
q 4380689 10485760,
q 1095173 2621440,
q 876139 2097152,
q 2190349 5242880,
q 4380701 10485760,
q 136897 327680,
q 4380707 10485760,
q 438071 1048576,
q 4380713 10485760,
q 1095179 2621440,
q 4380719 10485760,
q 2190361 5242880,
q 876145 2097152,
q 547591 1310720,
q 4380731 10485760,
q 2190367 5242880,
q 4380737 10485760,
q 219037 524288,
q 4380743 10485760,
q 2190373 5242880,
q 4380749 10485760,
q 273797 655360,
q 876151 2097152,
q 2190379 5242880,
q 4380761 10485760,
q 1095191 2621440,
q 4380767 10485760,
q 438077 1048576,
q 4380773 10485760,
q 547597 1310720,
q 4380779 10485760,
q 2190391 5242880,
q 876157 2097152,
q 1095197 2621440,
q 4380791 10485760,
q 2190397 5242880,
q 4380797 10485760,
q 6845 16384,
q 4380803 10485760,
q 2190403 5242880,
q 4380809 10485760,
q 1095203 2621440,
q 876163 2097152,
q 2190409 5242880,
q 4380821 10485760,
q 547603 1310720,
q 4380827 10485760,
q 438083 1048576,
q 4380833 10485760,
q 1095209 2621440,
q 4380839 10485760,
q 2190421 5242880,
q 876169 2097152,
q 273803 655360,
q 4380851 10485760,
q 2190427 5242880,
q 4380857 10485760,
q 219043 524288,
q 4380863 10485760,
q 2190433 5242880,
q 4380869 10485760,
q 547609 1310720,
q 876175 2097152
]
theorem cover10_ok :
checkCover (q 8030906143 10000000000) (q 876175 2097152) (q 875875 2097152) cover10 = true := by
decide +kernel
theorem cover10_sound : ∀ σ ∈ Set.Icc (((q 875875 2097152) : ℚ) : ℝ) (((q 876175 2097152) : ℚ) : ℝ),
rsF σ ≤ (((q 8030906143 10000000000) : ℚ) : ℝ) :=
checkCover_sound cover10_ok
end MaxLeafFormal.RSRate