"""Adversarial search against the cyclic-rigidity edge proof.
Looks for a nonconstant edge A and nonzero Phi making B=0 or (sigma=1) B constant.
Exact coefficient solving over Q via Groebner bases at bounded degrees.
"""
import sympy as s, json, hashlib
from pathlib import Path
t=s.symbols('t'); cases=[]
for m in range(1,6):
 for p in range(0,5):
  for q in range(1,5):
   if s.gcd(p,q)!=1:continue
   for r in range(q):
    for ss in range(1,5):
     sigma=s.Rational(q*ss-p*r,q)
     if sigma<1: continue
     for D in range(1,4):
      for N in range(0,4):
       aa=s.symbols(f'a0:{D}')
       ff=s.symbols(f'f0:{N+1}')
       A=t**D+sum(aa[i]*t**i for i in range(D))
       Phi=t**N+sum(ff[i]*t**i for i in range(N)) if N else s.Integer(1)
       B=s.expand(-p*t*A*s.diff(Phi,t)-ss*A*Phi-m*q*sigma*t*s.diff(A,t)*Phi)
       # For sigma>1 require B=0. For sigma=1 allow arbitrary constant.
       coeffs=[]
       poly=s.Poly(B,t)
       for power in range(poly.degree()+1):
        if sigma>1 or power>0: coeffs.append(poly.coeff_monomial(t**power))
       G=s.groebner(coeffs,*(list(aa)+list(ff)),order='grevlex') if aa or ff else None
       inconsistent=(not coeffs) is False and (G is not None and any(z.as_expr()==1 for z in G.polys))
       # Leading coefficient gives inconsistency in every case; assert solver sees it.
       assert inconsistent,(m,p,q,r,ss,D,N,B,coeffs,G)
       cases.append((m,p,q,r,ss,D,N))
cert={'status':'PASS','adversarial_degree_cases':len(cases),'ranges':{'m':'1..5','p':'0..4','q':'1..4','deg_A':'1..3','deg_Phi':'0..3'}}
out=Path(__file__).with_name('adversarial_certificate.json');out.write_text(json.dumps(cert,indent=2)+'\n')
print(json.dumps(cert,indent=2));print('sha256',hashlib.sha256(out.read_bytes()).hexdigest())