Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Proof of `Infinity-distance projection LP and its separating dual` (3rd statement)

groundedproofs/Lax263307Proofs/DistanceProjection.lean · lax-263307

What this proof establishes

no assumptions

thm✓Lax263307.DistanceProjection (3rd statement)

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

Description

Combine primal characterization with the dual normal bounds. Matching objectives identify the separation gap at the center with the returned distance.