Witness/replay support for i=0 strict-refutation certificates

The closed strict-refutation path added in #78 (SOS.Search.runClosedRefutation + closeSosClosedRefutation) closes a 0 ≤ p goal by finding a certificate −1 = σ₀ + σ₁·(−p) and reusing sos_strict_product_sound (strictGs = [], exponent = 1) to derive 0 < p, then le_of_lt. There is currently no way to freeze and replay this certificate — neither sos? nor sos_witness covers it.

Concretely:

• sos? can't suggest a replayable witness for a goal that only closes via the refutation. It emits sos_witness <cert> / sos_witness <cert> with exponent := n suggestions for the standard closed / strict-product paths, but the refutation produces its certificate inside runClosedRefutation, which sos? doesn't surface.
• sos_witness has no form that accepts a refutation certificate. The with exponent := <n> form (runSosWitnessStrictProduct) is guarded to .strict goals only ("with exponent := <nat> is only valid on strict-positivity goals"), but the refutation runs on a .closed (0 ≤ p) goal — the strictness is internal. So there's no syntax to paste the frozen −1 = σ₀ + σ₁·(−p) certificate.

Impact. Any proof that depends on the refutation path (e.g. BBR Lemma 7.2 in SOSTest/BBR.lean) must re-run the full CSDP solve + exact-rational rounding at every elaboration (~55s for BBR). With witness replay, such a goal could be frozen to an instant, solver-free check — useful for fast regression tests and for reproducibility on machines without CSDP.

Sketch of a fix.

• A sos_witness form that replays a refutation certificate on a .closed 0 ≤ p goal: elaborate the certificate, hand it to closeSosClosedRefutation (which already knows how to build the proof from a cert), skipping the search.
• Have sos? detect when a goal closed via runClosedRefutation and emit the corresponding replayable suggestion.

Noted as a follow-up during #78 review; not required for #78 itself.

Start by reading SOS.Search.runClosedRefutation and closeSosClosedRefutation, then inspect the witness handling behind sos? and sos_witness. Run the BBR example in SOSTest/BBR.lean to confirm the refutation path and its solve time. Done means a closed 0 ≤ p goal can replay a frozen refutation certificate without CSDP, and sos? suggests that replay form.