MaxLeafFormal.CCData
Source file MaxLeafFormal/CCData.lean of the Lean project (how it is built).
import Mathlib
/-!
# Graph Motif rate certificate data (generated)
Generated by `formal/scripts/export_cc_cert.py`, recomputing the parameters of
`ancillary/component_count_rate_interval.py`, SHA-256 `4ce8f7323b39dbb6fcce68425f52503d152b5384ec4195087f70f21c664ce1dc`.
Entry `j` is `y_j` for the interval `[0.7175 + j/10^4, 0.7175 + (j+1)/10^4]`.
Do not edit by hand. This file is data, not proof: every condition is re-checked in
`MaxLeafFormal.CCRate`.
-/
set_option maxRecDepth 100000
namespace MaxLeafFormal.CCRate
/-- The rational `a / b`. -/
def q (a b : ℕ) : ℚ := (a : ℚ) / b
/-- The parameters `y_j`, `j = 0, …, 924`. -/
def ys : List ℚ := [
q 64731 50000,
q 5183 4000,
q 16211 12500,
q 64901 50000,
q 25983 20000,
q 32507 25000,
q 65071 50000,
q 26051 20000,
q 4074 3125,
q 65241 50000,
q 26119 20000,
q 130709 100000,
q 65411 50000,
q 16367 12500,
q 2621 2000,
q 131163 100000,
q 131277 100000,
q 131391 100000,
q 26301 20000,
q 131619 100000,
q 32933 25000,
q 65923 50000,
q 3299 2500,
q 66037 50000,
q 33047 25000,
q 132303 100000,
q 132417 100000,
q 132531 100000,
q 26529 20000,
q 132759 100000,
q 66437 50000,
q 33247 25000,
q 66551 50000,
q 133217 100000,
q 133331 100000,
q 66723 50000,
q 3339 2500,
q 5347 4000,
q 133789 100000,
q 8369 6250,
q 134019 100000,
q 134133 100000,
q 16781 12500,
q 134363 100000,
q 67239 50000,
q 134593 100000,
q 33677 25000,
q 134823 100000,
q 67469 50000,
q 135053 100000,
q 4224 3125,
q 135283 100000,
q 67699 50000,
q 67757 50000,
q 135629 100000,
q 4242 3125,
q 6793 5000,
q 5439 4000,
q 136091 100000,
q 68103 50000,
q 68161 50000,
q 136437 100000,
q 136553 100000,
q 136669 100000,
q 27357 20000,
q 1369 1000,
q 17127 12500,
q 34283 25000,
q 4289 3125,
q 34341 25000,
q 3437 2500,
q 34399 25000,
q 8607 6250,
q 137829 100000,
q 27589 20000,
q 138061 100000,
q 138177 100000,
q 69147 50000,
q 13841 10000,
q 138527 100000,
q 138643 100000,
q 3469 2500,
q 34719 25000,
q 138993 100000,
q 13911 10000,
q 69613 50000,
q 139343 100000,
q 6973 5000,
q 139577 100000,
q 69847 50000,
q 139811 100000,
q 17491 12500,
q 28009 20000,
q 70081 50000,
q 140279 100000,
q 140397 100000,
q 70257 50000,
q 140631 100000,
q 140749 100000,
q 70433 50000,
q 17623 12500,
q 141101 100000,
q 141219 100000,
q 141337 100000,
q 70727 50000,
q 35393 25000,
q 14169 10000,
q 8863 6250,
q 70963 50000,
q 35511 25000,
q 71081 50000,
q 3557 2500,
q 71199 50000,
q 35629 25000,
q 71317 50000,
q 142753 100000,
q 142871 100000,
q 142989 100000,
q 35777 25000,
q 71613 50000,
q 28669 20000,
q 143463 100000,
q 71791 50000,
q 143701 100000,
q 7191 5000,
q 71969 50000,
q 144057 100000,
q 9011 6250,
q 28859 20000,
q 72207 50000,
q 144533 100000,
q 144653 100000,
q 36193 25000,
q 144891 100000,
q 14501 10000,
q 14513 10000,
q 145249 100000,
q 145369 100000,
q 9093 6250,
q 18201 12500,
q 145727 100000,
q 145847 100000,
q 145967 100000,
q 146087 100000,
q 146207 100000,
q 146327 100000,
q 146447 100000,
q 146567 100000,
q 146687 100000,
q 146807 100000,
q 146927 100000,
q 18381 12500,
q 4599 3125,
q 18411 12500,
q 147409 100000,
q 147529 100000,
q 2953 2000,
q 147771 100000,
q 147891 100000,
q 37003 25000,
q 148133 100000,
q 74127 50000,
q 1187 800,
q 9281 6250,
q 148617 100000,
q 74369 50000,
q 148859 100000,
q 7449 5000,
q 74551 50000,
q 149223 100000,
q 29869 20000,
q 74733 50000,
q 37397 25000,
q 149709 100000,
q 149831 100000,
q 149953 100000,
q 75037 50000,
q 37549 25000,
q 75159 50000,
q 3761 2500,
q 75281 50000,
q 37671 25000,
q 75403 50000,
q 150929 100000,
q 151051 100000,
q 151173 100000,
q 4728 3125,
q 75709 50000,
q 151541 100000,
q 151663 100000,
q 75893 50000,
q 151909 100000,
q 4751 3125,
q 30431 20000,
q 152277 100000,
q 381 250,
q 38131 25000,
q 152647 100000,
q 15277 10000,
q 152893 100000,
q 19127 12500,
q 7657 5000,
q 153263 100000,
q 153387 100000,
q 15351 10000,
q 76817 50000,
q 76879 50000,
q 76941 50000,
q 30801 20000,
q 154129 100000,
q 154253 100000,
q 154377 100000,
q 154501 100000,
q 77313 50000,
q 619 400,
q 77437 50000,
q 154999 100000,
q 155123 100000,
q 155247 100000,
q 38843 25000,
q 155497 100000,
q 155621 100000,
q 77873 50000,
q 155871 100000,
q 38999 25000,
q 156121 100000,
q 78123 50000,
q 156371 100000,
q 9781 6250,
q 78311 50000,
q 156747 100000,
q 19609 12500,
q 78499 50000,
q 157123 100000,
q 157249 100000,
q 1259 800,
q 63 40,
q 78813 50000,
q 19719 12500,
q 78939 50000,
q 39501 25000,
q 15813 10000,
q 9891 6250,
q 158383 100000,
q 158509 100000,
q 31727 20000,
q 79381 50000,
q 19861 12500,
q 31803 20000,
q 79571 50000,
q 39817 25000,
q 31879 20000,
q 79761 50000,
q 159649 100000,
q 4993 3125,
q 159903 100000,
q 16003 10000,
q 80079 50000,
q 32057 20000,
q 40103 25000,
q 8027 5000,
q 160667 100000,
q 32159 20000,
q 160923 100000,
q 3221 2000,
q 80589 50000,
q 80653 50000,
q 80717 50000,
q 80781 50000,
q 16169 10000,
q 161819 100000,
q 161947 100000,
q 6483 4000,
q 40551 25000,
q 40583 25000,
q 162461 100000,
q 162589 100000,
q 81359 50000,
q 162847 100000,
q 5093 3125,
q 32621 20000,
q 81617 50000,
q 163363 100000,
q 40873 25000,
q 163621 100000,
q 163751 100000,
q 4097 2500,
q 16401 10000,
q 164139 100000,
q 164269 100000,
q 164399 100000,
q 10283 6250,
q 82329 50000,
q 41197 25000,
q 82459 50000,
q 20631 12500,
q 165179 100000,
q 165309 100000,
q 165439 100000,
q 16557 10000,
q 1657 1000,
q 165831 100000,
q 165961 100000,
q 41523 25000,
q 166223 100000,
q 83177 50000,
q 33297 20000,
q 20827 12500,
q 166747 100000,
q 83439 50000,
q 16701 10000,
q 167141 100000,
q 167273 100000,
q 41851 25000,
q 10471 6250,
q 167667 100000,
q 167799 100000,
q 167931 100000,
q 168063 100000,
q 33639 20000,
q 168327 100000,
q 168459 100000,
q 10537 6250,
q 42181 25000,
q 21107 12500,
q 168989 100000,
q 84561 50000,
q 84627 50000,
q 169387 100000,
q 2119 1250,
q 169653 100000,
q 84893 50000,
q 169919 100000,
q 42513 25000,
q 34037 20000,
q 170319 100000,
q 42613 25000,
q 85293 50000,
q 170719 100000,
q 170853 100000,
q 170987 100000,
q 171121 100000,
q 34251 20000,
q 171389 100000,
q 171523 100000,
q 171657 100000,
q 171791 100000,
q 85963 50000,
q 8603 5000,
q 34439 20000,
q 172329 100000,
q 10779 6250,
q 172599 100000,
q 86367 50000,
q 172869 100000,
q 43251 25000,
q 173139 100000,
q 86637 50000,
q 17341 10000,
q 34709 20000,
q 2171 1250,
q 21727 12500,
q 5436 3125,
q 174087 100000,
q 174223 100000,
q 174359 100000,
q 34899 20000,
q 174631 100000,
q 10923 6250,
q 21863 12500,
q 1094 625,
q 175177 100000,
q 175313 100000,
q 3509 2000,
q 175587 100000,
q 43931 25000,
q 8793 5000,
q 175997 100000,
q 35227 20000,
q 11017 6250,
q 176409 100000,
q 88273 50000,
q 44171 25000,
q 176821 100000,
q 176959 100000,
q 177097 100000,
q 35447 20000,
q 44343 25000,
q 17751 10000,
q 177649 100000,
q 177787 100000,
q 7117 4000,
q 178063 100000,
q 89101 50000,
q 8917 5000,
q 178479 100000,
q 89309 50000,
q 178757 100000,
q 11181 6250,
q 35807 20000,
q 89587 50000,
q 179313 100000,
q 44863 25000,
q 22449 12500,
q 179731 100000,
q 179871 100000,
q 18001 10000,
q 3603 2000,
q 18029 10000,
q 18043 10000,
q 18057 10000,
q 18071 10000,
q 3617 2000,
q 180991 100000,
q 181131 100000,
q 22659 12500,
q 45353 25000,
q 181553 100000,
q 90847 50000,
q 36367 20000,
q 22747 12500,
q 182117 100000,
q 91129 50000,
q 228 125,
q 182541 100000,
q 91341 50000,
q 22853 12500,
q 91483 50000,
q 183107 100000,
q 183249 100000,
q 183391 100000,
q 183533 100000,
q 45919 25000,
q 91909 50000,
q 4599 2500,
q 184103 100000,
q 36849 20000,
q 46097 25000,
q 184531 100000,
q 92337 50000,
q 184817 100000,
q 1156 625,
q 185103 100000,
q 92623 50000,
q 18539 10000,
q 185533 100000,
q 185677 100000,
q 9291 5000,
q 46491 25000,
q 46527 25000,
q 46563 25000,
q 46599 25000,
q 9327 5000,
q 46671 25000,
q 186829 100000,
q 186973 100000,
q 93559 50000,
q 187263 100000,
q 187407 100000,
q 5861 3125,
q 187697 100000,
q 93921 50000,
q 46997 25000,
q 188133 100000,
q 94139 50000,
q 23553 12500,
q 188569 100000,
q 37743 20000,
q 188861 100000,
q 189007 100000,
q 189153 100000,
q 189299 100000,
q 37889 20000,
q 23699 12500,
q 94869 50000,
q 37977 20000,
q 190031 100000,
q 95089 50000,
q 7613 4000,
q 23809 12500,
q 190619 100000,
q 95383 50000,
q 95457 50000,
q 191061 100000,
q 191209 100000,
q 47839 25000,
q 11969 6250,
q 47913 25000,
q 959 500,
q 47987 25000,
q 6003 3125,
q 48061 25000,
q 192393 100000,
q 192541 100000,
q 19269 10000,
q 96419 50000,
q 192987 100000,
q 12071 6250,
q 38657 20000,
q 96717 50000,
q 12099 6250,
q 193733 100000,
q 96941 50000,
q 12127 6250,
q 97091 50000,
q 194331 100000,
q 194481 100000,
q 194631 100000,
q 194781 100000,
q 48733 25000,
q 97541 50000,
q 6101 3125,
q 195383 100000,
q 97767 50000,
q 39137 20000,
q 39167 20000,
q 97993 50000,
q 98069 50000,
q 196289 100000,
q 4911 2500,
q 12287 6250,
q 196743 100000,
q 39379 20000,
q 197047 100000,
q 197199 100000,
q 197351 100000,
q 197503 100000,
q 39531 20000,
q 12363 6250,
q 4949 2500,
q 198113 100000,
q 39653 20000,
q 99209 50000,
q 198571 100000,
q 49681 25000,
q 198877 100000,
q 199031 100000,
q 12449 6250,
q 99669 50000,
q 199491 100000,
q 39929 20000,
q 199799 100000,
q 199953 100000,
q 200107 100000,
q 200261 100000,
q 6263 3125,
q 20057 10000,
q 8029 4000,
q 200879 100000,
q 100517 50000,
q 201189 100000,
q 6292 3125,
q 201499 100000,
q 40331 20000,
q 20181 10000,
q 100983 50000,
q 202121 100000,
q 202277 100000,
q 202433 100000,
q 202589 100000,
q 40549 20000,
q 202901 100000,
q 101529 50000,
q 101607 50000,
q 203371 100000,
q 25441 12500,
q 50921 25000,
q 203841 100000,
q 203999 100000,
q 51039 25000,
q 204313 100000,
q 204471 100000,
q 51157 25000,
q 102393 50000,
q 12809 6250,
q 102551 50000,
q 10263 5000,
q 102709 50000,
q 25697 12500,
q 41147 20000,
q 205893 100000,
q 51513 25000,
q 206211 100000,
q 20637 10000,
q 206529 100000,
q 6459 3125,
q 206847 100000,
q 207007 100000,
q 103583 50000,
q 103663 50000,
q 103743 50000,
q 103823 50000,
q 103903 50000,
q 103983 50000,
q 104063 50000,
q 208287 100000,
q 6514 3125,
q 6519 3125,
q 208769 100000,
q 20893 10000,
q 209091 100000,
q 52313 25000,
q 104707 50000,
q 8383 4000,
q 209737 100000,
q 209899 100000,
q 10503 5000,
q 105111 50000,
q 13149 6250,
q 210547 100000,
q 210709 100000,
q 26359 12500,
q 105517 50000,
q 211197 100000,
q 1321 625,
q 211523 100000,
q 105843 50000,
q 211849 100000,
q 212013 100000,
q 13261 6250,
q 10617 5000,
q 26563 12500,
q 53167 25000,
q 6651 3125,
q 53249 25000,
q 213161 100000,
q 8533 4000,
q 21349 10000,
q 106827 50000,
q 213819 100000,
q 6687 3125,
q 214149 100000,
q 42863 20000,
q 2681 1250,
q 107323 50000,
q 214811 100000,
q 214977 100000,
q 215143 100000,
q 215309 100000,
q 8619 4000,
q 107821 50000,
q 6744 3125,
q 8639 4000,
q 108071 50000,
q 216309 100000,
q 54119 25000,
q 216643 100000,
q 21681 10000,
q 108489 50000,
q 43429 20000,
q 217313 100000,
q 217481 100000,
q 217649 100000,
q 217817 100000,
q 43597 20000,
q 109077 50000,
q 109161 50000,
q 218491 100000,
q 10933 5000,
q 218829 100000,
q 109499 50000,
q 219167 100000,
q 219337 100000,
q 109753 50000,
q 54919 25000,
q 109923 50000,
q 13751 6250,
q 110093 50000,
q 55089 25000,
q 220527 100000,
q 220697 100000,
q 55217 25000,
q 221039 100000,
q 22121 10000,
q 221381 100000,
q 13847 6250,
q 221723 100000,
q 44379 20000,
q 222067 100000,
q 111119 50000,
q 22241 10000,
q 111291 50000,
q 44551 20000,
q 222927 100000,
q 2231 1000,
q 27909 12500,
q 44689 20000,
q 111809 50000,
q 223791 100000,
q 44793 20000,
q 112069 50000,
q 28039 12500,
q 44897 20000,
q 224659 100000,
q 224833 100000,
q 225007 100000,
q 112591 50000,
q 56339 25000,
q 225531 100000,
q 112853 50000,
q 225881 100000,
q 28257 12500,
q 226231 100000,
q 113203 50000,
q 113291 50000,
q 226757 100000,
q 226933 100000,
q 227109 100000,
q 45457 20000,
q 227461 100000,
q 113819 50000,
q 113907 50000,
q 227991 100000,
q 28521 12500,
q 45669 20000,
q 114261 50000,
q 2287 1000,
q 228877 100000,
q 45811 20000,
q 14327 6250,
q 22941 10000,
q 229589 100000,
q 229767 100000,
q 45989 20000,
q 57531 25000,
q 115151 50000,
q 230481 100000,
q 11533 5000,
q 5771 2500,
q 231019 100000,
q 115599 50000,
q 115689 50000,
q 115779 50000,
q 115869 50000,
q 115959 50000,
q 116049 50000,
q 232279 100000,
q 232459 100000,
q 1454 625,
q 232821 100000,
q 116501 50000,
q 233183 100000,
q 46673 20000,
q 116773 50000,
q 7304 3125,
q 23391 10000,
q 58523 25000,
q 117137 50000,
q 29307 12500,
q 234639 100000,
q 234821 100000,
q 58751 25000,
q 235187 100000,
q 23537 10000,
q 117777 50000,
q 235737 100000,
q 235921 100000,
q 47221 20000,
q 236289 100000,
q 236473 100000,
q 236657 100000,
q 236841 100000,
q 118513 50000,
q 237211 100000,
q 59349 25000,
q 237581 100000,
q 118883 50000,
q 7436 3125,
q 238137 100000,
q 238323 100000,
q 238509 100000,
q 47739 20000,
q 238881 100000,
q 59767 25000,
q 119627 50000,
q 239441 100000,
q 59907 25000,
q 47963 20000,
q 120001 50000,
q 24019 10000,
q 120189 50000,
q 48113 20000,
q 240753 100000,
q 240941 100000,
q 24113 10000,
q 120659 50000,
q 241507 100000,
q 7553 3125,
q 48377 20000,
q 121037 50000,
q 242263 100000,
q 242453 100000,
q 121321 50000,
q 15177 6250,
q 121511 50000,
q 60803 25000,
q 243403 100000,
q 243593 100000,
q 30473 12500,
q 9759 4000,
q 122083 50000,
q 244357 100000,
q 61137 25000,
q 12237 5000,
q 61233 25000,
q 61281 25000,
q 61329 25000,
q 61377 25000,
q 245701 100000,
q 245893 100000,
q 123043 50000,
q 246279 100000,
q 30809 12500,
q 49333 20000,
q 246859 100000,
q 247053 100000,
q 247247 100000,
q 247441 100000,
q 49527 20000,
q 247829 100000,
q 31003 12500,
q 248219 100000,
q 124207 50000,
q 248609 100000,
q 62201 25000,
q 249 100,
q 49839 20000,
q 249391 100000,
q 249587 100000,
q 249783 100000,
q 12499 5000,
q 7818 3125,
q 250373 100000,
q 25057 10000,
q 250767 100000,
q 50193 20000,
q 125581 50000,
q 1571 625,
q 125779 50000,
q 62939 25000,
q 125977 50000,
q 31519 12500,
q 252351 100000,
q 5051 2000,
q 252749 100000,
q 63237 25000,
q 253147 100000,
q 253347 100000,
q 253547 100000,
q 253747 100000,
q 253947 100000,
q 254147 100000,
q 63587 25000,
q 63637 25000,
q 254749 100000,
q 5099 2000,
q 15947 6250,
q 255353 100000,
q 51111 20000,
q 255757 100000,
q 255959 100000,
q 256161 100000,
q 256363 100000,
q 128283 50000,
q 256769 100000,
q 64243 25000,
q 10287 4000,
q 128689 50000,
q 128791 50000,
q 128893 50000,
q 25799 10000,
q 129097 50000,
q 129199 50000,
q 258603 100000,
q 258807 100000,
q 64753 25000,
q 259217 100000,
q 259423 100000,
q 64907 25000,
q 129917 50000,
q 6501 2500,
q 130123 50000,
q 65113 25000,
q 260659 100000,
q 130433 50000,
q 261073 100000,
q 1633 625,
q 261487 100000,
q 52339 20000,
q 130951 50000,
q 26211 10000,
q 131159 50000,
q 262527 100000,
q 52547 20000,
q 8217 3125,
q 263153 100000,
q 131681 50000,
q 65893 25000,
q 263781 100000,
q 263991 100000,
q 264201 100000,
q 264411 100000,
q 264621 100000,
q 8276 3125,
q 265043 100000,
q 132627 50000,
q 53093 20000,
q 66419 25000,
q 8309 3125,
q 2661 1000,
q 33289 12500,
q 66631 25000,
q 16671 6250,
q 266949 100000,
q 133581 50000,
q 2139 800,
q 66897 25000,
q 133901 50000,
q 16751 6250,
q 268229 100000,
q 67111 25000,
q 134329 50000,
q 33609 12500,
q 269087 100000,
q 134651 50000
]
end MaxLeafFormal.CCRate