"""Exact local identities; does not certify the entire manuscript or Lean."""
from pathlib import Path
import hashlib, json
import sympy as z

root = Path(__file__).resolve().parents[1]
h,u,v,w,x,y,s,U,G,W,alpha,beta,T = z.symbols('h u v w x y s U G W alpha beta T')
S = lambda H,A,B,C: 2*A**3*B+3*A**4*C+H*(B**2-3*A**2*C**2)+H**2*C**3
p = lambda X,Y,Q: -2*Q**2*X+3*Q*Y**2-3*Q**3*Y
checks = {}
def zero(name, value):
    checks[name] = bool(z.expand(value) == 0)
    assert checks[name], name
xx,yy,ss = u**3+h*v,-u**2+h*w,S(h,u,v,w)
zero('cusp_identity', xx**2+yy**3-h*ss)
zero('shift_identity', (x+s**3)**2+(y-s**2)**3-(x**2+y**3-s*p(x,y,s)))
# Polynomial division by the monic relation in U, over a coefficient field.
relation = h*W-y-U**2
_, rem = z.div(z.expand(S(h,U,G-U*W,W)-(h*G**2-2*U*y*G+y**2*W)), relation, U)
zero('linearized_S_mod_relation', rem)
zero('compatibility_identity', y**2*(y+U**2)-h*(s-h*G**2+2*U*y*G)-((h*G-y*U)**2+y**3-h*s))
aa=1+2*s**2*x+4*s**5
bb=(3*s**3-3*s*y)*(1+2*s**2*x)-4*s**4*y**2
zero('explicit_bezout_certificate', aa*h+bb*y-1-((1+2*s**2*x)*(h-1-p(x,y,s))-4*s**4*(x**2+y**3-s*h)))
zero('squared_coefficient_certificate', alpha*(1+beta*y)*h+beta**2*y**2-1-(alpha*h+beta*y-1)*(1+beta*y))
zero('UG_relation_certificate', h*(y*T+alpha*x)-y*(h*T-beta*x)-x-(alpha*h+beta*y-1)*x)
zero('T_composite_certificate', alpha*(h*T-beta*x)+beta*(y*T+alpha*x)-T-(alpha*h+beta*y-1)*T)
F=h-p(xx,yy,ss)-1
P={h:z.Integer(2),u:0,v:-z.Rational(1,2),w:z.Rational(1,2)}
gradient=[z.diff(F,k).subs(P) for k in [h,u,v,w]]
checks['critical_gradient_exact'] = gradient == [0,0,0,0]
checks['critical_fibre_exact'] = F.subs(P) == -1
assert all(checks.values())
record={'method':'exact symbolic polynomial arithmetic; local certificates only',
        'sympy_version':z.__version__, 'source_sha256':hashlib.sha256((root/'sources/native/build/paper.tex').read_bytes()).hexdigest(),
        'checks':checks,'critical_gradient':list(map(str,gradient)),'critical_fibre':str(F.subs(P))}
(root/'outputs/independent_calculations.json').write_text(json.dumps(record,indent=2)+'\n')
print(json.dumps(record,indent=2))