# -*- coding: utf-8 -*-
"""
AUDIT 1 — Independent re-verification of Paper II Theorems 1-4 from a FRESH
raw-monomial encoding (typed separately from every previous script), plus a
fiber-count cross-check using a DIFFERENT ALGORITHM (Groebner quotient
dimension + standard monomials) than the resultant-based Degree Theorem.

Adversarial posture: assume the previous scripts were wrong. Re-derive.
"""
import sympy as sp
import json, time

t0 = time.time()
x, y, z, T, s = sp.symbols('x y z T s')
A_, B_ = sp.symbols('a b')
R = {"checks": [], "ALL": True}
def ck(label, ok):
    print(f"[{'PASS' if ok else 'FAIL'}] {label}", flush=True)
    R["checks"].append({"c": label, "ok": bool(ok)})
    if not ok: R["ALL"] = False

# FRESH raw encoding (independent transcription, fully expanded monomials)
F1 = 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
F2 = y + 3*x*z + 6*x**2*y*z + 3*x**3*y**2*z + 12*x*y**2 + 9*x**2*y**3
F3 = 2*x - 3*x**2*y - x**3*z
F = [F1, F2, F3]

# cross-check the raw encoding against the factored published form
G1 = (1+x*y)**3*z + y**2*(1+x*y)*(4+3*x*y)
G2 = y + 3*x*(1+x*y)**2*z + 3*x*y**2*(4+3*x*y)
ck("encodings agree (raw expanded == factored published)",
   sp.expand(F1-G1)==0 and sp.expand(F2-G2)==0)

# --- base facts -------------------------------------------------------------
ck("det J == -2 identically (fresh Bareiss)",
   sp.expand(sp.Matrix(F).jacobian([x,y,z]).det(method='bareiss')) == -2)

# --- Theorem 1 (fold) -------------------------------------------------------
Pc = {x: s, y: -3/(2*s), z: sp.Rational(13,2)/s**2}
img = [sp.cancel(f.subs(Pc)) for f in F]
ck("fold: F(C(s)) = (-1/(4s^2), 0, 0) identically in s",
   sp.cancel(img[0] + 1/(4*s**2))==0 and img[1]==0 and img[2]==0)
res = sp.factor(sp.resultant(F2, F3, z))
fset = {str(b) for b,e in sp.factor_list(res)[1]}
ck("fold completeness: Res_z(F2,F3) factors exactly {x, 2xy+3}", fset == {'x','2*x*y + 3'})

# --- Theorem 2 (torus + descent) -------------------------------------------
sub = {x: T*x, y: y/T, z: z/T**2}
ck("torus equivariance identity in T",
   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)
def toab(e):
    p = sp.Poly(sp.expand(e), x, y, z); out = 0
    for mono, co in zip(p.monoms(), p.coeffs()):
        i,j,k = mono
        if i != j + 2*k: return None
        out += co * A_**j * B_**k
    return sp.expand(out)
P1 = toab(sp.expand(F2*F3)); P2 = toab(sp.expand(F1*F3**2))
ck("descent: F2F3, F1F3^2 in C[a,b]", P1 is not None and P2 is not None)
Jab = sp.factor(sp.Matrix([P1,P2]).jacobian([A_,B_]).det())
ck("descended Jacobian == 2*(3a+b-2)^2 (perfect square)",
   sp.expand(Jab - 2*(3*A_+B_-2)**2) == 0)
ck("collision curve descends to (-3/2,13/2) ON the fold line; axis to (0,0) OFF it",
   sp.Integer(3)*sp.Rational(-3,2)+sp.Rational(13,2)-2 == 0 and (0+0-2) != 0)

# --- Theorem 3 cross-check: fiber count via GROEBNER QUOTIENT DIMENSION ------
def fiber_groebner(t1, t2, t3):
    zs = sp.solve(F3 - t3, z)
    if len(zs) != 1: return None
    zs = zs[0]
    g1 = sp.expand(sp.numer(sp.together(F1.subs(z, zs) - t1)))
    g2 = sp.expand(sp.numer(sp.together(F2.subs(z, zs) - t2)))
    # extraneous branch x=0: F3(0,y,z)=0 != t3, so x=0 not in the true fiber;
    # confirm numerators do not create x=0 solutions:
    r0 = sp.resultant(g1.subs(x,0), g2.subs(x,0), y)
    G = sp.groebner([g1, g2], x, y, order='grevlex')
    lms = [sp.Poly(p, x, y).monoms(order='grevlex')[0] for p in G.polys]
    bx = min((m[0] for m in lms if m[1]==0), default=None)
    by = min((m[1] for m in lms if m[0]==0), default=None)
    if bx is None or by is None: return ('not-zero-dim', None, r0)
    std = [(i,j) for i in range(bx) for j in range(by)
           if not any(i>=m[0] and j>=m[1] for m in lms)]
    # eliminant squarefree check via lex
    Gl = sp.groebner([g1, g2], y, x, order='lex')
    elim = [p for p in Gl.polys if p.has_only_gens(x)] or [sp.Poly(1, x)]
    e = elim[0].as_expr()
    k = min(m[0] for m in sp.Poly(e, x).monoms())
    e = sp.expand(e / x**k)
    sf = sp.degree(sp.cancel(e / sp.gcd(e, sp.diff(e, x))), x)
    return (len(std), int(sf), r0)

random_targets = [(sp.Rational(5,2), sp.Rational(-7,3), sp.Rational(11,4)),
                  (sp.Rational(-9,5), sp.Rational(4,7),  sp.Rational(3,2)),
                  (sp.Rational(13,6), sp.Rational(1,5),  sp.Rational(-8,3))]
ok3 = True
for t1,t2,t3 in random_targets:
    out = fiber_groebner(t1,t2,t3)
    print(f"        target ({t1},{t2},{t3}): quotient-dim={out[0]}, squarefree-eliminant-deg={out[1]}, x0-branch-res={out[2]!=0}", flush=True)
    if out[0] != 3 or out[1] != 3 or out[2] == 0: ok3 = False
ck("GROEBNER cross-check: quotient dim = 3 AND squarefree eliminant deg = 3 at 3 targets "
   "(independent algorithm agrees with Degree Theorem)", ok3)

R["elapsed"] = round(time.time()-t0, 2)
json.dump(R, open('post-jc-program/audit/audit1.json','w'), indent=2)
print(f"\nAUDIT 1: ALL={R['ALL']}  ({R['elapsed']}s)", flush=True)