# -*- coding: utf-8 -*-
"""
AUDIT 2 — WHY did the forge exclude m != 3? Adversarial question: is the
Rigidity Theorem an artifact of the ansatz, or structural?

CLAIM TO TEST: torus-homogeneity of the design class ITSELF forces m = 3.
Set up the weight equations symbolically and solve. If (m-3)*wx = 0 falls out,
the m != 3 exclusions are explained STRUCTURALLY (no nontrivial weight system
exists), upgrading Rigidity from 'empirical sweep result' to 'theorem with a
conceptual proof'.
"""
import sympy as sp

wx, wy, wz, W1, W2, W3, m = sp.symbols('w_x w_y w_z W1 W2 W3 m')

# Ansatz terms and their weights (monomial x^i y^j z^k has weight i*wx+j*wy+k*wz).
# F1 = y^2 P(a) + z u^m : terms y^2 a^j (j=0,1,...) and z a^j (j=0..m)
# F2 = y + x y^2 Q(a) + m x z u^{m-1} : terms y ; x y^2 a^j ; x z a^j
# F3 = x R(a) - x^m z : terms x a^j ; x^m z
# Homogeneity within each component, generic nonzero coefficients:
eqs = [
    # F1: y^2 and y^2*a same weight  => wx + wy = 0
    (2*wy) - (2*wy + wx + wy),
    # F1: y^2 vs z  => 2wy = wz ; both = W1
    2*wy - wz,
    2*wy - W1,
    # F2: y vs x y^2  => wy = wx + 2wy ; = W2
    wy - (wx + 2*wy),
    wy - W2,
    # F2: y vs x z  => wy = wx + wz
    wy - (wx + wz),
    # F3: x vs x*a => wx+wy=0 (already); x = W3
    wx - W3,
    # F3: x vs x^m z  => wx = m*wx + wz
    wx - (m*wx + wz),
]
sol = sp.solve(eqs, [wy, wz, W1, W2, W3], dict=True)
print("general solution of the weight system:", sol, flush=True)
# substitute back the remaining constraint on (m, wx):
residual = [sp.simplify(e.subs(sol[0])) for e in eqs]
constraint = [r for r in residual if r != 0]
print("residual constraint(s):", constraint, flush=True)
# expect  wx*(m-3) = 0  (up to sign)
ok = any(sp.simplify(c/wx - (3 - m)) == 0 or sp.simplify(c/wx - (m - 3)) == 0
         for c in constraint)
print(f"[{'PASS' if ok else 'FAIL'}] weight-forcing: nontrivial torus (wx != 0) exists "
      f"IFF m = 3  — the m!=3 forge exclusions are structural, not empirical", flush=True)
# Confirm m=3 weights are Alpoge's: wx=1 -> (wy,wz)=(-1,-2), targets (-2,-1,1)
inst = {k: v.subs({wx: 1, m: 3}) for k, v in sol[0].items()}
print("m=3, wx=1 weight system:", inst, flush=True)
ok2 = inst[wy] == -1 and inst[wz] == -2 and inst[W1] == -2 and inst[W2] == -1 and inst[W3] == 1
print(f"[{'PASS' if ok2 else 'FAIL'}] m=3 weight system == the verified torus of Theorem 2", flush=True)