Lemma 3 — an optimal ordering can be reached with the same ordering on each machine

Proved

JohnsonFlowShop.ThreeStage.same_ordering_dominant

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

flow-shopp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1permutation-schedulescheduling

Let $A_i, B_i, C_i > 0$ be the processing times of $n$ items on machines 1, 2, 3. For every feasible three-machine schedule $(s^1, s^2, s^3)$ , in which the three machines may process the items in different orders, there is an ordering $\sigma$ of the items such that the as-soon-as-possible schedule of $\sigma$ (same order on all three machines) is feasible and

\operatorname{makespan}\bigl(\text{as-soon-as-possible schedule of } \sigma\bigr) \le \operatorname{makespan}(s^3).

So in minimizing the total elapsed time on three machines one may restrict attention to a single common ordering, processed as early as possible. This reduction is what makes the comparison of orderings in Theorem 2 a comparison against all feasible schedules. It fails for four or more machines (p. 65).

Formalization Note The page's proof says "By Lemma 2"; the argument applies Lemma 1 (the same-sequence lemma, p. 61) to machines 1–2 and to machines 2–3, and Lemma 2 is the transitivity of relation (II). This is a misprint in the source. The "as soon as possible" part is the page 62 step that Lemma 3 inherits from the two-stage argument.

Preamble

import Mathlib
import Definitions.Def_JohnsonFlowShop_ThreeStage_IsFeasible
import Definitions.Def_JohnsonFlowShop_Shared_makespan
import Definitions.Def_JohnsonFlowShop_ThreeStage_asapSchedule

Formal statement

namespace JohnsonFlowShop.ThreeStage

/-- Lemma 3 (Johnson 1954, p. 65): an optimal ordering can be reached with the same ordering of
the items on all three machines. For positive processing times and every feasible three-machine
schedule `(s₁, s₂, s₃)` (whose machine orders may differ), there is an order `σ` whose
as-soon-as-possible schedule is feasible and has total elapsed time at most that of
`(s₁, s₂, s₃)`. -/
theorem same_ordering_dominant {n : ℕ} (A B C : Fin n → ℝ)
    (hA : ∀ i, 0 < A i) (hB : ∀ i, 0 < B i) (hC : ∀ i, 0 < C i)
    (s₁ s₂ s₃ : Fin n → ℝ) (hs : IsFeasible A B C s₁ s₂ s₃) :
    ∃ σ : Equiv.Perm (Fin n),
      IsFeasible A B C (asapStart1 A B C σ) (asapStart2 A B C σ) (asapStart3 A B C σ) ∧
      Shared.makespan C (asapStart3 A B C σ) ≤ Shared.makespan C s₃ := by sorry

end JohnsonFlowShop.ThreeStage

Source

Johnson, Optimal Two- and Three-Stage Production Schedules with Setup Times Included, NRLQ 1(1) 1954, p. 65, Lemma 3

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