"""Exact verifier for the single-u-mode cyclic rigidity theorem.

For integers m,K>=1, put
  g(u,y)=a0 + u^K a(y),  a0 != 0.
If H is polynomial and
  D(H)=m*u*H_u*g_y - H_y*(g+m*u*g_u) = c != 0,
then a(y)=0, hence g is constant.

The proof is coefficient-exact. This script independently checks the general
coefficient recurrence symbolically and stress-tests finite truncations over Q.
"""
from __future__ import annotations
import json, random, hashlib, platform
from pathlib import Path
import sympy as sp

u,y,m,K,a0,c=sp.symbols('u y m K a0 c', nonzero=True)
# General coefficient identity for a formal finite H and symbolic fixed integer m,K

def direct_coeff_identity(mi:int, Ki:int, N:int=8):
    hs=[sp.Function(f'h{i}')(y) for i in range(N+1)]
    A=sp.Function('a')(y)
    H=sum(hs[i]*u**i for i in range(N+1))
    g=a0+u**Ki*A
    D=sp.expand(mi*u*sp.diff(H,u)*sp.diff(g,y)-sp.diff(H,y)*(g+mi*u*sp.diff(g,u)))
    for n in range(N+1):
        got=sp.expand(D).coeff(u,n)
        want=-a0*sp.diff(hs[n],y)
        if n>=Ki:
            want += mi*(n-Ki)*hs[n-Ki]*sp.diff(A,y) - (1+mi*Ki)*A*sp.diff(hs[n-Ki],y)
        assert sp.simplify(got-want)==0, (mi,Ki,n,got,want)

for mi in range(1,8):
    for Ki in range(1,6):
        direct_coeff_identity(mi,Ki)

# Degree recurrence on the forced residue class n=lK.
# Normalize a0=c=1 only for this degree test; h0'=-1.
def forced_chain(mi:int, Ki:int, A:sp.Expr, L:int):
    f=[-y]
    for ell in range(1,L+1):
        rhs=sp.expand(mi*Ki*(ell-1)*f[ell-1]*sp.diff(A,y)
                      -(1+mi*Ki)*A*sp.diff(f[ell-1],y))
        f.append(sp.integrate(rhs,y))
    return [sp.expand(z) for z in f]

random.seed(20260721)
stress=[]
for mi in range(1,8):
  for Ki in range(1,6):
    for d in range(0,6):
      # nonzero polynomial of exact degree d
      coeff=[sp.Rational(random.randint(-5,5) or 1, random.randint(1,5)) for _ in range(d+1)]
      coeff[-1]=sp.Rational(random.randint(1,5),random.randint(1,5))
      A=sum(coeff[j]*y**j for j in range(d+1))
      chain=forced_chain(mi,Ki,A,6)
      degrees=[sp.Poly(z,y).degree() for z in chain]
      expected=[0 if ell==0 and False else ell*d+1 for ell in range(7)]
      # f0=-y has degree 1, matching ell*d+1.
      assert degrees==expected,(mi,Ki,d,degrees,expected)
      stress.append({'m':mi,'K':Ki,'deg_a':d,'degrees':degrees})

cert={
 'status':'PASS',
 'theorem':'single-u-mode cyclic rigidity',
 'identity_grid':{'m':'1..7','K':'1..5','checks':35},
 'degree_stress':{'cases':len(stress),'chain_length':7},
 'sympy':sp.__version__,
 'python':platform.python_version(),
 'key_formula':"f_l' = m*K*(l-1)*a'*f_{l-1} - (1+m*K)*a*f_{l-1}'",
 'degree_formula':"deg(f_l)=l*deg(a)+1 for every l>=0 when a!=0",
}
out=Path(__file__).with_name('single_u_mode_certificate.json')
out.write_text(json.dumps(cert,indent=2)+'\n',encoding='utf-8')
print(json.dumps(cert,indent=2))
print('certificate_sha256',hashlib.sha256(out.read_bytes()).hexdigest())