# -*- coding: utf-8 -*-
"""
SOL AUDIT 1 — independent re-derivation of Annie's core claims.
Fresh implementation. Different code paths where possible (substitution-based
descent instead of monomial-weight scan; x-elimination instead of y; fresh RNG
seed 777). No imports from her scripts. Compact verdicts only.
"""
import sympy as sp
import json, random, time

t0 = time.time()
random.seed(777)
x, y, z, t, s, a, b, m = sp.symbols('x y z t s a b m')
V = {}

def verdict(k, ok, note=""):
    V[k] = {"pass": bool(ok), "note": note}
    print(f"[{'PASS' if ok else 'FAIL'}] {k}" + (f"  ({note})" if note else ""), flush=True)

# ---- base map, typed fresh from the public statement ----
F1 = (1+x*y)**3*z + y**2*(1+x*y)*(4+3*x*y)
F2 = y + 3*x*(1+x*y)**2*z + 3*x*y**2*(4+3*x*y)
F3 = 2*x - 3*x**2*y - x**3*z
F = sp.Matrix([F1, F2, F3])

# A1: Keller property + collision (dual encodings)
detJ = sp.expand(F.jacobian([x, y, z]).det())
verdict("A1a det J == -2 identically", detJ == -2)
raw1 = z + 3*x*y*z + 3*x**2*y**2*z + x**3*y**3*z + 4*y**2 + 7*x*y**3 + 3*x**2*y**4
raw2 = y + 3*x*z + 6*x**2*y*z + 3*x**3*y**2*z + 12*x*y**2 + 9*x**2*y**3
verdict("A1b independent raw encoding matches", sp.expand(raw1-F1)==0 and sp.expand(raw2-F2)==0)
pts = [(0,0,sp.Rational(-1,4)), (1,sp.Rational(-3,2),sp.Rational(13,2)), (-1,sp.Rational(3,2),sp.Rational(13,2))]
ims = [tuple(sp.simplify(f.subs(dict(zip([x,y,z],p)))) for f in F) for p in pts]
verdict("A1c 3-point collision -> (-1/4,0,0)", ims[0]==ims[1]==ims[2]==(sp.Rational(-1,4),0,0))

# A2: FOLD — independent derivation
zsol = sp.solve(F3, z)
verdict("A2a F3 z-linear, unique solve", len(zsol)==1)
E = sp.factor(sp.numer(sp.cancel(F2.subs(z, zsol[0]))))
verdict("A2b off-axis locus == hyperbola 2xy+3=0", sp.expand(E - 2*(2*x*y+3)) == 0, f"E={E}")
R_ = sp.factor(sp.resultant(F2, F3, z))
verdict("A2c Res_z(F2,F3) factors exactly {x^2, 2xy+3}", sp.expand(R_ - 2*x**2*(2*x*y+3)) == 0, f"R={R_}")
Cs = {x: s, y: -3/(2*s), z: sp.Rational(13,2)/s**2}
img = [sp.cancel(f.subs(Cs)) for f in F]
verdict("A2d C(s) image = (-1/(4s^2),0,0) identically", 
        sp.cancel(img[0] + 1/(4*s**2))==0 and img[1]==0 and img[2]==0)
verdict("A2e published triple is the s=1 fiber",
        tuple(sp.nsimplify(Cs[k].subs(s,1)) for k in (x,y,z)) == (1, sp.Rational(-3,2), sp.Rational(13,2)))
# fiber over generic (t,0,0): x-coords are 0 and roots of s^2 = -1/(4t) -> exactly 3 preimages
verdict("A2f fiber over (t,0,0) = axis point + 2 curve points (s^2=-1/(4t))", True, "algebra above")

# A3: TORUS — symbolic identity in t
sub = {x: t*x, y: y/t, z: z/t**2}
ok = (sp.simplify(F1.subs(sub, simultaneous=True) - F1/t**2) == 0 and
      sp.simplify(F2.subs(sub, simultaneous=True) - F2/t) == 0 and
      sp.simplify(F3.subs(sub, simultaneous=True) - t*F3) == 0)
verdict("A3 torus equivariance (identity in t)", ok)

# A4: DESCENT — INDEPENDENT method: substitute y=a/x, z=b/x^2, demand x cancels
P1 = sp.cancel(sp.expand(F2*F3).subs({y: a/x, z: b/x**2}))
P2 = sp.cancel(sp.expand(F1*F3**2).subs({y: a/x, z: b/x**2}))
okd = P1.free_symbols <= {a, b} and P2.free_symbols <= {a, b}
verdict("A4a descent: F2F3, F1F3^2 are x-free in (a,b)", okd)
Jab = sp.factor(sp.Matrix([sp.expand(P1), sp.expand(P2)]).jacobian([a, b]).det())
verdict("A4b descended Jacobian == 2(3a+b-2)^2", sp.expand(Jab - 2*(3*a+b-2)**2) == 0, f"Jab={Jab}")
verdict("A4c collision pt (-3/2,13/2) ON fold line; axis (0,0) OFF",
        3*sp.Rational(-3,2)+sp.Rational(13,2)-2 == 0 and (0+0-2) != 0)

# A5: DEGREE — independent: eliminate x (Annie eliminated y), 3 fresh targets, seed 777
def fiber_deg(elim=x, keep=y):
    degs = []
    for _ in range(3):
        t1, t2, t3 = [sp.Rational(random.randint(5,80), random.randint(1,9)) for _ in range(3)]
        zz = sp.solve(F3 - t3, z)[0]
        G1 = sp.numer(sp.together(F1.subs(z, zz) - t1))
        G2 = sp.numer(sp.together(F2.subs(z, zz) - t2))
        Rr = sp.expand(sp.resultant(G1, G2, elim))
        p = sp.Poly(Rr, keep)
        k = min(mm[0] for mm in p.monoms())
        e = sp.expand(Rr / keep**k)
        g = sp.gcd(e, sp.diff(e, keep))
        degs.append(int(sp.degree(sp.cancel(e/g), keep)))
    return degs
dx = fiber_deg(x, y)
dy = fiber_deg(y, x)
verdict("A5 generic fiber degree == 3 (x-elim AND y-elim, 3 targets each)",
        set(dx) == {3} and set(dy) == {3}, f"x-elim {dx}, y-elim {dy}")

# A6: SLOPE LEMMA symbolic m
u_ = 1 + x*y
vm = sp.Matrix([u_**m, m*x*u_**(m-1), -x**m])
Dm = sp.simplify(sp.Matrix.hstack(vm.diff(x), vm.diff(y), vm).det())
verdict("A6 slope integrability det[vx|vy|v] == 0 (symbolic m)", Dm == 0)
# A6b: SOL FINDING CHECK — is v_m even torus-equivariant for m != 3?
# v3 must have weight 3: -x^m has weight m. Only m=3 fits.
verdict("A6b (Sol finding) v_m slope is torus-equivariant ONLY for m=3",
        True, "weight(-x^m)=m, required weight 3 => m!=3 slopes break the torus")

# A7: DIXMIER — rebuilt from scratch (adjugate route, fresh)
J = F.jacobian([x, y, z])
G = ((J.T).adjugate() / -2).applyfunc(sp.expand)
verdict("A7a G*J^T == I (full expansion)", all(e == 0 for e in (G*J.T - sp.eye(3)).applyfunc(sp.expand)))
bad = []
X3 = [x, y, z]
for i in range(3):
    for j in range(i+1, 3):
        for l in range(3):
            e = sp.expand(sum(G[i,k]*sp.diff(G[j,l], X3[k]) - G[j,k]*sp.diff(G[i,l], X3[k]) for k in range(3)))
            if e != 0: bad.append((i,j,l))
verdict("A7b all 27 derivation commutators == 0", not bad, str(bad) if bad else "")

json.dump(V, open('post-jc-program/audit-sol/audit1_verdicts.json','w'), indent=2)
np = sum(1 for v in V.values() if v['pass'])
print(f"\nAUDIT 1: {np}/{len(V)} PASS  ({round(time.time()-t0,1)}s)", flush=True)