feat(search): Harrison-style reduced encoding for closed pure-SOS [DRAFT]#73
Closed
kim-em wants to merge 2 commits into
Closed
feat(search): Harrison-style reduced encoding for closed pure-SOS [DRAFT]#73kim-em wants to merge 2 commits into
kim-em wants to merge 2 commits into
Conversation
This PR makes the Harrison-style parameterised encoding
(`tryReducedPureSdp`) the only pure-SOS-closed search path, generalised
to arbitrary relaxation depth and target shape, and adds CSDP-data
scaling for targets with large integer coefficients.
Changes:
* `tryReducedPureSdp`:
- Drops the `extraDeg ≠ 0` short-circuit. The basis now comes from
the existing `basisStrategy.basisAt target basisDeg` (same as
`tryOneSdp`) instead of a fixed `harrisonNewtonBasis`. Applies
`dropConstant` filtering to match `buildBlocks`.
- Scales `mats[0]` (the particular solution that absorbs target
coefficients) by `1/max(|entry|)` before handing to CSDP, and
scales the recovered free vector back by the same factor. Targets
like BBR Lemma 7.2 (`5.8 × 10¹²` coefficients) cause CSDP to
return "dual infeasible" (ret=2) without this scaling.
- Bounded by a new `Config.maxReducedGramVars : Nat := 2500` knob:
above this the reduced ℚ Gauss-Jordan in `gramParam` is expensive,
and the path returns `none` so the outer loop moves on.
* `runFeasibilitySearchCore`:
- `useReducedPure := gs.isEmpty && ps.isEmpty && isClosedGoal`
(was: `gs.isEmpty ∧ ps.isEmpty ∧ symmetries.size > 1`).
- Pure-SOS-closed goals go only through the reduced encoding, no
dense fallback per iteration. Iterative deepening across
`extraDeg` and basis strategies is the only recovery — matches
Harrison's `sumofsquares_general_symmetry`.
* `tryDirectSos` deleted (was just a fast `tryOneSdp` specialisation,
now subsumed by the reduced path).
* `buildReducedProblem`'s docstring updated — the encoding is now the
general pure-SOS solver, not just the `Z₂×Z₂` symmetric case.
* `Config.maxReducedGramVars` threaded through `runSearch` /
`runFeasibilitySearch` / `runStrict` / `runStrictProduct`.
The BBR Lemma 7.2 polynomial (https://arxiv.org/abs/2603.05609) does
not yet close: CSDP now returns ret=0/3 (was ret=2 pre-scaling), but
rounding the float free vector to any rational in the schedule
produces a Gram just outside the PSD cone — even with shrinkage
toward `y=0`. Closing BBR needs shrinkage toward the analytic centre
of the feasible set (a second SDP, or a different solver), which is
follow-up work. `SOSTest/BBR.lean` stays `fail_if_success` with an
updated comment documenting the remaining PSD-margin gap.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Investigated divergence (2) from issue #74: tried Harrison's uniform two-axis scaling (sos.ml:634) on our reduced encoding. CSDP returned ret=7 (primal infeasible) on every depth. Reason: Harrison's mats[0] and mats[k+1] have similar magnitudes after his Gauss-Jordan, so uniform scaling conditions both. In OUR encoding, mats[0] is the particular solution (entries scale with target coefficients, ~5e12 for BBR) while mats[k+1] is the null-space basis (~O(1)). Uniform scaling by 2^(-23) sends mats[k+1] to ~1e-7, below CSDP's working range. The asymmetric scaling already in place (divide mats[0] by max(|entry|), leave mats[k+1] alone) is the correct adaptation. Updates only the docstring; no code change. See #74 (comment) for the full investigation note. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Collaborator
Author
|
Closing: this was an exploratory branch for the pure-SOS reduced-encoding path while chasing BBR Lemma 7.2. BBR is now closed on Abandoning rather than parking. If a concrete pure-SOS target later fails where this path would help, it's easy to revive from the branch history. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR makes Harrison's parameterised reduced encoding (`tryReducedPureSdp`) the only pure-SOS-closed search path, generalised to arbitrary relaxation depth and target shape, and adds CSDP-data scaling for targets with large integer coefficients. Diagnostic context for the BBR Lemma 7.2 polynomial reported on Zulip by Maksym Radziwill.
Why draft
BBR does not close with this PR alone — it needs a closed-nonnegativity Positivstellensatz path (Artin form) we don't yet have. Tracked in #75. The change here is architectural cleanup that's necessary groundwork: `tryReducedPureSdp` was previously gated to non-trivial symmetries and depth 0, blocking any pure-SOS use beyond a narrow regime.
Changes
`tryReducedPureSdp`
`runFeasibilitySearchCore`
Other
Validation
🤖 Prepared with Claude Code