p. 62 — with a common order, starting each item as soon as possible minimizes the total time

Proved

JohnsonFlowShop.TwoStage.asap_optimal_for_order

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

flow-shopp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1scheduling

Let $n$ items have positive processing times $A_i > 0$ (machine 1) and $B_i > 0$ (machine 2), and let $\sigma$ be an order, $\sigma(k)$ being the item in position $k$ . Let $(a^1, a^2)$ be the as-soon-as-possible schedule of $\sigma$ (asapStart1, asapStart2). Then

$(a^1, a^2)$ is feasible;
$(a^1, a^2)$ processes the items in the order $\sigma$ on both machines;
for every feasible schedule $(s^1, s^2)$ that processes the items in the order $\sigma$ on both machines,

T(a) \le T(s),

where $T$ is the total elapsed time.

This is the step of p. 62, "since the orders are now the same, we may start each item as soon as possible to minimize the total time". Combined with Lemma 1 it shows that some as-soon-as-possible schedule of an order is optimal among all feasible schedules.

Preamble

import Mathlib
import Definitions.Def_JohnsonFlowShop_TwoStage_IsFeasible
import Definitions.Def_JohnsonFlowShop_Shared_makespan
import Definitions.Def_JohnsonFlowShop_TwoStage_FollowsOrder
import Definitions.Def_JohnsonFlowShop_TwoStage_asapStart1
import Definitions.Def_JohnsonFlowShop_TwoStage_asapStart2

Formal statement

namespace JohnsonFlowShop.TwoStage

/-- p. 62: once both machines follow the same order `σ`, starting each item as soon as
possible is feasible, follows `σ`, and minimizes the total elapsed time among all feasible
schedules that follow `σ`. -/
theorem asap_optimal_for_order {n : ℕ} (A B : Fin n → ℝ)
    (hA : ∀ i, 0 < A i) (hB : ∀ i, 0 < B i) (σ : Equiv.Perm (Fin n)) :
    IsFeasible A B (asapStart1 A σ) (asapStart2 A B σ) ∧
    FollowsOrder A B (asapStart1 A σ) (asapStart2 A B σ) σ ∧
    ∀ s₁ s₂ : Fin n → ℝ, IsFeasible A B s₁ s₂ → FollowsOrder A B s₁ s₂ σ →
      Shared.makespan B (asapStart2 A B σ) ≤ Shared.makespan B s₂ := by sorry

end JohnsonFlowShop.TwoStage

Source

Johnson, Optimal Two- and Three-Stage Production Schedules with Setup Times Included, NRLQ 1(1) 1954, p. 62, Two-stage production schedule ("Next, since the orders are now the same, we may start each item as soon as possible to minimize the total time")

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