Proof of `Soundness of exact rational LP certificates`
groundedproofs/Lax109476Proofs/Certificates.lean · lax-109476
What this proof establishes
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
Exact rational equalities and inequalities survive the embedding into the reals. Weak duality proves optimality of a matching pair, Farkas soundness proves infeasibility, and recession soundness proves unboundedness. Neither certificate existence nor a solver is needed to verify an outcome.