feat(search): σ-block symmetry reduction for constrained σ-blocks

Status

The pure-SOS symmetry path landed via PR #43 (SOS/Symmetry.lean +
the reduced search path in SOS/Search.lean:874–1100). It detects
variable-permutation symmetries that fix every input polynomial,
builds coefficient + Gram-symmetry equations, eliminates them over ℚ
before CSDP, solves in the reduced free-parameter space, and rounds
that reduced vector. Closes the three pure-SOS FIXMEs sos.ml:1819,
:1840, :1886.

What remains is extending the reduced construction to constrained
problems — σ-blocks for inequality products. This issue covers
σ-block symmetry only; equality cofactor symmetry is tracked
separately (see follow-up issue).

Important framing note (per Codex review). Harrison's
sumofsquares_general_symmetry (sos.ml:1487) and his constrained
prover real_positivnullstellensatz_general (sos.ml:1018) are
separate code paths. Harrison does not apply symmetry reduction
to the constrained Putinar/Schmüdgen builder. So this issue is an
extension beyond what Harrison does, applying his pure-SOS
symmetry idea to constrained problems. We don't get a free template
from his code — we have to design the constrained-side equations
ourselves.

What still doesn't close

Constrained-symmetric FIXMEs targeted here are evaluated as
Schmüdgen + symmetry (not Putinar-only + symmetry):

• sos.ml:1682 — interval [2,4]³ Schur. Six interval constraints
  with S₃ symmetry. Preordering enumeration (#38) is in place but
  rounding fails at default settings. Symmetry should make the SDP
  tractable.
• sos.ml:1672 — dodecahedral variant of :1682. Same shape.
• sos.ml:1690 — sharp ≥ 12 bound on :1682. Needs both higher
  maxDepth (Harrison reports 12) and symmetry.
• sos.ml:1643 — 0 ≤ x,y,z ∧ x+y+z ≤ 3 ⇒ xy+xz+yz ≥ 3xyz. Closes
  via Schmüdgen at default already, but a useful speed benchmark
  for the symmetry path (full S₃, three linear hypotheses, low
  degree).

Prerequisite: multiset-preserving symmetry detection

The current detectSymmetries in SOS/Symmetry.lean:82
requires gs.all (applyVarPerm π g = g) — every gᵢ must be
individually fixed by π. This misses interval-Schur S₃ symmetry:
the swap x ↔ y maps x - 2 to y - 2, not back to itself.

The detector has to be changed to preserve the inequality
multiset and return the induced permutation on constraint
indices. For inequalities, sign changes are not allowed; for
equalities, decide whether to match exact polynomial equality only or
to allow rational scalar multiples (since p = 0 ↔ -p = 0).

This prerequisite blocks any progress on constrained symmetry. Do it
first.

Design

Given detected symmetry group Π acting on Fin n, induce its
action on the constraint-index list, then for each (idxs, σ_S) in
Certificate.sigmas:

1. Fixed-block symmetry. If π · idxs = idxs as sorted lists
   (i.e. π fixes the constraint subset), then π acts on g_S = ∏ gᵢ
   trivially, and the σ-block Gram inherits
   Q_S[π̂(i), π̂(j)] = Q_S[i, j], provided the block basis is
   closed under π̂ (the lift of π to the σ-block's monomial basis).

2. Cross-block orbit equations. If π · idxs = idxs', then g_S
   maps to g_{S'}. The right equation is not Q_{S'} = Q_S —
   that only holds when basis order is invariant under π̂. The actual
   constraint is:

   Q_{S'}[π̂(i), π̂(j)] = Q_S[i, j]
   

   equivalently Q_{S'} = P_π Q_S P_πᵀ where P_π is the basis-permutation
   matrix. Matches the existing permuteMono convention.

3. Combined elimination. σ₀ + fixed-block + cross-block-orbit
   equations all go into the existing Harrison-style sparse
   eliminator. The free-parameter space is meaningfully smaller only
   if orbits across blocks are identified — reducing each block
   independently loses most of the win.

4. Cost matrix in the reduced space. Trace regularisation
   (identity on each σ-block in the unreduced problem) maps to a
   linear objective in the reduced free parameters, not a
   quadratic form. The current pure path computes this via traces of
   the coefficient matrices (Search.lean:1038).
   Extend the same computation across all σ-blocks.

Files

• SOS/Symmetry.lean — multiset-preserving detection; induced
  constraint-index permutation; basis-permutation matrices per
  σ-block.
• SOS/Search.lean — drop the gs.isEmpty ∧ ps.isEmpty gate on the
  reduced path (Search.lean:1232); thread σ-block bases through the
  equation builder.

Verification

• At least one of :1682, :1672 flips from FIXME to passing under
  maxSubsetCardinality := ∞.
• :1643 closes at least as fast as currently.
• :1690 may or may not flip depending on whether maxDepth = 12
  is feasible after symmetry reduction.
• No regression on currently-passing constrained tests.

Risks

• Group-action bookkeeping. Getting the constraint-index
  permutation, the basis-permutation matrix, and the cross-block
  equation indexing all consistent is the bulk of the work. The
  numerical pipeline is unchanged.
• Interaction with maxSubsetCardinality. Symmetry detection
  must run before cone enumeration, but the cone enumeration itself
  depends on the orbit structure (only one representative per orbit
  of subsets needs a σ-block). Initial implementation can ignore
  this and enumerate all subsets; the orbit-reduced enumeration is a
  follow-up.
• Basis-permutation closure. Dense monomial bases are
  permutation-closed; Newton-polytope-pruned bases may not be (a
  truncated basis might exclude some monomials that the permutation
  would map into). The detector needs to verify closure before
  emitting orbit equations.

Size

500–800 LOC including detection rewrite, σ-block equation builder,
cross-block orbit logic, certificate reconstruction, and tests.
~200–400 LOC was an underestimate.

Out of scope (separate issues)

• Equality cofactor symmetry. Cofactors qⱼ are linear
  coefficient vectors, not Gram blocks, so they inherit
  linear-coefficient orbit equalities (q_k = π · q_j when
  π · p_j = p_k), not Gram-symmetry equalities. Different variable
  model. Track in a follow-up issue.
• Cross-cofactor × σ-block symmetry. Symmetries that mix the
  cone and the ideal. Not seen in Harrison's examples.
• n > 5 symmetry detection. Current maxSymmetryArity := 5 is
  fine for everything we care about.