Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

§2, p. 96 — at λ_j = c_2j the variables that are zero in the (PR) solution can be set to zero in (PR_λ)

Proved
RossSolandGAP.Bound.PR_zeros_can_be_fixed

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

generalized-assignmentinteger-programminglagrangean-relaxationp2o-batch-p200ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let m≥2m\ge2m≥2, let rij≥0r_{ij}\ge0rij​≥0, let j↦ijj\mapsto i_jj↦ij​ be a cheapest-agent selection, and take the multipliers λj=c2j\lambda_j=c_{2j}λj​=c2j​, the second smallest of c1j,…,cmjc_{1j},\dots,c_{mj}c1j​,…,cmj​. Let xxx be feasible for (PRλ_\lambdaλ​) (binary, with ∑jrijxij≤bi\sum_j r_{ij}x_{ij}\le b_i∑j​rij​xij​≤bi​ for every agent iii). Define x′x'x′ by keeping xijx_{ij}xij​ when i=iji=i_ji=ij​ and setting xij′=0x'_{ij}=0xij′​=0 when i≠iji\ne i_ji=ij​, i.e. when xijx_{ij}xij​ is zero in the (PR) solution. Then x′x'x′ is feasible for (PRλ_\lambdaλ​) and

∑i∑jcijxij′+∑jc2j(1−∑ixij′) ≤ ∑i∑jcijxij+∑jc2j(1−∑ixij).\sum_{i}\sum_{j}c_{ij}x'_{ij}+\sum_{j}c_{2j}\Bigl(1-\sum_{i}x'_{ij}\Bigr)\ \le\ \sum_{i}\sum_{j}c_{ij}x_{ij}+\sum_{j}c_{2j}\Bigl(1-\sum_{i}x_{ij}\Bigr).i∑​j∑​cij​xij′​+j∑​c2j​(1−i∑​xij′​) ≤ i∑​j∑​cij​xij​+j∑​c2j​(1−i∑​xij​).

So, at these multipliers, (PRλ_\lambdaλ​) may be solved over points supported on the (PR) assignment pattern. This is the third observation in the paper's verification of its principal result.

Formalization Note rij≥0r_{ij}\ge0rij​≥0 is implicit in the paper ("the resource required by agent iii to do task jjj") and is needed: it is what keeps x′x'x′ within the budgets. Agents and tasks are 0-based.

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

theorem PR_zeros_can_be_fixed {m n : ℕ} (hm : 1 < m) (c r : Fin m → Fin n → ℝ)
    (b : Fin m → ℝ) (hr : ∀ i j, 0 ≤ r i j) (a : Fin n → Fin m) (ha : IsCheapest c a)
    (x : Fin m → Fin n → ℝ) (hx : FeasibleLag r b x) :
    FeasibleLag r b (fun i j => if a j = i then x i j else 0) ∧
    lagObj c (c2 hm c a) (fun i j => if a j = i then x i j else 0) ≤
      lagObj c (c2 hm c a) x := by sorry

end RossSolandGAP.Bound
Source
Ross & Soland, A Branch and Bound Algorithm for the Generalized Assignment Problem, Mathematical Programming 8, 1975, p. 96, §2, second paragraph, second sentence (third observation)
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

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me