Proof of Theorem 4 — under saturation, $P3\mid res1\cdot\cdot, p_j=1\mid C_{\max}$ is equivalent to 3-PARTITION

Proved

ResourceScheduling.Chain.threePartition_iff_p3Schedule

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

3-partitionp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1reductionsscheduling

Let $t \in \mathbb{N}$ , let $b$ be a positive integer and $a_1,\dots,a_{3t}$ positive integers with $\sum_{j=1}^{3t} a_j = tb$ . Consider the instance of $P3\mid res1\cdot\cdot, p_j = 1\mid C_{\max}$ with $3t$ unit-time jobs $J_1,\dots,J_{3t}$ , three identical machines, one resource of size $b$ , requirements $r_{1j} = a_j$ and no precedence constraints. Then

\{1,\dots,3t\} \text{ can be partitioned into } t \text{ disjoint 3-element sets } S_i \text{ with } \sum_{j\in S_i} a_j = b \iff \text{some feasible schedule has } C_{\max} \le t.

With $3t$ unit jobs on three machines in time $t$ , and total requirement $tb$ against a resource of size $b$ , both the machines and the resource are saturated; this is the paper's statement "When the machines and resources are all saturated, $P3\mid res1\cdot\cdot, p_j = 1\mid C_{\max}$ is equivalent to the following problem: 3-PARTITION". It is the reduction behind Theorem 4.

Formalization Note. Schedules have real start times and the resource constraint is checked at every real time. The page's version of 3-PARTITION has no bounds on the $a_j$ , so none are assumed here.

Preamble

import Mathlib
import Definitions.Def_ResourceScheduling_Chain_Constructions

Formal statement

namespace ResourceScheduling.Chain
theorem threePartition_iff_p3Schedule (P : ThreePartition) (hb : 0 < P.b)
    (ha : ∀ j, 0 < P.a j) (hsum : ∑ j, P.a j = P.t * P.b) :
    P.HasSolution ↔ P.p3Instance.HasScheduleWithin P.t := by sorry
end ResourceScheduling.Chain

Source

Błażewicz, Lenstra & Rinnooy Kan, Scheduling subject to resource constraints: classification and complexity, Discrete Appl. Math. 5 (1983), p. 16, proof of Theorem 4

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Let $P$ consist of natural numbers $t$ and $b$ and numbers $a_j \in \mathbb{N}$ for $j \in S = \{0,\dots,3t-1\}$ . Assume:

$b > 0$ ;
$a_j > 0$ for every $j$ ;
$\displaystyle\sum_{j \in S} a_j = t\,b$ .

The bounds $\tfrac14 b < a_j < \tfrac12 b$ are not assumed.

The theorem asserts that the following two statements are equivalent (if and only if).

(A) A partition exists. There is a map $\sigma: S \to \{0,\dots,t-1\}$ such that, for every $i$ , the set $\sigma^{-1}(i)$ has exactly three elements and its $a_j$ sum to $b$ .

(B) A schedule of makespan at most $t$ exists for the following instance:

$3t$ unit-time jobs indexed by $S$ ;
$3$ machines;
one resource of size $b$ , with job $j$ requiring $a_j$ ;
no precedence constraints.

Concretely, (B) says there are a machine $\mu(j) \in \{0,1,2\}$ and a real start time $S_j$ for each job such that:

$S_j \ge 0$ for all $j$ .
Distinct jobs on the same machine satisfy $S_j + 1 \le S_k$ or $S_k + 1 \le S_j$ .
For every real $\tau$ ,

\sum_{j \,:\, S_j \le \tau < S_j+1} a_j \le b.

$\max_j (S_j+1) \le t$ , where the maximum is taken as $0$ when there are no jobs.

Start times may be arbitrary nonnegative reals, not necessarily integers.

Degenerate cases. When $t = 0$ , both sides hold:

(A) is witnessed by the empty map;
(B) is witnessed by the empty schedule, whose makespan is $0 \le 0$ .

So the equivalence is trivially true in that case. The hypotheses are satisfiable (for example $t=1$ , $b=3$ , $a=(1,1,1)$ ), so the theorem is not vacuous.

Human review

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

View graph

Proof of Theorem 4 — under saturation, P3∣res1⋅⋅,pj=1∣Cmax⁡P3\mid res1\cdot\cdot, p_j=1\mid C_{\max}P3∣res1⋅⋅,pj​=1∣Cmax​ is equivalent to 3-PARTITION

Proof of Theorem 4 — under saturation, $P3\mid res1\cdot\cdot, p_j=1\mid C_{\max}$ is equivalent to 3-PARTITION