MaxLeafFormal.RSCover7
Source file MaxLeafFormal/RSCover7.lean of the Lean project (how it is built).
import MaxLeafFormal.RSCheck
/-!
# RS closed-form rate: cover 1, chunk 7 (generated)
Generated by `scripts/export_rs_cover.py` (bisection as in
`ancillary/rs_closed_form_interval.py`,
SHA-256 `6ea21466e9a6f7153bafd754cbc8d0cdea78ef1c6f83ec9b25309d6aec87643e`).
500 intervals covering [874975/2097152, 875275/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 `874975/2097152`. -/
def cover7 : List ℚ := [
q 2187439 5242880,
q 4374881 10485760,
q 1093721 2621440,
q 4374887 10485760,
q 437489 1048576,
q 4374893 10485760,
q 273431 655360,
q 4374899 10485760,
q 2187451 5242880,
q 874981 2097152,
q 1093727 2621440,
q 4374911 10485760,
q 2187457 5242880,
q 4374917 10485760,
q 109373 262144,
q 4374923 10485760,
q 2187463 5242880,
q 4374929 10485760,
q 1093733 2621440,
q 874987 2097152,
q 2187469 5242880,
q 4374941 10485760,
q 136717 327680,
q 4374947 10485760,
q 437495 1048576,
q 4374953 10485760,
q 1093739 2621440,
q 4374959 10485760,
q 2187481 5242880,
q 874993 2097152,
q 546871 1310720,
q 4374971 10485760,
q 2187487 5242880,
q 4374977 10485760,
q 218749 524288,
q 4374983 10485760,
q 2187493 5242880,
q 4374989 10485760,
q 273437 655360,
q 874999 2097152,
q 2187499 5242880,
q 4375001 10485760,
q 1093751 2621440,
q 4375007 10485760,
q 437501 1048576,
q 4375013 10485760,
q 546877 1310720,
q 4375019 10485760,
q 2187511 5242880,
q 875005 2097152,
q 1093757 2621440,
q 4375031 10485760,
q 2187517 5242880,
q 4375037 10485760,
q 1709 4096,
q 4375043 10485760,
q 2187523 5242880,
q 4375049 10485760,
q 1093763 2621440,
q 875011 2097152,
q 2187529 5242880,
q 4375061 10485760,
q 546883 1310720,
q 4375067 10485760,
q 437507 1048576,
q 4375073 10485760,
q 1093769 2621440,
q 4375079 10485760,
q 2187541 5242880,
q 875017 2097152,
q 273443 655360,
q 4375091 10485760,
q 2187547 5242880,
q 4375097 10485760,
q 218755 524288,
q 4375103 10485760,
q 2187553 5242880,
q 4375109 10485760,
q 546889 1310720,
q 875023 2097152,
q 2187559 5242880,
q 4375121 10485760,
q 1093781 2621440,
q 4375127 10485760,
q 437513 1048576,
q 4375133 10485760,
q 136723 327680,
q 4375139 10485760,
q 2187571 5242880,
q 875029 2097152,
q 1093787 2621440,
q 4375151 10485760,
q 2187577 5242880,
q 4375157 10485760,
q 109379 262144,
q 4375163 10485760,
q 2187583 5242880,
q 4375169 10485760,
q 1093793 2621440,
q 875035 2097152,
q 2187589 5242880,
q 4375181 10485760,
q 273449 655360,
q 4375187 10485760,
q 437519 1048576,
q 4375193 10485760,
q 1093799 2621440,
q 4375199 10485760,
q 2187601 5242880,
q 875041 2097152,
q 546901 1310720,
q 4375211 10485760,
q 2187607 5242880,
q 4375217 10485760,
q 218761 524288,
q 4375223 10485760,
q 2187613 5242880,
q 4375229 10485760,
q 68363 163840,
q 875047 2097152,
q 2187619 5242880,
q 4375241 10485760,
q 1093811 2621440,
q 4375247 10485760,
q 437525 1048576,
q 4375253 10485760,
q 546907 1310720,
q 4375259 10485760,
q 2187631 5242880,
q 875053 2097152,
q 1093817 2621440,
q 4375271 10485760,
q 2187637 5242880,
q 4375277 10485760,
q 54691 131072,
q 4375283 10485760,
q 2187643 5242880,
q 4375289 10485760,
q 1093823 2621440,
q 875059 2097152,
q 2187649 5242880,
q 4375301 10485760,
q 546913 1310720,
q 4375307 10485760,
q 437531 1048576,
q 4375313 10485760,
q 1093829 2621440,
q 4375319 10485760,
q 2187661 5242880,
q 875065 2097152,
q 136729 327680,
q 4375331 10485760,
q 2187667 5242880,
q 4375337 10485760,
q 218767 524288,
q 4375343 10485760,
q 2187673 5242880,
q 4375349 10485760,
q 546919 1310720,
q 875071 2097152,
q 2187679 5242880,
q 4375361 10485760,
q 1093841 2621440,
q 4375367 10485760,
q 437537 1048576,
q 4375373 10485760,
q 273461 655360,
q 4375379 10485760,
q 2187691 5242880,
q 875077 2097152,
q 1093847 2621440,
q 4375391 10485760,
q 2187697 5242880,
q 4375397 10485760,
q 109385 262144,
q 4375403 10485760,
q 2187703 5242880,
q 4375409 10485760,
q 1093853 2621440,
q 875083 2097152,
q 2187709 5242880,
q 4375421 10485760,
q 34183 81920,
q 4375427 10485760,
q 437543 1048576,
q 4375433 10485760,
q 1093859 2621440,
q 4375439 10485760,
q 2187721 5242880,
q 875089 2097152,
q 546931 1310720,
q 4375451 10485760,
q 2187727 5242880,
q 4375457 10485760,
q 218773 524288,
q 4375463 10485760,
q 2187733 5242880,
q 4375469 10485760,
q 273467 655360,
q 875095 2097152,
q 2187739 5242880,
q 4375481 10485760,
q 1093871 2621440,
q 4375487 10485760,
q 437549 1048576,
q 4375493 10485760,
q 546937 1310720,
q 4375499 10485760,
q 2187751 5242880,
q 875101 2097152,
q 1093877 2621440,
q 4375511 10485760,
q 2187757 5242880,
q 4375517 10485760,
q 27347 65536,
q 4375523 10485760,
q 2187763 5242880,
q 4375529 10485760,
q 1093883 2621440,
q 875107 2097152,
q 2187769 5242880,
q 4375541 10485760,
q 546943 1310720,
q 4375547 10485760,
q 437555 1048576,
q 4375553 10485760,
q 1093889 2621440,
q 4375559 10485760,
q 2187781 5242880,
q 875113 2097152,
q 273473 655360,
q 4375571 10485760,
q 2187787 5242880,
q 4375577 10485760,
q 218779 524288,
q 4375583 10485760,
q 2187793 5242880,
q 4375589 10485760,
q 546949 1310720,
q 875119 2097152,
q 2187799 5242880,
q 4375601 10485760,
q 1093901 2621440,
q 4375607 10485760,
q 437561 1048576,
q 4375613 10485760,
q 68369 163840,
q 4375619 10485760,
q 2187811 5242880,
q 875125 2097152,
q 1093907 2621440,
q 4375631 10485760,
q 2187817 5242880,
q 4375637 10485760,
q 109391 262144,
q 4375643 10485760,
q 2187823 5242880,
q 4375649 10485760,
q 1093913 2621440,
q 875131 2097152,
q 2187829 5242880,
q 4375661 10485760,
q 273479 655360,
q 4375667 10485760,
q 437567 1048576,
q 4375673 10485760,
q 1093919 2621440,
q 4375679 10485760,
q 2187841 5242880,
q 875137 2097152,
q 546961 1310720,
q 4375691 10485760,
q 2187847 5242880,
q 4375697 10485760,
q 218785 524288,
q 4375703 10485760,
q 2187853 5242880,
q 4375709 10485760,
q 136741 327680,
q 875143 2097152,
q 2187859 5242880,
q 4375721 10485760,
q 1093931 2621440,
q 4375727 10485760,
q 437573 1048576,
q 4375733 10485760,
q 546967 1310720,
q 4375739 10485760,
q 2187871 5242880,
q 875149 2097152,
q 1093937 2621440,
q 4375751 10485760,
q 2187877 5242880,
q 4375757 10485760,
q 54697 131072,
q 4375763 10485760,
q 2187883 5242880,
q 4375769 10485760,
q 1093943 2621440,
q 875155 2097152,
q 2187889 5242880,
q 4375781 10485760,
q 546973 1310720,
q 4375787 10485760,
q 437579 1048576,
q 4375793 10485760,
q 1093949 2621440,
q 4375799 10485760,
q 2187901 5242880,
q 875161 2097152,
q 17093 40960,
q 4375811 10485760,
q 2187907 5242880,
q 4375817 10485760,
q 218791 524288,
q 4375823 10485760,
q 2187913 5242880,
q 4375829 10485760,
q 546979 1310720,
q 875167 2097152,
q 2187919 5242880,
q 4375841 10485760,
q 1093961 2621440,
q 4375847 10485760,
q 437585 1048576,
q 4375853 10485760,
q 273491 655360,
q 4375859 10485760,
q 2187931 5242880,
q 875173 2097152,
q 1093967 2621440,
q 4375871 10485760,
q 2187937 5242880,
q 4375877 10485760,
q 109397 262144,
q 4375883 10485760,
q 2187943 5242880,
q 4375889 10485760,
q 1093973 2621440,
q 875179 2097152,
q 2187949 5242880,
q 4375901 10485760,
q 136747 327680,
q 4375907 10485760,
q 437591 1048576,
q 4375913 10485760,
q 1093979 2621440,
q 4375919 10485760,
q 2187961 5242880,
q 875185 2097152,
q 546991 1310720,
q 4375931 10485760,
q 2187967 5242880,
q 4375937 10485760,
q 218797 524288,
q 4375943 10485760,
q 2187973 5242880,
q 4375949 10485760,
q 273497 655360,
q 875191 2097152,
q 2187979 5242880,
q 4375961 10485760,
q 1093991 2621440,
q 4375967 10485760,
q 437597 1048576,
q 4375973 10485760,
q 546997 1310720,
q 4375979 10485760,
q 2187991 5242880,
q 875197 2097152,
q 1093997 2621440,
q 4375991 10485760,
q 2187997 5242880,
q 4375997 10485760,
q 13675 32768,
q 4376003 10485760,
q 2188003 5242880,
q 4376009 10485760,
q 1094003 2621440,
q 875203 2097152,
q 2188009 5242880,
q 4376021 10485760,
q 547003 1310720,
q 4376027 10485760,
q 437603 1048576,
q 4376033 10485760,
q 1094009 2621440,
q 4376039 10485760,
q 2188021 5242880,
q 875209 2097152,
q 273503 655360,
q 4376051 10485760,
q 2188027 5242880,
q 4376057 10485760,
q 218803 524288,
q 4376063 10485760,
q 2188033 5242880,
q 4376069 10485760,
q 547009 1310720,
q 875215 2097152,
q 2188039 5242880,
q 4376081 10485760,
q 1094021 2621440,
q 4376087 10485760,
q 437609 1048576,
q 4376093 10485760,
q 136753 327680,
q 4376099 10485760,
q 2188051 5242880,
q 875221 2097152,
q 1094027 2621440,
q 4376111 10485760,
q 2188057 5242880,
q 4376117 10485760,
q 109403 262144,
q 4376123 10485760,
q 2188063 5242880,
q 4376129 10485760,
q 1094033 2621440,
q 875227 2097152,
q 2188069 5242880,
q 4376141 10485760,
q 273509 655360,
q 4376147 10485760,
q 437615 1048576,
q 4376153 10485760,
q 1094039 2621440,
q 4376159 10485760,
q 2188081 5242880,
q 875233 2097152,
q 547021 1310720,
q 4376171 10485760,
q 2188087 5242880,
q 4376177 10485760,
q 218809 524288,
q 4376183 10485760,
q 2188093 5242880,
q 4376189 10485760,
q 34189 81920,
q 875239 2097152,
q 2188099 5242880,
q 4376201 10485760,
q 1094051 2621440,
q 4376207 10485760,
q 437621 1048576,
q 4376213 10485760,
q 547027 1310720,
q 4376219 10485760,
q 2188111 5242880,
q 875245 2097152,
q 1094057 2621440,
q 4376231 10485760,
q 2188117 5242880,
q 4376237 10485760,
q 54703 131072,
q 4376243 10485760,
q 2188123 5242880,
q 4376249 10485760,
q 1094063 2621440,
q 875251 2097152,
q 2188129 5242880,
q 4376261 10485760,
q 547033 1310720,
q 4376267 10485760,
q 437627 1048576,
q 4376273 10485760,
q 1094069 2621440,
q 4376279 10485760,
q 2188141 5242880,
q 875257 2097152,
q 136759 327680,
q 4376291 10485760,
q 2188147 5242880,
q 4376297 10485760,
q 218815 524288,
q 4376303 10485760,
q 2188153 5242880,
q 4376309 10485760,
q 547039 1310720,
q 875263 2097152,
q 2188159 5242880,
q 4376321 10485760,
q 1094081 2621440,
q 4376327 10485760,
q 437633 1048576,
q 4376333 10485760,
q 273521 655360,
q 4376339 10485760,
q 2188171 5242880,
q 875269 2097152,
q 1094087 2621440,
q 4376351 10485760,
q 2188177 5242880,
q 4376357 10485760,
q 109409 262144,
q 4376363 10485760,
q 2188183 5242880,
q 4376369 10485760,
q 1094093 2621440,
q 875275 2097152
]
theorem cover7_ok :
checkCover (q 8030906143 10000000000) (q 875275 2097152) (q 874975 2097152) cover7 = true := by
decide +kernel
theorem cover7_sound : ∀ σ ∈ Set.Icc (((q 874975 2097152) : ℚ) : ℝ) (((q 875275 2097152) : ℚ) : ℝ),
rsF σ ≤ (((q 8030906143 10000000000) : ℚ) : ℝ) :=
checkCover_sound cover7_ok
end MaxLeafFormal.RSRate