artifacts/claim2/method.md

# Claim C1 method

This route replaces the rejected single-anisotropic-Gaussian spot check with an
independently reconstructed symbolic derivation:

1. `M^T M=I` gives `||Mx||^2=||x||^2` pointwise, hence equality of expectations.
2. Haar left invariance gives `QMX =_d MX` for every orthogonal `Q`, which is the
   definition of spherical symmetry.
3. Joint convexity of hockey-stick divergence under mixtures follows from
   convexity of the positive-part function.
4. Conditioning on `M`, applying the bijection `M^T`, and using
   `||M^Tv||=||v||` bounds every symmetrized shift by the original
   worst-direction supremum.

The verifier checks the dependency DAG, exact symbolic isometry algebra, the
two exhaustive sign cases for positive-part convexity, and three intentionally
invalid mutations.