Proof of `Rational LP certificates for distance projection` (2nd statement)
groundedproofs/Lax263307Proofs/RationalProjection.lean · lax-263307
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
The branch test uses the distance coordinate in the actual optimal certificate. The matching dual gives that exact gap. Infeasible and unbounded certificates are handled using the registered certificate soundness theorem.