Adaptive rationalisation for facial-reduction recovery (beyond the fixed denominator ladder)

Follow-up from #80, which added facial-reduction rational recovery so by sos (config := { maxRefutationPower := k }) can close non-SOS non-negative polynomials (Motzkin). That PR folded in the cheap robustness fixes from review (free-variable seeding from rawY, reduction to an independent rational null basis, sign-convention/comment notes). This issue tracks the larger robustness work deferred from that review.

The recovery currently rationalises the float null-space projector against a fixed denominator ladder {1,2,3,4,6,8,12,16,24,48}. That catches Motzkin (projector rationalises at denominator 1) but is not a general design: an exact rational projector can have larger or non-divisor denominators, and the failure mode is silent (a slightly-wrong face → inconsistent system or non-PSD Gram).

Make the rationalisation adaptive — keep the fixed ladder as a cheap first pass, then:

• Common-denominator detection from each rationalised column (and from rawY for the free coordinates).
• Bounded continued fractions per normalised projector entry, with a max denominator tied to Config.maxRoundingDenomLog2.
• Denominators derived from observed entry spacings.
• (Later) LLL / PSLQ for simultaneous rational approximation of a null vector.

Related hardening, also deferred:

• Null-space tolerance. The rank cut |λ| < maxAbs·1e-4 + 1e-12 is brittle. Try a tolerance ladder (1e-6 … 1e-3) and prefer cuts with a visible spectral gap; cheap because the final certificate is exact-checked.
• Jacobi eigensolver fail-closed. The from-scratch cyclic Jacobi has hard-coded convergence (off ≤ 1e-28, 100 sweeps), no residual/orthogonality check, and a θ² overflow risk for extreme ratios. Return a converged flag + residual and bail when the decomposition is untrustworthy (rather than rationalising a garbage projector).

None of this affects soundness — Certificate.checks (decide +kernel) remains the gate; this is purely search completeness/robustness. Best validated against more non-SOS non-negative test cases than Motzkin alone (e.g. Robinson, Choi–Lam, Schmüdgen's examples).

🤖 Prepared with Claude Code

Start at the facial-reduction rational recovery used by by sos, including Config.maxRoundingDenomLog2 and the fixed denominator ladder. Review Certificate.checks as the exact validity gate, then implement and validate adaptive rationalisation and the deferred tolerance/eigensolver hardening. Done means trustworthy recovery across Motzkin and additional examples such as Robinson, Choi–Lam, and Schmüdgen's cases.