Eq. (3.10) — $M^{LP}_j = t_j(0^+) + \sum_{k\in N_2}(1-\mu_k)p_k + \tfrac12 p_j$

Proved

SingleMachineSched.AlphaSched.eq_3_10

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

alpha-pointsp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1scheduling

Let $n$ jobs have integral processing times $p_j > 0$ , integral release dates $r_j \ge 0$ and weights $w_j > 0$ , indexed by nonincreasing $w_j/p_j$ . Fix a job $j$ . Let $t_j(0^+)$ be its start time in the LP schedule, $N_2$ the set of jobs $k \ne j$ processed in the LP schedule between the start and the completion of $j$ , and, for $k \in N_2$ , $\mu_k$ the fraction of job $j$ processed before the start of job $k$ . Then

M^{LP}_j = t_j(0^+) + \sum_{k \in N_2} (1 - \mu_k)\, p_k + \frac12 p_j .

The identity expresses the LP mean busy time through the structure of the LP schedule around job $j$ ; it is the form in which the paper compares the expected completion time with $M^{LP}_j + \tfrac12 p_j$ .

Preamble

import Mathlib
import Definitions.Def_SingleMachineSched_AlphaSched_AlphaPoints

Formal statement

namespace SingleMachineSched.AlphaSched

/-- Eq. (3.10) (Goemans et al. 2002, p. 182): in the LP schedule,
`M^LP_j = t_j(0⁺) + Σ_{k ∈ N₂} (1 - μ_k) p_k + p_j / 2`. -/
theorem eq_3_10 {n : ℕ} (p r : Fin n → ℕ) (w : Fin n → ℝ)
    (hp : ∀ j, 0 < p j) (hw : ∀ j, 0 < w j)
    (hsort : ∀ j k : Fin n, j ≤ k → w k / p k ≤ w j / p j) (j : Fin n) :
    mLP p r j = startTime (lpSet p r) j +
      ∑ k ∈ N2 p r j, (1 - mu p r j k) * (p k : ℝ) + (p j : ℝ) / 2 := by sorry

end SingleMachineSched.AlphaSched

Source

Goemans, Queyranne, Schulz, Skutella & Wang, Single Machine Scheduling with Release Dates, SIAM J. Discrete Math. 15(2) (2002), p. 182, Eq. (3.10)

Human review

Endorsed by Shuze Chen · Oct 1, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Eq. (3.10) — MjLP=tj(0+)+∑k∈N2(1−μk)pk+12pjM^{LP}_j = t_j(0^+) + \sum_{k\in N_2}(1-\mu_k)p_k + \tfrac12 p_jMjLP​=tj​(0+)+∑k∈N2​​(1−μk​)pk​+21​pj​

Eq. (3.10) — $M^{LP}_j = t_j(0^+) + \sum_{k\in N_2}(1-\mu_k)p_k + \tfrac12 p_j$