import MaxLeafFormal.RSCheck /-! # RS closed-form rate: cover 1, chunk 12 (generated) Generated by `scripts/export_rs_cover.py` (bisection as in `ancillary/rs_closed_form_interval.py`, SHA-256 `6ea21466e9a6f7153bafd754cbc8d0cdea78ef1c6f83ec9b25309d6aec87643e`). 500 intervals covering [876475/2097152, 876775/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 `876475/2097152`. -/ def cover12 : List ℚ := [ q 2191189 5242880, q 4382381 10485760, q 273899 655360, q 4382387 10485760, q 438239 1048576, q 4382393 10485760, q 1095599 2621440, q 4382399 10485760, q 2191201 5242880, q 876481 2097152, q 547801 1310720, q 4382411 10485760, q 2191207 5242880, q 4382417 10485760, q 219121 524288, q 4382423 10485760, q 2191213 5242880, q 4382429 10485760, q 136951 327680, q 876487 2097152, q 2191219 5242880, q 4382441 10485760, q 1095611 2621440, q 4382447 10485760, q 438245 1048576, q 4382453 10485760, q 547807 1310720, q 4382459 10485760, q 2191231 5242880, q 876493 2097152, q 1095617 2621440, q 4382471 10485760, q 2191237 5242880, q 4382477 10485760, q 54781 131072, q 4382483 10485760, q 2191243 5242880, q 4382489 10485760, q 1095623 2621440, q 876499 2097152, q 2191249 5242880, q 4382501 10485760, q 547813 1310720, q 4382507 10485760, q 438251 1048576, q 4382513 10485760, q 1095629 2621440, q 4382519 10485760, q 2191261 5242880, q 876505 2097152, q 68477 163840, q 4382531 10485760, q 2191267 5242880, q 4382537 10485760, q 219127 524288, q 4382543 10485760, q 2191273 5242880, q 4382549 10485760, q 547819 1310720, q 876511 2097152, q 2191279 5242880, q 4382561 10485760, q 1095641 2621440, q 4382567 10485760, q 438257 1048576, q 4382573 10485760, q 273911 655360, q 4382579 10485760, q 2191291 5242880, q 876517 2097152, q 1095647 2621440, q 4382591 10485760, q 2191297 5242880, q 4382597 10485760, q 109565 262144, q 4382603 10485760, q 2191303 5242880, q 4382609 10485760, q 1095653 2621440, q 876523 2097152, q 2191309 5242880, q 4382621 10485760, q 136957 327680, q 4382627 10485760, q 438263 1048576, q 4382633 10485760, q 1095659 2621440, q 4382639 10485760, q 2191321 5242880, q 876529 2097152, q 547831 1310720, q 4382651 10485760, q 2191327 5242880, q 4382657 10485760, q 219133 524288, q 4382663 10485760, q 2191333 5242880, q 4382669 10485760, q 273917 655360, q 876535 2097152, q 2191339 5242880, q 4382681 10485760, q 1095671 2621440, q 4382687 10485760, q 438269 1048576, q 4382693 10485760, q 547837 1310720, q 4382699 10485760, q 2191351 5242880, q 876541 2097152, q 1095677 2621440, q 4382711 10485760, q 2191357 5242880, q 4382717 10485760, q 107 256, q 4382723 10485760, q 2191363 5242880, q 4382729 10485760, q 1095683 2621440, q 876547 2097152, q 2191369 5242880, q 4382741 10485760, q 547843 1310720, q 4382747 10485760, q 438275 1048576, q 4382753 10485760, q 1095689 2621440, q 4382759 10485760, q 2191381 5242880, q 876553 2097152, q 273923 655360, q 4382771 10485760, q 2191387 5242880, q 4382777 10485760, q 219139 524288, q 4382783 10485760, q 2191393 5242880, q 4382789 10485760, q 547849 1310720, q 876559 2097152, q 2191399 5242880, q 4382801 10485760, q 1095701 2621440, q 4382807 10485760, q 438281 1048576, q 4382813 10485760, q 136963 327680, q 4382819 10485760, q 2191411 5242880, q 876565 2097152, q 1095707 2621440, q 4382831 10485760, q 2191417 5242880, q 4382837 10485760, q 109571 262144, q 4382843 10485760, q 2191423 5242880, q 4382849 10485760, q 1095713 2621440, q 876571 2097152, q 2191429 5242880, q 4382861 10485760, q 273929 655360, q 4382867 10485760, q 438287 1048576, q 4382873 10485760, q 1095719 2621440, q 4382879 10485760, q 2191441 5242880, q 876577 2097152, q 547861 1310720, q 4382891 10485760, q 2191447 5242880, q 4382897 10485760, q 219145 524288, q 4382903 10485760, q 2191453 5242880, q 4382909 10485760, q 68483 163840, q 876583 2097152, q 2191459 5242880, q 4382921 10485760, q 1095731 2621440, q 4382927 10485760, q 438293 1048576, q 4382933 10485760, q 547867 1310720, q 4382939 10485760, q 2191471 5242880, q 876589 2097152, q 1095737 2621440, q 4382951 10485760, q 2191477 5242880, q 4382957 10485760, q 54787 131072, q 4382963 10485760, q 2191483 5242880, q 4382969 10485760, q 1095743 2621440, q 876595 2097152, q 2191489 5242880, q 4382981 10485760, q 547873 1310720, q 4382987 10485760, q 438299 1048576, q 4382993 10485760, q 1095749 2621440, q 4382999 10485760, q 2191501 5242880, q 876601 2097152, q 136969 327680, q 4383011 10485760, q 2191507 5242880, q 4383017 10485760, q 219151 524288, q 4383023 10485760, q 2191513 5242880, q 4383029 10485760, q 547879 1310720, q 876607 2097152, q 2191519 5242880, q 4383041 10485760, q 1095761 2621440, q 4383047 10485760, q 438305 1048576, q 4383053 10485760, q 273941 655360, q 4383059 10485760, q 2191531 5242880, q 876613 2097152, q 1095767 2621440, q 4383071 10485760, q 2191537 5242880, q 4383077 10485760, q 109577 262144, q 4383083 10485760, q 2191543 5242880, q 4383089 10485760, q 1095773 2621440, q 876619 2097152, q 2191549 5242880, q 4383101 10485760, q 34243 81920, q 4383107 10485760, q 438311 1048576, q 4383113 10485760, q 1095779 2621440, q 4383119 10485760, q 2191561 5242880, q 876625 2097152, q 547891 1310720, q 4383131 10485760, q 2191567 5242880, q 4383137 10485760, q 219157 524288, q 4383143 10485760, q 2191573 5242880, q 4383149 10485760, q 273947 655360, q 876631 2097152, q 2191579 5242880, q 4383161 10485760, q 1095791 2621440, q 4383167 10485760, q 438317 1048576, q 4383173 10485760, q 547897 1310720, q 4383179 10485760, q 2191591 5242880, q 876637 2097152, q 1095797 2621440, q 4383191 10485760, q 2191597 5242880, q 4383197 10485760, q 27395 65536, q 4383203 10485760, q 2191603 5242880, q 4383209 10485760, q 1095803 2621440, q 876643 2097152, q 2191609 5242880, q 4383221 10485760, q 547903 1310720, q 4383227 10485760, q 438323 1048576, q 4383233 10485760, q 1095809 2621440, q 4383239 10485760, q 2191621 5242880, q 876649 2097152, q 273953 655360, q 4383251 10485760, q 2191627 5242880, q 4383257 10485760, q 219163 524288, q 4383263 10485760, q 2191633 5242880, q 4383269 10485760, q 547909 1310720, q 876655 2097152, q 2191639 5242880, q 4383281 10485760, q 1095821 2621440, q 4383287 10485760, q 438329 1048576, q 4383293 10485760, q 68489 163840, q 4383299 10485760, q 2191651 5242880, q 876661 2097152, q 1095827 2621440, q 4383311 10485760, q 2191657 5242880, q 4383317 10485760, q 109583 262144, q 4383323 10485760, q 2191663 5242880, q 4383329 10485760, q 1095833 2621440, q 876667 2097152, q 2191669 5242880, q 4383341 10485760, q 273959 655360, q 4383347 10485760, q 438335 1048576, q 4383353 10485760, q 1095839 2621440, q 4383359 10485760, q 2191681 5242880, q 876673 2097152, q 547921 1310720, q 4383371 10485760, q 2191687 5242880, q 4383377 10485760, q 219169 524288, q 4383383 10485760, q 2191693 5242880, q 4383389 10485760, q 136981 327680, q 876679 2097152, q 2191699 5242880, q 4383401 10485760, q 1095851 2621440, q 4383407 10485760, q 438341 1048576, q 4383413 10485760, q 547927 1310720, q 4383419 10485760, q 2191711 5242880, q 876685 2097152, q 1095857 2621440, q 4383431 10485760, q 2191717 5242880, q 4383437 10485760, q 54793 131072, q 4383443 10485760, q 2191723 5242880, q 4383449 10485760, q 1095863 2621440, q 876691 2097152, q 2191729 5242880, q 4383461 10485760, q 547933 1310720, q 4383467 10485760, q 438347 1048576, q 4383473 10485760, q 1095869 2621440, q 4383479 10485760, q 2191741 5242880, q 876697 2097152, q 17123 40960, q 4383491 10485760, q 2191747 5242880, q 4383497 10485760, q 219175 524288, q 4383503 10485760, q 2191753 5242880, q 4383509 10485760, q 547939 1310720, q 876703 2097152, q 2191759 5242880, q 4383521 10485760, q 1095881 2621440, q 4383527 10485760, q 438353 1048576, q 4383533 10485760, q 273971 655360, q 4383539 10485760, q 2191771 5242880, q 876709 2097152, q 1095887 2621440, q 4383551 10485760, q 2191777 5242880, q 4383557 10485760, q 109589 262144, q 4383563 10485760, q 2191783 5242880, q 4383569 10485760, q 1095893 2621440, q 876715 2097152, q 2191789 5242880, q 4383581 10485760, q 136987 327680, q 4383587 10485760, q 438359 1048576, q 4383593 10485760, q 1095899 2621440, q 4383599 10485760, q 2191801 5242880, q 876721 2097152, q 547951 1310720, q 4383611 10485760, q 2191807 5242880, q 4383617 10485760, q 219181 524288, q 4383623 10485760, q 2191813 5242880, q 4383629 10485760, q 273977 655360, q 876727 2097152, q 2191819 5242880, q 4383641 10485760, q 1095911 2621440, q 4383647 10485760, q 438365 1048576, q 4383653 10485760, q 547957 1310720, q 4383659 10485760, q 2191831 5242880, q 876733 2097152, q 1095917 2621440, q 4383671 10485760, q 2191837 5242880, q 4383677 10485760, q 13699 32768, q 4383683 10485760, q 2191843 5242880, q 4383689 10485760, q 1095923 2621440, q 876739 2097152, q 2191849 5242880, q 4383701 10485760, q 547963 1310720, q 4383707 10485760, q 438371 1048576, q 4383713 10485760, q 1095929 2621440, q 4383719 10485760, q 2191861 5242880, q 876745 2097152, q 273983 655360, q 4383731 10485760, q 2191867 5242880, q 4383737 10485760, q 219187 524288, q 4383743 10485760, q 2191873 5242880, q 4383749 10485760, q 547969 1310720, q 876751 2097152, q 2191879 5242880, q 4383761 10485760, q 1095941 2621440, q 4383767 10485760, q 438377 1048576, q 4383773 10485760, q 136993 327680, q 4383779 10485760, q 2191891 5242880, q 876757 2097152, q 1095947 2621440, q 4383791 10485760, q 2191897 5242880, q 4383797 10485760, q 109595 262144, q 4383803 10485760, q 2191903 5242880, q 4383809 10485760, q 1095953 2621440, q 876763 2097152, q 2191909 5242880, q 4383821 10485760, q 273989 655360, q 4383827 10485760, q 438383 1048576, q 4383833 10485760, q 1095959 2621440, q 4383839 10485760, q 2191921 5242880, q 876769 2097152, q 547981 1310720, q 4383851 10485760, q 2191927 5242880, q 4383857 10485760, q 219193 524288, q 4383863 10485760, q 2191933 5242880, q 4383869 10485760, q 34249 81920, q 876775 2097152 ] theorem cover12_ok : checkCover (q 8030906143 10000000000) (q 876775 2097152) (q 876475 2097152) cover12 = true := by decide +kernel theorem cover12_sound : ∀ σ ∈ Set.Icc (((q 876475 2097152) : ℚ) : ℝ) (((q 876775 2097152) : ℚ) : ℝ), rsF σ ≤ (((q 8030906143 10000000000) : ℚ) : ℝ) := checkCover_sound cover12_ok end MaxLeafFormal.RSRate