"""Exact symbolic certificate and reproducible Lean certificate generation."""
import sympy as s
from pathlib import Path
import json
zv=s.symbols('a b c d e x y z')
a,b,c,d,e,x,y,z=zv
t=s.Symbol('t')
F=s.Matrix([-a-2*x**3*y**2+x**3*z/2,-b+d+15*x**2*y**3-6*x**2*y*z,-c+e+9*x**2*y**4-3*x**2*y**2*z,-d+12*x**3*y**4-3*x**3*y**2*z,-e+4*x**3*y**5-x**3*y**3*z,a+s.Rational(3,2)*x**2*y-x,b-3*x*z-y,c+5*x*y**3-3*x*y*z-z-s.Rational(1,4)])
J=F.jacobian(zv)
points=[[0,0,0,0,0,0,0,-s.Rational(1,4)],[s.Rational(13,4),45,-s.Rational(297,8),-s.Rational(351,8),s.Rational(351,16),1,-s.Rational(3,2),s.Rational(31,2)],[-s.Rational(13,4),-45,-s.Rational(297,8),s.Rational(351,8),s.Rational(351,16),-1,s.Rational(3,2),s.Rational(31,2)]]
assert (J+s.eye(8)).charpoly(t).as_expr()==t**8
assert all(F.subs(dict(zip(zv,p)))==s.zeros(8,1) for p in points)
Path(__file__).with_suffix('.json').write_text(json.dumps({'order':list(map(str,zv)),'field':list(map(str,F)),'shifted_charpoly':str(t**8),'zeros':[[str(v) for v in p] for p in points]},indent=2)+'\n')
print('Verified the characteristic polynomial and three rational zeros.')