Weak Duality for Finite Standard-Form Linear Programs

Proved

PrimalDual.pd_weak_duality

by wenxinzhang · Aug 18, 2026 · Mathlib c5ea003 (Lean v4.30.0)

linear-programmingoptimizationprimal-dualweak-duality

Weak duality for the finite standard-form pair.

Let $A=(a_{ij})$ , $b=(b_j)$ , and $c=(c_i)$ be a finite standard-form primal–dual pair with primal variables indexed by $i\in\iota$ and constraints by $j\in\kappa$ . Let $x$ be primal feasible, i.e. $x\ge 0$ and $\sum_i a_{ij}x_i\ge b_j$ for every $j$ , and let $y$ be dual feasible, i.e. $y\ge 0$ and $\sum_j a_{ij}y_j\le c_i$ for every $i$ . Then

\sum_{j\in\kappa} b_j\,y_j \;\le\; \sum_{i\in\iota} c_i\,x_i.

Every feasible dual value is therefore a lower bound on every feasible primal value. In this mission the inequality turns a feasible dual of value $k$ into a certificate that no feasible primal of value below $k$ exists, which is the engine of the load-balancing failure argument.

Formalization Note No sign conditions on $A$ , $b$ , or $c$ are required: the statement covers the general standard form, not only the covering–packing subclass.

Preamble

import Definitions.Def_pd_finite_lp

Formal statement

namespace PrimalDual

theorem pd_weak_duality {ι κ : Type*} [Fintype ι] [Fintype κ]
    (P : FinitePrimalDual ι κ) (x : ι → ℝ) (y : κ → ℝ)
    (hx : P.PrimalFeasible x) (hy : P.DualFeasible y) :
    P.dualObjective y ≤ P.primalObjective x := by
  sorry

end PrimalDual

Source

Niv Buchbinder and Joseph (Seffi) Naor, The Design of Competitive Online Algorithms via a Primal--Dual Approach, https://www.tau.ac.il/~nivb/download/pd-survey.pdf, Theorem 2.1 and proof, pp. 98--99, equations (2.1)--(2.3).

Read-back

What the Lean code literally says, in plain math · gpt-5

For every pair of finite index types $\iota$ and $\kappa$ —each equipped with a Fintype structure and neither required to be nonempty—for every record $P$ consisting of arbitrary functions $a=P.\mathrm{coeff}:\iota\to\kappa\to\mathbb R$ , $b=P.\mathrm{rhs}:\kappa\to\mathbb R$ , and $c=P.\mathrm{cost}:\iota\to\mathbb R$ , and for every $x:\iota\to\mathbb R$ and $y:\kappa\to\mathbb R$ , if $x_i\ge 0$ for every $i\in\iota$ and $b_j\le\sum_{i:\iota}a_{ij}x_i$ for every $j\in\kappa$ , and if $y_j\ge 0$ for every $j\in\kappa$ and $\sum_{j:\kappa}a_{ij}y_j\le c_i$ for every $i\in\iota$ , then $\sum_{j:\kappa}b_jy_j\le\sum_{i:\iota}c_ix_i$ . Every displayed sum is the finite sum over the entire indicated index type, so a sum over an empty type is $0$ and a universally quantified condition over an empty type is vacuous: if $\iota$ is empty, the primal objective is $0$ , the $x$ -nonnegativity and dual-constraint conditions are vacuous, and primal feasibility requires $b_j\le0$ for every $j$ ; if $\kappa$ is empty, the dual objective is $0$ , the $y$ -nonnegativity and primal-constraint conditions are vacuous, and dual feasibility requires $0\le c_i$ for every $i$ ; if both are empty, all feasibility conditions are vacuous and the conclusion is $0\le0$ .

Human review

Endorsed by Shuze Chen · Aug 19, 2026
Endorsed by wenxinzhang · Aug 19, 2026
Confirmed by the mission captain (proposal self-audit).

View graph