Exact-Rational Certificates in Podium: Constructions, Proofs, and Prior Art

Constructions, proofs and prior-art positioning for exact-rational certificates in the Podium library: barrier certificates, qualified Karush-Kuhn-Tucker bounds, Lyapunov certificates and sum-of-squares certificates. For nonconvex quadratically constrained quadratic programs, a checked rational dual minorant and an exactly feasible rational point bound the optimum. Coincident accepted endpoints certify global optimality; exact closure requires optimal rational witnesses. The note proves local multiplier-error bounds under stated nonsingular and singular-endpoint hypotheses, separates numerical proposal error from rational rounding, and gives an exact degree-four certificate that proves a positive S-procedure relaxation gap on a two-ball instance. The implementation tests representative instances rather than establishing general numerical success rates.