feat(search): equality cofactor symmetry reduction

[kim-em]

Context

Split off from #37 per Codex review. #37 covers σ-block symmetry for
inequality products; this issue covers the analogous reduction for
equality cofactors.

Equality cofactors qⱼ are not Gram blocks — they're linear
polynomials in a fixed monomial basis, encoded in our pipeline as
signed coefficients via the x⁺ - x⁻ LP split (see
SOS/Search.lean).
So they inherit a different kind of symmetry constraint than σ-blocks.

What the symmetry equation looks like

If a detected symmetry π ∈ Π maps equality polynomial pⱼ to p_k
(possibly with rational scalar — see normalisation note below), then
qⱼ and q_k are related by:

q_k = π · qⱼ

in the chosen monomial basis. Concretely: if qⱼ = Σ_b c_{j,b} · m_b
where m_b ranges over basis monomials, then
q_k = Σ_b c_{j,b} · (π · m_b). This is a linear-coefficient orbit
equation, not a Gram-symmetry equation.

When π · pⱼ = pⱼ (fixed cofactor), the constraint is the orbit-fixed
form c_{j, π̂(b)} = c_{j, b} on the coefficients.

Sign / scalar normalisation

p = 0 ↔ -p = 0, so symmetry detection has a choice: match equalities
up to rational scalar (more permissive), or require exact polynomial
equality (simpler). Inequalities don't get this freedom — g ≥ 0 and
-g ≥ 0 are not equivalent. Recommend exact-polynomial matching for v1.

Don't constrain the x⁺ / x⁻ split directly

Our current LP encoding splits the cofactor coefficient as c = x⁺ - x⁻
with x⁺, x⁻ ≥ 0. The decomposition isn't unique, so applying
symmetry constraints at the x⁺ / x⁻ layer is the wrong level.
Constrain the signed coefficient c directly before/inside the
sparse eliminator. In the reduced SDP path, the LP split can probably
disappear entirely: keep cofactor coefficients as unrestricted linear
variables, eliminate them with the Gram variables, reconstruct the
cofactor polynomials from the final affine solution.

Files

• SOS/Symmetry.lean — basis-permutation matrices for the cofactor
  block (smaller scope than σ-block since cofactors are linear, not
  quadratic).
• SOS/Search.lean — refactor the cofactor encoding from x⁺ - x⁻ LP
  blocks to unrestricted linear variables on the reduced path. Keep
  the LP split for the non-reduced path (back-compat).

Verification

• An equality-constrained example with non-trivial symmetry — e.g. a
  ported variant of sos.ml:1650 (w² + x² + y² + z² = 1 → (w+x+y+z)² ≤ 4, full S₄ on the four variables) — solves in the
  reduced cofactor space. (Currently closes via direct construction
  at default maxDepth := 1; symmetry should give a smaller free
  parameter count and faster solve.)
• No regression on currently-passing equality-constrained tests.

Risks

• Reconstructing the cofactor polynomial from the reduced solution
  must produce the same polynomial the verifier expects. Test
  thoroughly against the non-reduced path.
• Removing the x⁺ / x⁻ split on the reduced path is a localised
  refactor but touches the certificate-decode side. Worth pairing with
  a soundness check (the Certificate.checks polynomial-identity test
  catches any divergence).

Size

~150–300 LOC. Most of the work is the encoding refactor and the
linear-coefficient orbit equation builder; the sparse eliminator is
unchanged.

Depends on

• feat(search): σ-block symmetry reduction for constrained σ-blocks #37 (σ-block symmetry): the detection rewrite to multiset-preserving
  must land first, since the cofactor side reuses the same detector.

Out of scope

• Cross-cofactor × σ-block symmetry (symmetries that mix cone and
  ideal). Not seen in Harrison's examples.