feat(search): close BBR via multi-block reduced Schmüdgen + i=0 refutation

[kim-em]

This PR closes the BBR Lemma 7.2 polynomial (degree-8 bivariate, integer coefficients up to ~5.8×10¹², reported by Maksym Radziwill on Zulip) via by sos, with a fully kernel-checked proof — #print axioms shows only propext, Classical.choice, Quot.sound (no native_decide).

The mechanism is Harrison's HOL Light REAL_SOS, identified by instrumenting it directly: BBR closes through the i=0 branch of REAL_NONLINEAR_PROVER's tryall loop — the strict refutation −1 = σ₀ + σ₁·(−P) proving 0 < P by contradiction — not the i=1 Artin form P = σ₀ + σ₁·(−P). The −1 target yields a far better-conditioned reduced SDP whose float Gram rounds cleanly to a rational certificate.

Two pieces:

• Multi-block reduced Schmüdgen encoder (tryReducedSchmudgenSdp and helpers). Generalises the existing single-block reduced encoding (tryReducedPureSdp) to any number of PSD blocks: polynomial-identity equations are eliminated over ℚ before CSDP, so CSDP sees a pure-PSD problem with no equality constraints — far better conditioned than the dense tryOneSdp, whose equality constraints are primal-infeasible at BBR's coefficient scale. Reached only by the closed strict-refutation, via an explicit refutation flag threaded from runClosedRefutation through runFeasibilitySearch. There is no dense fallback, and no other goal touches the encoder — every non-refutation goal stays on tryOneSdp, byte-identical to its pre-feature path.

• Closed strict-refutation path (runClosedRefutation + closeSosClosedRefutation). Searches for −1 = σ₀ + σ₁·(−p) against gs ++ [−p]. Soundness reuses the existing sos_strict_product_sound with strictGs = [], exponent = 1 (so the target is −(strictProductPoly [])¹ = −1 and the strict-positivity hypothesis is vacuous, yielding 0 < p), then le_of_lt. Tried on unconstrained closed goals after plain SOS fails — one extra CSDP solve per such hard failure, sound (a false −1 certificate is impossible).

SOSTest/BBR.lean becomes a direct by sos regression test (needs maxRoundingDenom := 1 <<< 66, the wider denominator schedule now in main via #77). The BBR module is a genuine live degree-8 SDP solve (~57s); it was a failing ~21s search before. Removing the encoder fallback returns every other module to its main timing (e.g. isolated SOSTest.DivMod 13s, vs 17s when constrained-closed goals detoured through the encoder). lake test is green.

Deliberately minimal: this is the smallest addition to main that closes BBR. It does NOT include the closed-Artin path (#76), the pivot-priority primitive, or #73's pure-SOS dispatch change — none of which BBR needs. main's pure-SOS dispatch (symmetry-gated useReducedPure, tryDirectSos) is left untouched.

🤖 Prepared with Claude Code