# -*- coding: utf-8 -*-
"""AUDIT 2b — weight-forcing lemma, fixed staging.
Solve the consistent subsystem for the dependent weights, THEN evaluate the
final homogeneity constraint. Expect residual == (3 - m)*wx: a nontrivial
torus exists iff m = 3."""
import sympy as sp
wx, wy, wz, W1, W2, W3, m = sp.symbols('w_x w_y w_z W1 W2 W3 m')

core = [wx + wy,            # F1: y^2 vs y^2*a  (and F3: x vs x*a)
        2*wy - wz,          # F1: y^2 vs z*u^m
        2*wy - W1,
        wy - W2,            # F2: y
        wy - (wx + wz),     # F2: y vs x*z*u^{m-1}
        wx - W3]            # F3: x
sol = sp.solve(core, [wy, wz, W1, W2, W3], dict=True)
print("dependent weights:", sol[0], flush=True)
final = wx - (m*wx + wz)    # F3: x vs x^m z
residual = sp.expand(final.subs(sol[0]))
print("final homogeneity constraint reduces to:", residual, "= 0", flush=True)
ok = sp.simplify(residual - (3 - m)*wx) == 0
print(f"[{'PASS' if ok else 'FAIL'}] residual == (3-m)*wx  =>  nontrivial torus exists IFF m=3.", flush=True)
inst = {k: v.subs(wx, 1) for k, v in sol[0].items()}
ok2 = inst == {wy: -1, wz: -2, W1: -2, W2: -1, W3: 1}
print(f"[{'PASS' if ok2 else 'FAIL'}] m=3, wx=1 gives exactly the verified torus (1,-1,-2)->(-2,-1,1)", flush=True)
print("\nLEMMA (verified): the m != 3 forge exclusions are STRUCTURAL — no nontrivial")
print("weight system makes the design class homogeneous unless m = 3. Rigidity is")
print("not an empirical accident of the sweep; it is representation theory.", flush=True)