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

Proved

SingleMachineSched.AlphaJSched.eq_3_10

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

p2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1scheduling

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

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

This expresses the mean busy time through the structure of the LP schedule around $j$ ; together with (3.11) it is what the proof of Theorem 3.9 compares.

Formalization Note. $N_2$ and $\mu_k$ are the definitions of the file LPStructure. The weights and their order are the paper's standing assumptions; the smallest-index rule is what makes the structure hold.

Preamble

import Mathlib
import Definitions.Def_SingleMachineSched_AlphaJSched_LPSchedule
import Definitions.Def_SingleMachineSched_AlphaJSched_AlphaPoints
import Definitions.Def_SingleMachineSched_AlphaJSched_LPStructure

Formal statement

namespace SingleMachineSched.AlphaJSched

/-- Equation (3.10): `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.AlphaJSched

Source

Goemans, Queyranne, Schulz, Skutella & Wang, Single Machine Scheduling with Release Dates, SIAM J. Discrete Math. 15(2) (2002), p. 182, Section 3.2, 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+\tfrac12p_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+\tfrac12p_j$