MaxLeafFormal.RSCover9
Source file MaxLeafFormal/RSCover9.lean of the Lean project (how it is built).
import MaxLeafFormal.RSCheck
/-!
# RS closed-form rate: cover 1, chunk 9 (generated)
Generated by `scripts/export_rs_cover.py` (bisection as in
`ancillary/rs_closed_form_interval.py`,
SHA-256 `6ea21466e9a6f7153bafd754cbc8d0cdea78ef1c6f83ec9b25309d6aec87643e`).
500 intervals covering [875575/2097152, 875875/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 `875575/2097152`. -/
def cover9 : List ℚ := [
q 2188939 5242880,
q 4377881 10485760,
q 1094471 2621440,
q 4377887 10485760,
q 437789 1048576,
q 4377893 10485760,
q 547237 1310720,
q 4377899 10485760,
q 2188951 5242880,
q 875581 2097152,
q 1094477 2621440,
q 4377911 10485760,
q 2188957 5242880,
q 4377917 10485760,
q 13681 32768,
q 4377923 10485760,
q 2188963 5242880,
q 4377929 10485760,
q 1094483 2621440,
q 875587 2097152,
q 2188969 5242880,
q 4377941 10485760,
q 547243 1310720,
q 4377947 10485760,
q 437795 1048576,
q 4377953 10485760,
q 1094489 2621440,
q 4377959 10485760,
q 2188981 5242880,
q 875593 2097152,
q 273623 655360,
q 4377971 10485760,
q 2188987 5242880,
q 4377977 10485760,
q 218899 524288,
q 4377983 10485760,
q 2188993 5242880,
q 4377989 10485760,
q 547249 1310720,
q 875599 2097152,
q 2188999 5242880,
q 4378001 10485760,
q 1094501 2621440,
q 4378007 10485760,
q 437801 1048576,
q 4378013 10485760,
q 136813 327680,
q 4378019 10485760,
q 2189011 5242880,
q 875605 2097152,
q 1094507 2621440,
q 4378031 10485760,
q 2189017 5242880,
q 4378037 10485760,
q 109451 262144,
q 4378043 10485760,
q 2189023 5242880,
q 4378049 10485760,
q 1094513 2621440,
q 875611 2097152,
q 2189029 5242880,
q 4378061 10485760,
q 273629 655360,
q 4378067 10485760,
q 437807 1048576,
q 4378073 10485760,
q 1094519 2621440,
q 4378079 10485760,
q 2189041 5242880,
q 875617 2097152,
q 547261 1310720,
q 4378091 10485760,
q 2189047 5242880,
q 4378097 10485760,
q 218905 524288,
q 4378103 10485760,
q 2189053 5242880,
q 4378109 10485760,
q 8551 20480,
q 875623 2097152,
q 2189059 5242880,
q 4378121 10485760,
q 1094531 2621440,
q 4378127 10485760,
q 437813 1048576,
q 4378133 10485760,
q 547267 1310720,
q 4378139 10485760,
q 2189071 5242880,
q 875629 2097152,
q 1094537 2621440,
q 4378151 10485760,
q 2189077 5242880,
q 4378157 10485760,
q 54727 131072,
q 4378163 10485760,
q 2189083 5242880,
q 4378169 10485760,
q 1094543 2621440,
q 875635 2097152,
q 2189089 5242880,
q 4378181 10485760,
q 547273 1310720,
q 4378187 10485760,
q 437819 1048576,
q 4378193 10485760,
q 1094549 2621440,
q 4378199 10485760,
q 2189101 5242880,
q 875641 2097152,
q 136819 327680,
q 4378211 10485760,
q 2189107 5242880,
q 4378217 10485760,
q 218911 524288,
q 4378223 10485760,
q 2189113 5242880,
q 4378229 10485760,
q 547279 1310720,
q 875647 2097152,
q 2189119 5242880,
q 4378241 10485760,
q 1094561 2621440,
q 4378247 10485760,
q 437825 1048576,
q 4378253 10485760,
q 273641 655360,
q 4378259 10485760,
q 2189131 5242880,
q 875653 2097152,
q 1094567 2621440,
q 4378271 10485760,
q 2189137 5242880,
q 4378277 10485760,
q 109457 262144,
q 4378283 10485760,
q 2189143 5242880,
q 4378289 10485760,
q 1094573 2621440,
q 875659 2097152,
q 2189149 5242880,
q 4378301 10485760,
q 68411 163840,
q 4378307 10485760,
q 437831 1048576,
q 4378313 10485760,
q 1094579 2621440,
q 4378319 10485760,
q 2189161 5242880,
q 875665 2097152,
q 547291 1310720,
q 4378331 10485760,
q 2189167 5242880,
q 4378337 10485760,
q 218917 524288,
q 4378343 10485760,
q 2189173 5242880,
q 4378349 10485760,
q 273647 655360,
q 875671 2097152,
q 2189179 5242880,
q 4378361 10485760,
q 1094591 2621440,
q 4378367 10485760,
q 437837 1048576,
q 4378373 10485760,
q 547297 1310720,
q 4378379 10485760,
q 2189191 5242880,
q 875677 2097152,
q 1094597 2621440,
q 4378391 10485760,
q 2189197 5242880,
q 4378397 10485760,
q 27365 65536,
q 4378403 10485760,
q 2189203 5242880,
q 4378409 10485760,
q 1094603 2621440,
q 875683 2097152,
q 2189209 5242880,
q 4378421 10485760,
q 547303 1310720,
q 4378427 10485760,
q 437843 1048576,
q 4378433 10485760,
q 1094609 2621440,
q 4378439 10485760,
q 2189221 5242880,
q 875689 2097152,
q 273653 655360,
q 4378451 10485760,
q 2189227 5242880,
q 4378457 10485760,
q 218923 524288,
q 4378463 10485760,
q 2189233 5242880,
q 4378469 10485760,
q 547309 1310720,
q 875695 2097152,
q 2189239 5242880,
q 4378481 10485760,
q 1094621 2621440,
q 4378487 10485760,
q 437849 1048576,
q 4378493 10485760,
q 34207 81920,
q 4378499 10485760,
q 2189251 5242880,
q 875701 2097152,
q 1094627 2621440,
q 4378511 10485760,
q 2189257 5242880,
q 4378517 10485760,
q 109463 262144,
q 4378523 10485760,
q 2189263 5242880,
q 4378529 10485760,
q 1094633 2621440,
q 875707 2097152,
q 2189269 5242880,
q 4378541 10485760,
q 273659 655360,
q 4378547 10485760,
q 437855 1048576,
q 4378553 10485760,
q 1094639 2621440,
q 4378559 10485760,
q 2189281 5242880,
q 875713 2097152,
q 547321 1310720,
q 4378571 10485760,
q 2189287 5242880,
q 4378577 10485760,
q 218929 524288,
q 4378583 10485760,
q 2189293 5242880,
q 4378589 10485760,
q 136831 327680,
q 875719 2097152,
q 2189299 5242880,
q 4378601 10485760,
q 1094651 2621440,
q 4378607 10485760,
q 437861 1048576,
q 4378613 10485760,
q 547327 1310720,
q 4378619 10485760,
q 2189311 5242880,
q 875725 2097152,
q 1094657 2621440,
q 4378631 10485760,
q 2189317 5242880,
q 4378637 10485760,
q 54733 131072,
q 4378643 10485760,
q 2189323 5242880,
q 4378649 10485760,
q 1094663 2621440,
q 875731 2097152,
q 2189329 5242880,
q 4378661 10485760,
q 547333 1310720,
q 4378667 10485760,
q 437867 1048576,
q 4378673 10485760,
q 1094669 2621440,
q 4378679 10485760,
q 2189341 5242880,
q 875737 2097152,
q 68417 163840,
q 4378691 10485760,
q 2189347 5242880,
q 4378697 10485760,
q 218935 524288,
q 4378703 10485760,
q 2189353 5242880,
q 4378709 10485760,
q 547339 1310720,
q 875743 2097152,
q 2189359 5242880,
q 4378721 10485760,
q 1094681 2621440,
q 4378727 10485760,
q 437873 1048576,
q 4378733 10485760,
q 273671 655360,
q 4378739 10485760,
q 2189371 5242880,
q 875749 2097152,
q 1094687 2621440,
q 4378751 10485760,
q 2189377 5242880,
q 4378757 10485760,
q 109469 262144,
q 4378763 10485760,
q 2189383 5242880,
q 4378769 10485760,
q 1094693 2621440,
q 875755 2097152,
q 2189389 5242880,
q 4378781 10485760,
q 136837 327680,
q 4378787 10485760,
q 437879 1048576,
q 4378793 10485760,
q 1094699 2621440,
q 4378799 10485760,
q 2189401 5242880,
q 875761 2097152,
q 547351 1310720,
q 4378811 10485760,
q 2189407 5242880,
q 4378817 10485760,
q 218941 524288,
q 4378823 10485760,
q 2189413 5242880,
q 4378829 10485760,
q 273677 655360,
q 875767 2097152,
q 2189419 5242880,
q 4378841 10485760,
q 1094711 2621440,
q 4378847 10485760,
q 437885 1048576,
q 4378853 10485760,
q 547357 1310720,
q 4378859 10485760,
q 2189431 5242880,
q 875773 2097152,
q 1094717 2621440,
q 4378871 10485760,
q 2189437 5242880,
q 4378877 10485760,
q 3421 8192,
q 4378883 10485760,
q 2189443 5242880,
q 4378889 10485760,
q 1094723 2621440,
q 875779 2097152,
q 2189449 5242880,
q 4378901 10485760,
q 547363 1310720,
q 4378907 10485760,
q 437891 1048576,
q 4378913 10485760,
q 1094729 2621440,
q 4378919 10485760,
q 2189461 5242880,
q 875785 2097152,
q 273683 655360,
q 4378931 10485760,
q 2189467 5242880,
q 4378937 10485760,
q 218947 524288,
q 4378943 10485760,
q 2189473 5242880,
q 4378949 10485760,
q 547369 1310720,
q 875791 2097152,
q 2189479 5242880,
q 4378961 10485760,
q 1094741 2621440,
q 4378967 10485760,
q 437897 1048576,
q 4378973 10485760,
q 136843 327680,
q 4378979 10485760,
q 2189491 5242880,
q 875797 2097152,
q 1094747 2621440,
q 4378991 10485760,
q 2189497 5242880,
q 4378997 10485760,
q 109475 262144,
q 4379003 10485760,
q 2189503 5242880,
q 4379009 10485760,
q 1094753 2621440,
q 875803 2097152,
q 2189509 5242880,
q 4379021 10485760,
q 273689 655360,
q 4379027 10485760,
q 437903 1048576,
q 4379033 10485760,
q 1094759 2621440,
q 4379039 10485760,
q 2189521 5242880,
q 875809 2097152,
q 547381 1310720,
q 4379051 10485760,
q 2189527 5242880,
q 4379057 10485760,
q 218953 524288,
q 4379063 10485760,
q 2189533 5242880,
q 4379069 10485760,
q 68423 163840,
q 875815 2097152,
q 2189539 5242880,
q 4379081 10485760,
q 1094771 2621440,
q 4379087 10485760,
q 437909 1048576,
q 4379093 10485760,
q 547387 1310720,
q 4379099 10485760,
q 2189551 5242880,
q 875821 2097152,
q 1094777 2621440,
q 4379111 10485760,
q 2189557 5242880,
q 4379117 10485760,
q 54739 131072,
q 4379123 10485760,
q 2189563 5242880,
q 4379129 10485760,
q 1094783 2621440,
q 875827 2097152,
q 2189569 5242880,
q 4379141 10485760,
q 547393 1310720,
q 4379147 10485760,
q 437915 1048576,
q 4379153 10485760,
q 1094789 2621440,
q 4379159 10485760,
q 2189581 5242880,
q 875833 2097152,
q 136849 327680,
q 4379171 10485760,
q 2189587 5242880,
q 4379177 10485760,
q 218959 524288,
q 4379183 10485760,
q 2189593 5242880,
q 4379189 10485760,
q 547399 1310720,
q 875839 2097152,
q 2189599 5242880,
q 4379201 10485760,
q 1094801 2621440,
q 4379207 10485760,
q 437921 1048576,
q 4379213 10485760,
q 273701 655360,
q 4379219 10485760,
q 2189611 5242880,
q 875845 2097152,
q 1094807 2621440,
q 4379231 10485760,
q 2189617 5242880,
q 4379237 10485760,
q 109481 262144,
q 4379243 10485760,
q 2189623 5242880,
q 4379249 10485760,
q 1094813 2621440,
q 875851 2097152,
q 2189629 5242880,
q 4379261 10485760,
q 34213 81920,
q 4379267 10485760,
q 437927 1048576,
q 4379273 10485760,
q 1094819 2621440,
q 4379279 10485760,
q 2189641 5242880,
q 875857 2097152,
q 547411 1310720,
q 4379291 10485760,
q 2189647 5242880,
q 4379297 10485760,
q 218965 524288,
q 4379303 10485760,
q 2189653 5242880,
q 4379309 10485760,
q 273707 655360,
q 875863 2097152,
q 2189659 5242880,
q 4379321 10485760,
q 1094831 2621440,
q 4379327 10485760,
q 437933 1048576,
q 4379333 10485760,
q 547417 1310720,
q 4379339 10485760,
q 2189671 5242880,
q 875869 2097152,
q 1094837 2621440,
q 4379351 10485760,
q 2189677 5242880,
q 4379357 10485760,
q 27371 65536,
q 4379363 10485760,
q 2189683 5242880,
q 4379369 10485760,
q 1094843 2621440,
q 875875 2097152
]
theorem cover9_ok :
checkCover (q 8030906143 10000000000) (q 875875 2097152) (q 875575 2097152) cover9 = true := by
decide +kernel
theorem cover9_sound : ∀ σ ∈ Set.Icc (((q 875575 2097152) : ℚ) : ℝ) (((q 875875 2097152) : ℚ) : ℝ),
rsF σ ≤ (((q 8030906143 10000000000) : ℚ) : ℝ) :=
checkCover_sound cover9_ok
end MaxLeafFormal.RSRate