Machine-Checked Foundations for the Exact-Rational Riccati Certificate: A Lean Companion Note

Verification companion to the rational Riccati certificate paper. It maps cited mathematical results to Lean 4 declarations and explicit hypotheses, pins the twenty-file corpus and its compilation environment, and catalogues executable exact-arithmetic checks. The formal results establish mathematical acceptance predicates and supporting facts; the shipped Python sweeps are not covered by an algorithm-refinement theorem. This version includes a fresh compilation of the cited corpus and clarifies the boundary between formal proofs, paper proofs and finite numerical checks.