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

This note collects the constructions, proofs, and prior-art positioning behind the exact-rational certificates in the Podium library (podium.verify): barrier certificates for abort safety, Karush-Kuhn-Tucker certificates for the online convex solves, control-Lyapunov certificates, sum-of-squares certificates, and an optimality-gap bracket for nonconvex quadratically constrained quadratic programs. None of the underlying certificate mathematics is new; the note documents the exact instantiation, its verification, and its relation to the exact-SOS/moment, rational-SDP-recovery, and QCQP-duality literature, so that a math-inclined reader can audit the certificate layer directly. In detail, guidance and control software relies on numerical optimization and floating-point synthesis whose executions are difficult to verify directly. We study the problem of verifying solver outputs: given a certificate produced by an untrusted floating-point solver, we re-verify it in exact rational arithmetic, so that acceptance constitutes a proof that carries no rounding error. We apply this to four properties: abort safety, via barrier certificates; optimality of the online convex solves, via Karush-Kuhn-Tucker conditions for quadratic and second-order cone programs; closed-loop stability, via Lyapunov ellipsoids from a discrete-time linear-quadratic regulator; and polynomial set containment, via sum-of-squares certificates. For nonconvex quadratically constrained quadratic programs (QCQPs), we specialize the exact rational recovery of a semidefinite certificate (Peyrl-Parrilo; Kaltofen et al.) to the S-procedure dual, yielding a tolerance-free, machine-checkable optimality-gap bracket: a rational lower bound from the S-procedure dual and a rational upper bound from a feasible point, coinciding exactly at a global optimum. The note's original analysis characterizes how the certified lower bound degrades under rational rounding of the dual multiplier: the value loss is second-order in the rounding denominator in the nonsingular case and first-order in the trust-region hard case, with soundness retained in both, and it vanishes when the optimal multiplier is rational. For several constraints the S-procedure need not be tight, and the bracket then certifies a duality gap with both endpoints exact. Each result is accompanied by a verifying test in the reference implementation.