Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

p. 66 — total idle time of machine 3 is max⁡1≤u≤v≤n(Hv+Ku)\max_{1 \le u \le v \le n}(H_v + K_u)max1≤u≤v≤n​(Hv​+Ku​)

Proved
JohnsonFlowShop.ThreeStage.makespan_asap_eq

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

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

Let Ai,Bi,Ci>0A_i, B_i, C_i > 0Ai​,Bi​,Ci​>0, let n≥1n \ge 1n≥1, and let σ\sigmaσ be any ordering of the items. With KuK_uKu​ and HvH_vHv​ the quantities of σ\sigmaσ (positions 1,…,n1, \dots, n1,…,n in the paper's indexing), the total elapsed time of the as-soon-as-possible three-machine schedule of σ\sigmaσ is

makespan⁡=∑i=1nCi+max⁡1≤u≤v≤n(Ku+Hv).\operatorname{makespan} = \sum_{i=1}^{n} C_i + \max_{1 \le u \le v \le n} \bigl(K_u + H_v\bigr).makespan=i=1∑n​Ci​+1≤u≤v≤nmax​(Ku​+Hv​).

Equivalently, since machine 3 is busy for ∑iCi\sum_i C_i∑i​Ci​ and idle for ∑iYi\sum_i Y_i∑i​Yi​, the total idle time of machine 3 is ∑i=1nYi=max⁡1≤u≤v≤n(Hv+Ku)\sum_{i=1}^{n} Y_i = \max_{1 \le u \le v \le n} (H_v + K_u)∑i=1n​Yi​=max1≤u≤v≤n​(Hv​+Ku​), the display of p. 66. On p. 68 Johnson restates it: max⁡u≤v≤n(Ku+Hv+∑i=1nCi)\max_{u \le v \le n}(K_u + H_v + \sum_{i=1}^{n} C_i)maxu≤v≤n​(Ku​+Hv​+∑i=1n​Ci​) "is the maximum sum of elements passed through on all 'walks' in the time matrix from the upper left-hand corner to the lower right-hand corner, taking steps to the right or downward. The problem is to find a scheduling of items which minimizes this maximum walk."

This turns the three-stage problem into the minimization of an explicit function of the ordering.

Formalization Note The statement is in elapsed-time form. The maximum over pairs is written as max⁡vmax⁡u≤v\max_v \max_{u \le v}maxv​maxu≤v​ over 0-based positions. It holds for every ordering; the special-case hypothesis min⁡A≥max⁡B\min A \ge \max BminA≥maxB is not assumed.

Preamble
import Mathlib
import Definitions.Def_JohnsonFlowShop_Shared_makespan
import Definitions.Def_JohnsonFlowShop_ThreeStage_asapSchedule
import Definitions.Def_JohnsonFlowShop_Shared_K
import Definitions.Def_JohnsonFlowShop_ThreeStage_H
Formal statement
namespace JohnsonFlowShop.ThreeStage

/-- p. 66 (closed form of the total idle time of machine 3, `Σ Y_i = max_{u ≤ v} (H_v + K_u)`),
in elapsed-time form (p. 68): for positive processing times, `n ≥ 1` and every order `σ`, the
total elapsed time of the as-soon-as-possible schedule of `σ` equals
`∑_i C_i + max_{u ≤ v} (K_u + H_v)`, the maximum over pairs of positions `u ≤ v`. -/
theorem makespan_asap_eq {n : ℕ} [NeZero n] (A B C : Fin n → ℝ)
    (hA : ∀ i, 0 < A i) (hB : ∀ i, 0 < B i) (hC : ∀ i, 0 < C i)
    (σ : Equiv.Perm (Fin n)) :
    Shared.makespan C (asapStart3 A B C σ) =
      ∑ i, C i + Finset.univ.sup' Finset.univ_nonempty (fun v : Fin n =>
        (Finset.Iic v).sup' Finset.nonempty_Iic (fun u => Shared.K A B σ u + H B C σ v)) := by sorry

end JohnsonFlowShop.ThreeStage
Source
Johnson, Optimal Two- and Three-Stage Production Schedules with Setup Times Included, NRLQ 1(1) 1954, p. 66, Three-stage production schedule, display Σ Y_i = max_{1≤u≤v≤n}(H_v + K_u); p. 68, maximum walk
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

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