[codex] add reduced symmetric pure SOS path

[kim-em]

Summary

Implements the pure-SOS part of #37 using Harrison-style symmetry reduction. The search now detects non-trivial variable-permutation symmetry on pure σ₀ goals, builds coefficient and Gram-symmetry equations over ℚ, eliminates them before CSDP, solves in the reduced free-parameter space, and rounds that reduced vector before exact LDL verification.

The important compatibility details are that the reduced path uses Harrison’s pure newton_polytope basis order, his one-pass sparse equation eliminator rather than RREF, and the same homogeneous constant-variable sign convention. Those details are what make the S₃ examples round.

This enables the Harrison regressions sos.ml:1819, sos.ml:1840, and sos.ml:1886.

Validation

• lake build SOSTest

Notes

The current implementation covers pure SOS (gs = [], ps = []) with non-trivial symmetry. Extending the same reduced construction to Putinar/equality blocks remains future work for the constrained examples in #37.