Prove2Me

§2, pp. 95–96 — the optimal dual multipliers of (PR_L) are exactly c_1j ≤ λ_j ≤ c_2j

Proved
RossSolandGAP.Bound.PRL_optimal_duals

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

dualitygeneralized-assignmentlagrangean-relaxationlinear-programmingp2o-batch-p200ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let m≥2m\ge2 and let j↦ijj\mapsto i_j be a cheapest-agent selection, so c1j=cijjc_{1j}=c_{i_jj} is the smallest and c2jc_{2j} the second smallest of c1j,…,cmjc_{1j},\dots,c_{mj}. Consider the bounded-variable linear program

(PRL)min⁡ ∑i∈I∑j∈Jcijxijs.t.∑i∈Ixij=1 (j∈J),0≤xij≤1,\text{(PR}_L)\qquad\min\ \sum_{i\in I}\sum_{j\in J}c_{ij}x_{ij}\quad\text{s.t.}\quad\sum_{i\in I}x_{ij}=1\ (j\in J),\quad 0\le x_{ij}\le1,

and its linear-programming dual, with a free multiplier λj\lambda_j for each equation and a multiplier uij≥0u_{ij}\ge0 for each upper bound xij≤1x_{ij}\le1:

max⁡ ∑j∈Jλj−∑i∈I∑j∈Juijs.t.λj−uij≤cij, uij≥0.\max\ \sum_{j\in J}\lambda_j-\sum_{i\in I}\sum_{j\in J}u_{ij}\quad\text{s.t.}\quad\lambda_j-u_{ij}\le c_{ij},\ u_{ij}\ge0 .

Then:

  1. the (PR) solution (xijj=1x_{i_jj}=1, other entries 00) is optimal for (PRL_L), with value Z=∑jc1jZ=\sum_jc_{1j};
  2. a vector λ\lambda is part of an optimal dual solution (λ,u)(\lambda,u) if and only if
c1j≤λj≤c2jfor all j∈J.c_{1j}\le\lambda_j\le c_{2j}\qquad\text{for all }j\in J.

This is the paper's remark that "each optimal dual multiplier λj\lambda_j for (PRL_L) lies anywhere in the range c1j≤λj≤c2jc_{1j}\le\lambda_j\le c_{2j}", so optimal multipliers are very easy to compute, and λ=c2\lambda=c_2 is the largest of them.

Formalization Note "Lies anywhere in the range" is read as: the set of optimal λ\lambda is exactly the box ∏j[c1j,c2j]\prod_j[c_{1j},c_{2j}]. The claim depends on the upper bounds xij≤1x_{ij}\le1 carrying dual multipliers; without them only λj≤c1j\lambda_j\le c_{1j} is dual feasible. The dual is written out explicitly; no LP duality theorem is assumed. Agents and tasks are 0-based.

Preamble
import Mathlib
import Definitions.Def_RossSolandGAP_Bound_Model
open Finset
Formal statement
namespace RossSolandGAP.Bound

theorem PRL_optimal_duals {m n : ℕ} (hm : 1 < m) (c : Fin m → Fin n → ℝ)
    (a : Fin n → Fin m) (ha : IsCheapest c a) :
    (FeasiblePRL (xPR a) ∧ cost c (xPR a) = Z c a ∧
      ∀ x, FeasiblePRL x → Z c a ≤ cost c x) ∧
    ∀ lam : Fin n → ℝ, (∃ u, IsOptDualPRL c lam u) ↔
      ∀ j, c (a j) j ≤ lam j ∧ lam j ≤ c2 hm c a j := by sorry

end RossSolandGAP.Bound
Source
Ross & Soland, A Branch and Bound Algorithm for the Generalized Assignment Problem, Mathematical Programming 8, 1975, pp. 95-96, §2, (PR_L) and the sentence 'It is particularly important to note that each optimal dual multiplier ...'
Human review

  • Endorsed by Shuze Chen · Sep 27, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Sep 27, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph