Restricting the Full Dual Witness to a Prefix

Proved

PrimalDual.buchbinder_naor_restrict_dual_through

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

dual-feasibilitylinear-programmingload-balancingonline-algorithmsprimal-dual

Let $y$ be a feasible dual solution of the unrelated-machines packing dual that assigns unit total mass to every job: $y\ge 0$ , $\sum_{i} \tilde p(i,j)\,y(i,j)\le 1$ for every machine $j$ , and $\sum_{j} y(i,j)=1$ for every job $i$ , all sums ranging over eligible pairs. Restrict $y$ to the eligible pairs of the first $k$ jobs. Then the restriction is feasible for the prefix dual, and its objective equals the number of revealed jobs:

\sum_{(i,j)\,:\,i<k} y(i,j)\;=\;k.

This prefix lemma makes explicit the restriction implicit in the source's weak-duality failure certificate: at the moment of a hypothetical failure after $k$ assignments, it supplies a feasible dual of value exactly $k$ for the prefix program.

Formalization Note The restriction only forgets pairs with job index $\ge k$ ; no values are altered. A job with no eligible machine is incompatible with the unit-mass hypothesis, so the premise already forces every job to have at least one eligible machine.

Preamble

import Definitions.Def_pd_unrelated_machines

Formal statement

namespace PrimalDual

/--
A full feasible dual assigning every job restricts to a feasible prefix dual,
and its prefix objective is exactly the number of revealed jobs.
-/
theorem buchbinder_naor_restrict_dual_through
    {jobs machines : ℕ} (I : UnrelatedMachines.Instance jobs machines)
    (y : I.EligiblePair → ℝ) (hy : I.DualAssignsAll y)
    (k : ℕ) (hk : k ≤ jobs) :
    (I.lpThrough k).DualFeasible (I.restrictDual y k) ∧
      (I.lpThrough k).dualObjective (I.restrictDual y k) = (k : ℝ) := 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, formal prefix version of the feasible-dual-value argument immediately before Theorem 8.1 on p. 194 and in Claim (2) on p. 196.

Read-back

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

For all $J,M\in\mathbb N$ , let $[J]=\{i\in\mathbb N:i<J\}$ and $[M]=\{j\in\mathbb N:j<M\}$ ; for every instance $I$ consisting of $M>0$ and loads $p_{ij}\in\mathbb R$ for $i\in[J]$ , $j\in[M]$ , with $p_{ij}\ge 0$ , define the eligible-pair set $E=\{(i,j)\in[J]\times[M]:p_{ij}\le 1\}$ . For every function $y:E\to\mathbb R$ such that (i) $y_{ij}\ge 0$ for every $(i,j)\in E$ , (ii) for every machine $j\in[M]$ , $\sum_{\{i:(i,j)\in E\}}p_{ij}y_{ij}\le 1$ , (iii) for every job $i\in[J]$ , $\sum_{\{j:(i,j)\in E\}}y_{ij}\le 1$ , and additionally (iv) for every job $i\in[J]$ , $\sum_{\{j:(i,j)\in E\}}y_{ij}=1$ , and for every $k\in\mathbb N$ satisfying $k\le J$ , let $E_k=\{(i,j)\in E:i<k\}$ . The prefix LP has one dual coordinate for every pair in $E_k$ , retains primal coordinates for every machine in $[M]$ and every job in $[J]$ , uses coefficient $p_{ij}$ at the machine coordinate matching $j$ , coefficient $1$ at the job coordinate matching $i$ , and coefficient $0$ at nonmatching coordinates, and has every primal cost and every dual-objective right-hand-side coefficient equal to $1$ ; the restriction of $y$ to this LP is $y|_{E_k}$ , assigning each prefix pair its original value. The theorem asserts simultaneously that this restriction satisfies $y_{ij}\ge 0$ for every $(i,j)\in E_k$ , $\sum_{\{i:(i,j)\in E_k\}}p_{ij}y_{ij}\le 1$ for every $j\in[M]$ , and $\sum_{\{j:(i,j)\in E_k\}}y_{ij}\le 1$ for every $i\in[J]$ , including jobs $i\ge k$ whose displayed sum is empty, and that its dual objective is exactly $\sum_{(i,j)\in E_k}y_{ij}=k$ as an equality in $\mathbb R$ . If $J=0$ , then $k=0$ , both $E$ and $E_k$ are empty, the job-indexed assumptions and conclusions are vacuous, every remaining dual sum is $0\le 1$ , and the objective equality is $0=0$ ; for any $J$ , if $k=0$ , then $E_k$ is empty, prefix nonnegativity is vacuous, every prefix machine and job sum is $0\le 1$ , and the objective is $0=k$ ; if any job has no eligible pair, condition (iv) demands that an empty sum $0$ equal $1$ , so no such $y$ satisfies the hypotheses (in particular, globally having no eligible pairs is compatible with the hypotheses only when $J=0$ , and $E_k$ cannot be empty for $k>0$ under the hypotheses).

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