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

Proof of `Attainment of a finite linear-programming optimum`

groundedproofs/Lax109476Proofs/Attainment.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.

Read the Lean proof on GitHub

Description

Let α\alpha be the finite supremum of the feasible objectives. Apply Farkas' lemma to the original system with the extra constraint cTx≥αc^T x\ge\alpha. An infeasibility certificate has a nonnegative multiplier tt for this extra row. If t=0t=0, it contradicts original feasibility. If t>0t>0, divide the remaining multipliers by tt to obtain a dual feasible point with objective strictly below α\alpha. Weak duality then contradicts the supremum property. Thus the threshold system is feasible and attains α\alpha.