feat(search): closed Artin-form Positivstellensatz path

[kim-em]

This PR adds an opt-in iterative-deepening fallback that proves 0 ≤ p via an Artin-form Positivstellensatz certificate of the shape p^{2k+1} = σ₀ + σ₁ · (−p) + … — a closed cert for p^exponent against the augmented inequality list gs ++ [−p], with exponent odd. Soundness is by contradiction on p < 0: an odd power of a negative real is negative, contradicting the cert's non-negativity at φ. Closes #75.

The fallback is enabled per call via sos (config := { maxArtinExponent := <n> }); the default 0 keeps it off so the existing test suite isn't slowed by extra CSDP solves on legitimate-failure cases. sos_witness gains a closed-Artin dispatch on with exponent := <odd n>.

The BBR Lemma 7.2 polynomial — the motivating target — remains beyond reach at the denominator schedule and relaxation depth we currently expose; closing it for real likely needs both Harrison-scale denominators (2^66) and a much larger relaxation depth. The regression test stays as fail_if_success and now documents the new path.

🤖 Prepared with Claude Code

[kim-em]

Status:

In:

• sos_closed_artin_sound (SOS/Verifier.lean): odd-power-of-negative contradiction.
• runClosedArtin (SOS/Search.lean): iterates odd exponents 1, 3, …, maxExponent over runFeasibilitySearch with augmented list gs ++ [−p].
• closeSosClosedArtin (SOS/Tactic.lean) and dispatch behind Config.maxArtinExponent (default 0, opt-in).
• sos_witness <cert> with exponent := <odd n> now dispatches to the closed-Artin path on closed goals; even exponents are rejected with a clear error.
• Hand-rolled sos_witness regression tests covering exponent 1, exponent 3, and the even-rejection error.

Out of reach: BBR Lemma 7.2. I ran the actual probe with sos (config := { maxArtinExponent := 3, maxDepth := 2, maxRoundingDenom := 2^28 }). 62 seconds of CSDP work, then search failed to find a certificate. The blockers are the ones the issue flagged:

• Coefficient magnitude: p has coefficients ~5×10¹², so p^3 carries ~10³⁸. Rounding the float Gram CSDP returns to an exact rational matrix needs denominators beyond our 2^24/2^28 cap. Harrison's REAL_SOS reportedly closes BBR around 2^66.
• Basis growth: at exponent 3 on 2 variables, σ₀ basis is 91 monomials, gram 91×91 — solvable in CSDP, but exacerbates the rounding problem.
• decide +kernel on the final identity check would also become very expensive at the coefficient magnitudes we'd see, even if a Gram round were found.

The BBR regression test stays as fail_if_success and documents the path now available.

Follow-up to actually close BBR (not in this PR):

1. Wider denominator schedule — extend niceDenominators past 2^24, and let Config.maxRoundingDenom go to ~2^64. This is the most direct unblock.
2. Either bigger maxDepth or a Harrison-style "deepen σ-block bases per exponent" inside runClosedArtin instead of a single fixed depth across the iteration.
3. Possibly: scale-aware SDP conditioning that accounts for the target^exponent blow-up before handing to CSDP, beyond the mats[0]/b shifts in conditionProblem.

Codex review note (deferred from this PR): the automatic-fallback path (search + dispatch end-to-end) doesn't have an integration test — just the closer is covered by sos_witness tests. I tried a plain 0 ≤ x from 0 ≤ x^3 integration example, but the build error swallowed by Lake's --json output mode prevented quick debugging, so I dropped it. Would be a one-line addition once the swallowed-error problem is sorted.

[kim-em]

Trimmed the obsolete content: dropped the two BBR-specific commits (the sos_witness proof from Maksym's explicit decomposition, and the cbv/decide-axioms docs). BBR Lemma 7.2 is now closed on main by #78 via the live i=0 strict-refutation (−1 = σ₀ + σ₁·(−P)), which is far better-conditioned than the Artin form — so that hand-decomposition proof is fully superseded.

What remains here is the substance for #75: the closed Artin-form path (runClosedArtin, sos_closed_artin_sound, closeSosClosedArtin, maxArtinExponent), proving 0 ≤ p via p^{2k+1} = σ₀ + σ₁·(−p).

No pressing reason to merge this right now. It's genuinely complementary to #78's refutation — Artin proves 0 ≤ p including targets that touch zero, whereas the refutation proves the strict 0 < p — but post-#78 there's no failing target that needs the boundary-touching capability. If revived it would also need rebasing onto current main: the remaining commit predates #78, so its dispatch in Tactic.lean and its SOSTest/BBR.lean docstring (which still describes BBR as out of reach) are both stale.

Leaving open as a deferred follow-up against #75.