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

[kim-em]

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 (feat(search): drop hard-coded Putinar restriction; enumerate constraint-product monoid #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.

[kim-em]

Rewrote issue body with the post-mortem from PR #42 and the actual plan (eliminate equalities over ℚ → reduced SDP in free orbit parameters → round in the small space).

PR #42 is closed; the issue-37 branch remains for reference. SOS/Symmetry.lean there (applyVarPerm, permuteMono, detectSymmetries, basisPermutation, orbit union-find) is reusable for the new plan — start a fresh branch and cherry-pick that file.

[kim-em]

Claiming this. I’ll prepare the reduced symmetric SDP implementation and open a draft PR.

[kim-em]

Opened draft PR #43 with the reduced symmetric pure-SOS infrastructure. It currently closes the Z₂×Z₂ Harrison case () and leaves the S₃ rounding issue (/) called out as remaining work.

[kim-em]

Opened draft PR #43 with the reduced symmetric pure-SOS infrastructure. It currently closes the Z₂×Z₂ Harrison case (sos.ml:1886) and leaves the S₃ rounding issue (sos.ml:1819/:1840) called out as remaining work.

[kim-em]

Follow-up investigation found the missing Harrison details: basis order, one-pass sparse elimination rather than RREF, and the homogeneous constant-variable sign convention. I force-pushed PR #43 with those fixes. lake build SOSTest now passes with sos.ml:1819, :1840, and :1886 enabled.

[kim-em]

Codex (via /second-opinion) reviewed an earlier draft of this issue. Substantive corrections, all folded into the rewrite above; equality cofactor symmetry split out to #56. Summary of the review:

Framing correction

Harrison does not apply symmetry reduction to constrained problems. sumofsquares_general_symmetry (sos.ml:1487) and real_positivnullstellensatz_general (sos.ml:1018) are separate code paths. This issue is an extension beyond Harrison, applying his pure-SOS symmetry idea to the constrained builder. Original wording suggested "mirror what Harrison does"; that was wrong.

Math corrections

1. Cross-block orbit equation. I had Q_a = Q_b; correct form is Q_{πS}[π̂(i), π̂(j)] = Q_S[i, j], i.e. Q_{πS} = P_π Q_S P_πᵀ. Literal equality only when basis order is invariant under π̂ (generally false).

2. Equality cofactors are linear, not Gram. I said cofactors "inherit Gram-symmetry reduction" — wrong. They inherit linear-coefficient orbit constraints q_k = π · q_j. Split into feat(search): equality cofactor symmetry reduction #56.

3. Cost matrix. Trace regularisation maps to a linear objective in reduced coordinates, not a quadratic form.

Prerequisite I missed

detectSymmetries in SOS/Symmetry.lean:82 requires gs.all (applyVarPerm π g = g) — every gᵢ individually fixed. This misses interval-Schur S₃ because x - 2 ↔ y - 2 is a multiset-preserving swap, not a per-element fix. The detector has to be rewritten to preserve the inequality multiset and return the induced constraint-index permutation before any of this issue's σ-block work can fire.

Target framing correction

sos.ml:1682, :1672, :1690 are stress tests for Schmüdgen + symmetry, not Putinar-only + symmetry. Harrison's REAL_SOS always uses preordering (real_positivnullstellensatz_general false), so the original phrasing "constrained-symmetric Harrison cases" obscured that two features are needed together. :1643 reframed as a speed benchmark rather than a "Putinar + symmetry closes it" target.

Scope split

Per Codex: split σ-block symmetry from equality cofactor symmetry. They have different variable models (Gram vs. linear coefficient vector) and different soundness obligations. Done — cofactor symmetry is now #56.

Size revision

200–400 LOC was an underestimate. Realistic estimate: 500–800 LOC for σ-blocks alone, including multiset detection, induced index permutation, cross-block orbit equations, basis-permutation closure checks, certificate reconstruction, and tests.

Confirmed-as-stable

• Fixed-block constraint Q_S[π̂(i), π̂(j)] = Q_S[i, j] is mathematically right.
• Combined elimination over coefficient + symmetry + cofactor equations is sound (just rational linear equations).
• The bulk of the work is group-action bookkeeping; the numerical pipeline is unchanged.