Motivation

Tree-width measures how closely a graph resembles a tree. Graphs of bounded tree-width admit dynamic-programming algorithms for problems that are NP-hard in general (colouring, Hamiltonicity, and every property expressible in monadic second-order logic, by Courcelle's theorem), which is why the parameter is central to parameterized complexity and to combinatorial optimization on sparse networks. The question this mission addresses is structural: which excluded substructures force bounded tree-width?

The answer is the Excluded Grid Theorem of Robertson and Seymour: excluding a fixed graph $H$ as a minor bounds the tree-width if and only if $H$ is planar. The "only if" direction is easy, since grids are planar and have unbounded tree-width. The "if" direction is the content of Graph Minors. V. Excluding a Planar Graph (J. Combin. Theory Ser. B 41 (1986) 92–114). It is a cornerstone of the Graph Minors series that culminates in the Robertson–Seymour theorem (graphs are well-quasi-ordered by the minor relation), and it underlies polynomial-time minor testing for planar $H$ (Graph Minors XIII) and the Erdős–Pósa-type results of Sect. 8 of the same paper.

Timeline. Robertson and Seymour, Graph Minors V (1986): tree-width at most an explicit, iterated-exponential function of the grid size. Robertson, Seymour and Thomas, Quickly excluding a planar graph (JCTB 62, 1994): bound $2^{O(\theta^5)}$ for the $\theta$-grid. Chekuri and Chuzhoy (J. ACM 2016): the first polynomial bound. Chuzhoy and Tan (JCTB 2021): $O(\theta^9\,\mathrm{polylog}\,\theta)$.

Setting

Graphs are finite. A graph $H$ is a minor of $G$ if $H$ can be obtained by contraction from a subgraph of $G$; equivalently, there are nonempty, pairwise disjoint vertex sets $\beta(w)\subseteq V(G)$, one per vertex $w$ of $H$, each inducing a connected subgraph, such that every edge $ab$ of $H$ is matched by an edge of $G$ between $\beta(a)$ and $\beta(b)$.

A tree-decomposition of $G$ is a tree $T$ together with bags $X_t\subseteq V(G)$ ($t\in V(T)$) such that every vertex lies in some bag, both ends of every edge lie in a common bag, and $X_t\cap X_{t''}\subseteq X_{t'}$ whenever $t'$ lies on the path of $T$ between $t$ and $t''$. Its width is $\max_t(|X_t|-1)$, and the tree-width $\mathrm{tw}(G)$ is the least width of a tree-decomposition of $G$.

The $\theta$-grid has vertex set $\{v_{ij}: 1\le i,j\le\theta\}$, with $v_{ij}$ adjacent to $v_{i'j'}$ exactly when $|i-i'|+|j-j'|=1$. For even $\theta\ge 6$, $\mathcal F_\theta$ is the class of graphs with no minor isomorphic to the $\theta$-grid. Every planar graph $H$ is a minor of some even grid of size at least 6; $\theta(H)$ denotes the least such size.

The paper fixes explicit parameters. For $k\ge 2$: $\alpha(2,n)=n+1$ and $\alpha(k,n)=2^{n\theta^4}+\alpha(k-1,2^{n\theta^4}+n+1)$. Then $\theta_1=2\alpha(\theta^2/2,\theta^2/2)$; $\phi_{\theta_1}=\theta^2/2$ and $\phi_k=\phi_{k+1}2^{\phi_{k+1}\theta^2}$; $\theta_2=\phi_0+2\phi_1+\dots+2\phi_{\theta_1-1}+\phi_{\theta_1}$; $\theta_3=(\theta^2/2)^{\theta_2-1}$; $\theta_4=\theta_2\binom{\theta_3}{\theta_2}+\tfrac12\theta^2\binom{\theta_3}{\theta^2/2}$; $\theta_5=(\theta^2/2)^{\theta_4-1}$; $\theta_6=\theta_3\binom{\theta_5}{\theta_4}+\tfrac12\theta^2\binom{\theta_5}{\theta^2/2}$; $\theta_7=\alpha(\theta_5,\theta_6)$; $\theta_8=3\theta_5(3^{\theta_5}-1)/4$; $\theta_9=\theta_7(\theta_8+1)+1$.

Two auxiliary structures carry the argument. An $(m,n)$-web is a pair of families of paths $(A_1,\dots,A_m)$, $(B_1,\dots,B_n)$, each family vertex-disjoint, every $A_i$ meeting every $B_j$, and all $m+n$ paths pairwise edge-disjoint. An $(m,n)$-mesh is the same with arbitrary connected subgraphs in place of paths and without edge-disjointness.

Formalization targets

Goal: (2.1)

For every finite planar graph $H$ and every finite graph $G$,

Principal theorem: (7.3)

For even $\theta\ge 6$ and $G\in\mathcal F_\theta$,

Intermediate targets

• Sect. 2: every planar graph is a minor of some even $\theta$-grid, $\theta\ge 6$.
• (3.2): $n$ disjoint connected subgraphs meeting each of $V_1,\dots,V_k$, or a hitting set of size $<\alpha(k,n)$.
• (4.1), (4.2), (4.4), (4.5), (4.6): no $(\theta_2,\theta_2)$-web in $G\in\mathcal F_\theta$.
• (5.1), (5.2), (5.3): no $(\theta_5,\theta_6)$-mesh in $G\in\mathcal F_\theta$.
• (6.2), (6.3), (6.4): weighted and unweighted balanced-cut lemmas valid for all graphs.
• (7.1), (7.2): separations of order $\le\theta_7$ splitting $V(G)$, or any $X\subseteq V(G)$, in ratio $1-\theta_8^{-1}$.

Significance

The theorem converts a qualitative exclusion (no $H$ minor) into a quantitative width bound, and it is the entry point of the structure theory of minor-closed classes: every minor-closed class excluding a planar graph has bounded tree-width, and hence all MSO-definable problems on it are solvable in linear time. It is used in the proof of the graph minor theorem, in minor testing, and in the Erdős–Pósa property for planar minors (Sect. 8 of the paper).

The result is proved and classical; to our knowledge it has not been machine-checked in any proof assistant, and Mathlib has no graph minors, tree-decompositions or Menger's theorem. A formalization produces reusable definitions (branch-set minors, tree-decompositions, separations, grids) and a checked proof of the paper's explicit bound. The goal is stated with the paper's constant $\theta_9$, not an optimized one; later improvements are stronger variants, not replacements.

Difficulty

The obvious attempt, building a tree-decomposition greedily from small separations, fails because nothing forces small balanced separations to exist. The whole argument supplies them: a graph without a large grid minor has no large mesh (5.3), and a graph with no large mesh has a balanced separation of bounded order (7.1). The step from no grid to no mesh goes through webs and spiders (Sect. 4) and relies on two results from Graph Minors I ((3.1) and (4.3) of the paper, cited without proof), which themselves depend on Menger's theorem. The balanced-cut lemmas (6.2)–(6.4) rest on Tutte's ordering of 2-connected graphs. None of this infrastructure exists in Mathlib.

Formalization scope

Graphs are Mathlib SimpleGraphs on finite types (Fintype V, DecidableEq V). The paper allows loops and multiple edges; for $G$ this changes nothing, since every notion used depends only on adjacency, and for $H$ in the goal it specializes the theorem to simple planar graphs. Minors use the branch-set model (IsMinor); planarity (IsPlanar) is the existence of a crossing-free drawing in $\mathbb R^2$, mirroring the platform's FourColor.IsPlanar. Tree-width is not defined as an infimum; "tree-width at most $w$" (TreewidthLE) is the existence of a tree-decomposition with all bags of size $\le w+1$ over a finite tree. $\theta(H)$ enters the goal as a hypothesis IsLeast {t | Even t ∧ 6 ≤ t ∧ IsMinor H (grid t)} θ, which is satisfiable for every planar $H$ by the Sect. 2 milestone, so the goal is not vacuous. Every statement of Sects. 3–7 that mentions $\theta$ carries the standing assumption "$\theta$ even, $\theta\ge 6$" as hypotheses. Rational bounds such as $(1-\theta_8^{-1})|V(G)|$ and $2(3^k-1)^{-1}|V(G)|$ are compared in $\mathbb Q$.

Two printed statements are corrected. (4.5) is printed for $0\le k<\theta_2$ and is stated for $0\le k<\theta_1$, the only range on which $\phi_{k+1},\psi_{k+1}$ are defined. (5.1) is false as printed for $p=1$, $q\ge 1$, so it carries the hypothesis "$p=1$ implies $q=0$"; the paper uses it only with $p=\theta^2/2$.

Needed infrastructure, reusable well beyond this mission: Menger's theorem, the Graph Minors I linkage results, Tutte's ordering of 2-connected graphs, and a library of lemmas for minors and tree-decompositions. Proofs of any milestone, of the cited results as separate theorems, and of basic API for the definitions are welcome.

Selected references

• N. Robertson, P. D. Seymour, Graph Minors. V. Excluding a Planar Graph, J. Combin. Theory Ser. B 41 (1986) 92–114. https://doi.org/10.1016/0095-8956(86)90030-4
• N. Robertson, P. D. Seymour, Graph Minors. I. Excluding a Forest, J. Combin. Theory Ser. B 35 (1983) 39–61. https://doi.org/10.1016/0095-8956(83)90079-5
• N. Robertson, P. D. Seymour, R. Thomas, Quickly Excluding a Planar Graph, J. Combin. Theory Ser. B 62 (1994) 323–348. https://doi.org/10.1006/jctb.1994.1073
• C. Chekuri, J. Chuzhoy, Polynomial Bounds for the Grid-Minor Theorem, J. ACM 63 (2016), Art. 40. https://doi.org/10.1145/2820609
• J. Chuzhoy, Z. Tan, Towards Tight(er) Bounds for the Excluded Grid Theorem, J. Combin. Theory Ser. B 146 (2021) 219–265. https://doi.org/10.1016/j.jctb.2020.09.010
• B. Courcelle, The Monadic Second-Order Logic of Graphs. I. Recognizable Sets of Finite Graphs, Information and Computation 85 (1990) 12–75. https://doi.org/10.1016/0890-5401(90)90043-H

Why formalize the Four Color Theorem in Lean 4?

The Four Color Theorem links a short mathematical statement to a large collection of finite checks. For contributors to graph theory and proof assistants, it is a concrete test of whether abstract mathematics, executable verification, and a public theorem statement can share one auditable foundation. The proposed result is a complete Lean 4 formalization, reusing Mathlib and adapting the established proof architecture to Lean.

The mathematical result is established. Robertson, Sanders, Seymour, and Thomas gave a modern computer-assisted proof in 1997. Gonthier subsequently developed a Coq formalization covering both mathematical reasoning and computation, described in his 2005 report and 2008 Notices article. This mission is classified as ResearchPaper because it formalizes these published results. (RSST, Gonthier 2005, Gonthier 2008)

Graphs, drawings, and colors

The root Lean interface uses Mathlib's SimpleGraph: a finite vertex set with a symmetric, irreflexive adjacency relation. Edges in this representation carry no additional identities or multiplicities. The conventional statement also permits parallel edges. Already-proved local infrastructure uses Mathlib's Graph V E to erase parallel edges while preserving a genuine plane drawing and proper vertex colorings; only the actual vertex set must be finite. A proper vertex coloring assigns a color to every vertex and assigns different colors to adjacent vertices. Four available colors means at most four colors are used; there is no requirement that each color occur.

A planar drawing places distinct vertices at distinct points of the real plane and represents each edge by an injective continuous arc joining its endpoints. An arc contains no other vertex, and arcs of different undirected edges meet only at shared endpoints. Reversing the orientation of an edge reverses its parameterization. A graph is planar when such a drawing exists. This is a geometric condition independent of coloring and of the eventual configuration checkers. Gonthier discusses the graph-embedding formulation in Section 2, PDF p. 4 of the 2005 report.

Write $V$ for the vertex set, $G$ for its adjacency relation, and $C=\{0,1,2,3\}$ for the available colors. Empty graphs, isolated vertices, and disconnected graphs are included. The drawing is a witness to a hypothesis; the theorem does not impose coordinates, a prescribed embedding, or a straight-line representation.

Formalization target

For every finite loopless planar graph, establish

The draft Lean target is FourColor.four_color: for every finite vertex type and every SimpleGraph on that type, FourColor.IsPlanar G implies G.Colorable 4. Its graph formulation follows RSST's Section 1, PDF p. 2 of the author-hosted manuscript. The manuscript's PDF page numbers differ from the journal's pagination.

The exact unchanged root signature is:

FourColor.four_color.{u} :
  ∀ (V : Type u) [Finite V] (G : SimpleGraph V),
    FourColor.IsPlanar G → G.Colorable 4

This is an open target signature, not a completed proof. The existing FourColor.FinalAudit.multigraph_four_color_of_necessary_targets conditionally connects the mission obligations to the conventional finite loopless planar multigraph statement. Its drawing has distinct vertex positions and injective continuous arcs for each edge identity; erasing parallel edges is proved to preserve planarity and every proper-coloring constraint. This bridge adds no simplicity, connectedness, triangulation, or nonemptiness assumption to the conventional conclusion. The root target itself remains unchanged.

An equivalent combinatorial formulation is welcome only with the formally verified translations needed to recover this target. If equivalence is claimed, both directions must be proved under precisely stated conventions. In particular, a hypermap coloring theorem alone does not complete this mission.

The original seven structural milestones remain unchanged:

These correspond to Gonthier's reductions in Section 3, PDF pp. 6–9, and development in Sections 5.1–5.6 of the 2005 report. Exact locations and executable-reference declarations accompany each milestone. Milestones 2, 3 and 6 imply milestone 7; milestones 1 and 7 imply the graph target. Those two conditional implications have been checked in Lean against the exact proposed statements. Milestone 6 now has thirteen concrete supporting targets:

The fixed catalogue and fixed rules are shared by both branches. The local Lean assembly checks that reducibility, geometric exclusion, reflection, the transfer bound, the seven degree cases, and milestones 4–5 imply milestone 6. It then connects to the unchanged hypermap and graph targets. The generic presentation checker offers a sufficient route to the semantic degree targets; its ability to certify every source presentation is not presumed. That route also requires actual presentation certificates and proofs of acceptance for the degree cases. Generic soundness and catalogue geometry alone do not supply those witnesses. Direct proofs of the seven semantic coverage obligations remain valid. Catalogue geometry remains a separate, meaningful finite theorem.

Exact mission obligations

There are 21 open theorem targets: 20 supporting milestones and one root. Every name below has prefix FourColor.. All remain future mission work; the checked conditional assembly is not a proof of any of these targets.

The degree cases quantify over minimal counterexamples with the exact positive score defined by the fixed rules; neighboring degrees have no artificial upper bound. The dependency path uses 16 necessary input targets to derive targets 19, 20 and 21. Targets 6 and 10 support the optional presentation-certificate route. None of targets 19, 20 or 21 is assumed as a shortcut in this assembly.

What completion would provide

The theorem provides a uniform existence guarantee for all finite planar graphs, without a bound on their size. Its Lean development should also make reusable graph embeddings, finite combinatorial maps, coloring transports, and verified finite checkers available to later work.

The existing Rocq development is an executable reference for definitions, dependency structure, and proof behavior. It is not a proof import into Lean. The proposed contribution is a Lean development whose proof objects and computation are justified within Lean's documented foundations. A mechanically translated collection of scripts is not required; contributors should choose abstractions that work well with Mathlib.

Where the difficulty lies

Checking finitely many small graphs does not establish the theorem for arbitrary finite graphs. The development must justify why its finite computational tasks suffice, and must connect their results to the graph statement. The mathematical and computational obligations must meet at explicit, proved interfaces.

There is also a representation gap. The standard target concerns vertex colorings of graphs drawn in the plane, whereas the reference implementation's combinatorial core colors faces of planar bridgeless hypermaps. The latter endpoint is four_color_hypermap in combinatorial4ct.v. Correct treatment of duality, connected components, and isolated vertices is part of the work. Renaming a combinatorial predicate “planar” cannot establish that connection.

Formalization scope and acceptance criteria

Use Lean 4 with a supported, pinned Mathlib revision. The initial draft is checked against Lean v4.30.0 and Mathlib c5ea00351c28e24afc9f0f84379aa41082b1188f. Any later migration must preserve the statements and repeat the relevant checks. Reuse Mathlib's graph and coloring interfaces where appropriate, and develop missing infrastructure as reusable modules. The topological definition must not assume colorability, successful certificate verification, or the conclusion of an intermediate theorem.

The definition layer now provides plane drawings, finite permutation hypermaps, an exact graph/face incidence representation, minimal counterexamples, and rational face charges. Coloring equivalence across a face representation is proved for every positive number of colors, with isolated vertices handled explicitly. Exact Euler equality defines combinatorial planarity; geometric realization is a theorem obligation and cannot be assumed from the name.

The concrete core now defines configurations, ordered boundary traces, contracts, chromograms, Kempe closure, kernel preembeddings and reflected occurrences. The reference reducibility checker has proved soundness and completeness. All 633 maps, rings and contracts are literal data with kernel-validated table/index proofs. The 38 base entries and their 71 symmetrized entries are explicit, and the executable matcher has proved semantic correctness. These infrastructure results do not prove the catalogue's geometric validity, its reducibility, or unavoidability.

The production targets import FourColor.CompactCatalogue.configurations, a compact catalogue containing the same literal maps, rings and contracts. A generic verified decoder constructs validated entries without storing large evaluated proof terms in every import. A separate kernel-checked comparison proves exact ordered equality with the original catalogue, proves that every raw entry is accepted, and proves that none is dropped. The original certificate batches remain available for that audit but are excluded from production target imports. This representation change does not alter any of the 21 mathematical obligations.

Data provenance is pinned to Rocq commit c1d6b1cd5288bea4b067aac13cdde3c18dffe018. Independent fresh-source comparisons check all 633 configurations and every base/expanded rule entry against that snapshot, including actual evaluated Lean payloads. These comparisons establish source correspondence; they are not proofs of reducibility or unavoidability.

The duplicate-data gate rejects unexplained or unintended duplicates and permits verified source-mandated repetition encoding multiplicity or weight. The only repeated rule payload is drule1, deliberately listed twice: the source explains its two-point transfer in discharge.v, lines 17–24 and retains both copies in base_drules (line 145). The Lean rule-match count also counts both copies, preserving weight two. Thus there are 38 base entries with 37 distinct payloads, and 71 expanded entries with 70 distinct payloads. Both copies must remain. No configuration duplicates or other repeated rule payloads are permitted without separately verified source justification.

The reference reducibility evaluator is exponentially expensive. Contributors should implement verified compressed representations or efficient checkers, with acceptance implying the same semantic C-reducibility. Completeness of the reference checker then recovers the stated certificate-existence target. The presentation language is a transparent finite baseline; its generic soundness is an open target, and no completeness claim is made. Source-style quizzes/hubcaps or direct Lean proofs can close the same seven semantic coverage targets. This keeps performance choices separate from the mathematical endpoint.

All computational claims needed by the theorem must be established in Lean. External generators may prepare candidate data or certificates, but their output must be validated by a checker with proved correctness, and the resulting proof must be accepted by the Lean kernel. A recorded successful run of an external program is insufficient. The final theorem and its dependency closure must contain no sorry, admit, unproved custom axiom, or unsupported computational assumption. An axiom audit must identify only Lean/Mathlib's documented foundations. The current 37-declaration conditional/infrastructure audit uses only propext, Classical.choice and Quot.sound; it does not claim an unconditional Four Color proof. Python generators and runtime JSON extraction are outside the mathematical trust boundary and cannot discharge the 21 targets.

Completion requires a reproducible repository in which lake build succeeds from a clean environment and builds the final theorem. Pin toolchain, dependencies, source revisions, and certificate data; document regeneration and verification commands. Maintain a dependency map connecting Lean declarations to exact paper locations and Rocq declarations, and record justified differences in representation. The local multigraph adapter already justifies forgetting parallel-edge multiplicities and transports proper colorings. Any auxiliary restrictions such as connectedness or nonemptiness must be discharged before the root theorem. The current statement and conditional builds verify proposal infrastructure. Success requires proofs of the mission obligations and the final theorem in the reproducible clean build, with no unproved assumptions beyond the documented Lean/Mathlib foundations. All 21 targets remain open at proposal finalization. The submission snapshot records the repository base commit, exact working-file hashes, toolchain, Mathlib revision, payload hashes and audit report; it must not misrepresent uncommitted files as contents of the base commit.

Selected references

• Georges Gonthier, A Computer-Checked Proof of the Four Colour Theorem, technical report, 2005. Sections 2–5. Microsoft Research PDF.
• Georges Gonthier, Formal Proof—The Four-Color Theorem, Notices of the AMS 55(11), 1382–1393, 2008. Theorem 1 and the formalization architecture. AMS PDF.
• Gonthier and Rocq-community contributors, fourcolor, executable formalization, pinned to commit c1d6b1cd5288bea4b067aac13cdde3c18dffe018. Repository.
• Neil Robertson, Daniel Sanders, Paul Seymour, Robin Thomas, The Four-Colour Theorem, Journal of Combinatorial Theory, Series B 70(1), 2–44, 1997. DOI; author-hosted manuscript.

Motivation

Vehicle routing problems ask for minimum-cost vehicle routes that deliver goods from a depot to a set of customers. In the split-delivery vehicle routing problem with time windows (SDVRPTW) a customer's demand may be served by several vehicles, and each customer must be visited inside a prescribed time window. Allowing split deliveries matters in practice: for the variant without time windows, Dror and Trudeau (1989) showed empirically that splitting can save substantially, and Archetti, Savelsbergh and Speranza (2006) proved the savings can reach 50%.

Exact methods for the SDVRPTW are branch-and-price algorithms, and they rely on structural properties of optimal solutions to prune the search. Desaulniers (Operations Research 58(1), 2010) collects these properties in §2 of his paper and uses the strongest one, Corollary 2, as a family of valid inequalities (constraint (7)) in his branch-and-price-and-cut method.

Timeline (as reported by Desaulniers 2010, §§1–2).

• 1989–1990. Dror and Trudeau prove, for the SDVRP without time windows and with the triangle inequality, that some optimal solution has no two routes sharing more than one split customer.
• 2006. Gendreau, Dejax, Feillet and Gueguen observe that the property holds with time windows, derive the arc-based Corollary 1, and remark that elementary routes suffice (Remark 1).
• 2010. Desaulniers strengthens Corollary 1 to pairs of reverse arcs (Corollary 2) and exploits it as cutting planes.

Setting

An instance has $n$ customers $\mathcal N$, a start depot $0$ and an end depot $n+1$ (the same location at the beginning and end of the planning horizon), and the following data: a vehicle capacity $Q > 0$; a demand $d_i > 0$ for each customer, which may exceed $Q$; a time window $[e_v, l_v]$ for each node, shared by the two depot copies; nonnegative travel times $t_{vw}$, which include the service time at $v$; and nonnegative costs $c_{vw}$. The arc set $\mathcal A$ contains the idle arc $(0, n+1)$ and every arc $(v, w)$, $v \ne w$, with $e_v + t_{vw} \le l_w$. The triangle inequality $t_{vx} \le t_{vw} + t_{wx}$, $c_{vx} \le c_{vw} + c_{wx}$ is assumed throughout.

A route is a walk $0 \to v_1 \to \dots \to v_m \to n+1$ along arcs of $\mathcal A$, customers possibly repeated, with service start times inside the time windows that respect travel times (waiting is allowed), and nonnegative quantities delivered at its visits whose total is at most $Q$. Its cost is the sum of its arc costs. A solution is a finite family of routes, one per vehicle, with no bound on their number; it is feasible if every customer $i$ receives in total at least $d_i$, and optimal if it is feasible and no feasible solution costs less. For customers $i, j$, let $x_{ij}$ be the number of times arc $(i, j)$ is traversed, summed over all routes of a solution, and let $\mathcal A(\mathcal N) = \mathcal A \cap (\mathcal N \times \mathcal N)$.

Formalization targets

All four statements assume the triangle inequality and that the instance has a feasible solution, and assert the existence of an optimal solution with a structural property.

Goal: Corollary 2 (p. 181)

The two arcs of a pair of reverse customer arcs are used at most once in total. This is the form constraint (7) of the paper gives to the corollary.

Milestones

1. Remark 1. Some optimal solution has only elementary routes: no route visits a customer twice.
2. Theorem 1. Some optimal solution has no two distinct routes with two customers in common.
3. Corollary 1. Some optimal solution has $x_{ij} \le 1$ for all $(i, j) \in \mathcal A(\mathcal N)$.

Significance

The result. Corollary 2 turns a property of optimal solutions into linear inequalities on arc-flow variables. Adding them to the arc-flow formulation cuts off fractional points of its linear relaxation while keeping an optimal integer solution, which is how Desaulniers uses them. Remark 1 justifies pricing only elementary routes in column generation. Theorem 1 is the combinatorial fact underneath both corollaries and is reused throughout the split-delivery literature.

Formalizing it. The four results are proved in the literature (Dror–Trudeau; Gendreau et al. 2006); Desaulniers states them without proof. No machine-checked version exists. This mission produces a reusable Lean model of the SDVRPTW (instances, arc sets, feasible routes with schedules and delivery patterns, solutions, optimality) and checked proofs of these properties, including the existence of an optimal solution, which the paper takes for granted.

Difficulty

The obvious argument is local: take an optimal solution that violates the property, shift quantities between two routes, remove a visit, and shortcut. Three points make this less routine than it sounds. First, the statements are existential: each exchange must keep the solution optimal and not reintroduce a violation already removed, so one needs a termination measure that decreases under every exchange (Corollary 2 needs elementarity and the Theorem 1 property simultaneously, not two separate optimal solutions). Second, removing a visit is feasible only because the arc set is defined by time windows: the shortcut arc $(v, w)$ must be shown to exist from the schedule and the triangle inequality on travel times, and the new schedule must be built explicitly. Third, the feasible set is infinite (real quantities, unbounded walks, unbounded number of vehicles), so the existence of an optimal solution is itself a statement to prove, not a hypothesis.

Formalization scope

Namespace SplitDeliveryVRPTW.Known. Nodes are the inductive type Node n (start, cust i for i : Fin n, finish). All quantities, times and costs are real. The arc set is exactly the set the paper defines (read as "if and only if"), with arcs into the start depot and out of the end depot excluded. The triangle inequality for $t$ is imposed on pairwise distinct nodes and for $c$ on triples of arcs, where the paper's data is defined. A route is a customer list (repetitions allowed) with a time function over path positions and a quantity function over visits. A solution is an indexed family Fin m → Route I, so identical routes may appear twice. Demand satisfaction uses $\ge$, as constraint (2) does. The per-vehicle bound $\min\{d_i, Q\}$ of constraint (14) is omitted because it changes neither the feasible route patterns nor the costs.

Explicit readings of imprecise phrases:

• "split customer", "in common" (Theorem 1) are undefined in the paper. A customer two distinct routes visit is split, and the routes have it in common. This visit-based reading is at least as strong as a delivery-based one.
• Corollary 2's wording "at most one arc in set $\mathcal A^*_{ij}$ appears at most once" is read through constraint (7): the total number of traversals of the arcs of $\mathcal A^*_{ij}$ is at most one. It is stated in the equivalent form free of the choice of $\mathcal A^*(\mathcal N)$.
• "there exists an optimal solution" is conditional on feasibility, which is the hypothesis added.

Ruled-out trivializations: routes are not restricted to elementary walks (that would make Remark 1 definitional), solutions are not sets (that would forbid duplicate routes), optimality compares against solutions with any number of routes and any visit pattern, "split" is never counted over visits by the same route, capacity and time windows are part of route feasibility, and deliveries occur only at visits.

Useful infrastructure, reusable beyond this mission: shortcut lemmas for feasible routes (removing a visit), exchange lemmas between two routes, and existence of an optimum for split-delivery routing. Contributions of any of these as separate lemmas are welcome.

Selected references

• G. Desaulniers, Branch-and-Price-and-Cut for the Split-Delivery Vehicle Routing Problem with Time Windows, Operations Research 58(1):179–192, 2010. https://doi.org/10.1287/opre.1090.0713
• M. Dror, P. Trudeau, Savings by split delivery routing, Transportation Science 23(2):141–145, 1989. https://doi.org/10.1287/trsc.23.2.141
• M. Dror, P. Trudeau, Split delivery routing, Naval Research Logistics 37(3):383–402, 1990. https://doi.org/10.1002/nav.3800370304
• M. Gendreau, P. Dejax, D. Feillet, C. Gueguen, Vehicle routing with time windows and split deliveries, Technical Report 2006-851, Laboratoire Informatique d'Avignon, 2006.
• C. Archetti, M. W. P. Savelsbergh, M. G. Speranza, Worst-case analysis for split delivery vehicle routing problems, Transportation Science 40(2):226–234, 2006. https://doi.org/10.1287/trsc.1050.0117

Motivation

Many production and computing systems run jobs on parallel machines that also draw on a shared, limited resource: tools, workers, memory, power. Adding such a resource to a scheduling problem can change its complexity entirely. Błażewicz, Lenstra and Rinnooy Kan (DAM 1983) extended the three-field classification $\alpha\mid\beta\mid\gamma$ of Graham, Lawler, Lenstra and Rinnooy Kan by a resource field $res\lambda\sigma\rho$, and determined the complexity of every problem with unit-time jobs on identical or uniform machines under the makespan criterion. Their Fig. 2 separates the maximal polynomially solvable cases from the minimal NP-hard ones.

This mission formalizes the polynomial side. Two identical machines are easy under arbitrary resources (Theorem 1, due to Garey and Johnson, via maximum matching). Three identical machines with one resource are NP-hard in the strong sense (Theorem 4), and so are two uniform machines with unit resources (Theorem 3). What remains for uniform machines is settled by two algorithms: a sorting-and-shifting procedure for two uniform machines with one resource of arbitrary size (Theorem 5), and a bottleneck transportation problem for any number of uniform machines with one resource and 0–1 requirements (Theorem 6). The hardness results are the subject of the companion missions I and II.

Setting

There are $n$ jobs $J_1,\dots,J_n$ and $m$ machines $M_1,\dots,M_m$. Machine $M_i$ has speed $q_i>0$; every job has unit execution requirement, so it takes time $1/q_i$ on $M_i$. Identical machines ($P$) have $q_i=1$; uniform machines ($Q$) have arbitrary speeds. There are $l$ resources $R_h$ with positive integer sizes $s_h$, and job $J_j$ needs a nonnegative integer amount $r_{hj}$ of $R_h$ throughout its execution. The field $res\lambda\sigma\rho$ records restrictions: $\lambda$ bounds the number of resources, $\sigma$ their sizes, $\rho$ the requirements, a dot meaning "part of the input". So $res1{\cdot}{\cdot}$ is one resource with arbitrary size and requirements, and $res1{\cdot}1$ is one resource with requirements in $\{0,1\}$.

A schedule gives every job a machine $\mu(j)$ and a start time $S_j\ge0$; the job is executed during $[S_j,C_j)$ with $C_j=S_j+1/q_{\mu(j)}$. It is feasible if jobs on the same machine do not overlap and, at every time $t$, the jobs executed at $t$ use at most $s_h$ of each resource $R_h$. The makespan is $C_{\max}=\max_j C_j$. No precedence constraints occur in this mission.

Formalization targets

Goal: Theorem 5, correctness of the algorithm

For $Q2\mid res1{\cdot}{\cdot},\,p_j=1\mid C_{\max}$ with $q_1\ge q_2$: put all jobs on $M_1$ in order of nonincreasing $r_{1j}$, then repeatedly move the last job of $M_1$ to the earliest feasible time on $M_2$ after the jobs already there, as long as this strictly reduces $C_{\max}$. For every order with nonincreasing requirements, the resulting schedule $A$ is feasible and

Milestones for the goal

The paper's proof has two steps, both milestones. Call a schedule an (a)–(c) schedule when (a) $M_1$ runs its jobs back to back from time $0$ in nonincreasing $r_{1j}$, (b) $M_2$ runs its jobs in nondecreasing $r_{1k}$, and (c) every requirement on $M_1$ is at least every requirement on $M_2$.

1. The algorithm's schedule is feasible, is an (a)–(c) schedule, and is best among feasible (a)–(c) schedules.
2. Every feasible schedule can be transformed into a feasible (a)–(c) schedule with no larger $C_{\max}$.

Further results

• Theorem 1. For $P2\mid res{\cdot}{\cdot}{\cdot},\,p_j=1\mid C_{\max}$, with $G$ the graph joining two jobs when they can run together and $S$ a maximum matching of $G$, the optimal makespan is $n-|S|$.
• Theorem 6. For $Q\mid res1{\cdot}1,\,p_j=1\mid C_{\max}$ with the $s_1$ fastest machines listed first, the optimal makespan equals the optimal value of a bottleneck transportation problem that assigns jobs to slots (machine, position) with cost $k/q_i$, resource jobs only to the $s_1$ fastest machines.

Significance

Theorems 5 and 6 complete the classification of Fig. 2 for uniform machines: every special case of $Q\mid res{\cdot}{\cdot}{\cdot},\,p_j=1\mid C_{\max}$ not covered by the hardness theorems has a polynomial algorithm. Theorem 1 is the classical reduction of two-machine resource scheduling to maximum matching, the model case for later work on scheduling with conflict graphs.

The paper proves these results briefly: "clearly" for the first half of Theorem 5, "obviously" for Theorem 1, and a one-paragraph model for Theorem 6. The exchange argument of Theorem 5 is presented "in an informal way" through five steps that pass through fractional, preempted jobs. A machine-checked proof makes these arguments exact on a model with real start times. No formalization of these results is known, and the platform had no statement about resource-constrained scheduling on uniform machines before this mission.

Difficulty

With $q_1\ne q_2$ the job boundaries on the two machines are misaligned: a job on $M_2$ overlaps parts of several jobs on $M_1$, so the resource check cannot be done slot by slot, and discrete reasoning on integer time grids does not apply. The exchange argument of Theorem 5 must control the resource usage at every real time while jobs are moved between machines and reordered, and it has to end with a nonpreemptive schedule even though the paper's intermediate steps split jobs. For Theorem 1, the hard direction is the lower bound: a feasible schedule with arbitrary real start times must be converted into a matching, which is a statement about how unit jobs on two machines can overlap. For Theorem 6, one must show that restricting resource jobs to the fastest machines and to back-to-back positions loses nothing.

Formalization scope

• Model. Jobs, machines and resources are Fin n, Fin m, Fin l (0-based). Speeds are positive reals, sizes positive naturals, requirements naturals. Start times are nonnegative reals, execution intervals are half-open, and the resource constraint is checked at every real time. $C_{\max}=0$ for $n=0$. The model carries a precedence digraph for consistency with the companion missions; every statement here assumes it has no arcs.
• Implicit hypothesis. Theorems 1 and 5 assume every job fits alone ($r_{hj}\le s_h$), which the paper leaves unstated; without it no feasible schedule exists.
• The algorithm is a Lean definition following the page: the order is an argument (any nonincreasing order), "as early as possible" is the earliest start after $M_2$'s last job at which the resource constraint holds throughout, and the loop stops at the first move that does not strictly reduce $C_{\max}$.
• Optimality is always stated in full: feasibility plus a lower bound against every feasible schedule. No minimum is written as an infimum of a possibly empty set.
• Theorem 6 is stated with 0–1 slot assignments, the interpretation the paper gives to $x_{ijk}$; the page's constraint $\sum_{k=1}^{m}$ is read as $\sum_{k=1}^{n}$.
• Not formalized: the running times $O(ln^2+n^{5/2})$ (Theorem 1), $O(n\log n)$ (Theorem 5, including the phrase "This O(n log n) algorithm") and $O(n^3)$ (Theorem 6), which depend on a machine model the paper does not fix and, for Theorems 1 and 6, on cited matching and transportation algorithms.
• Ruled out: a formalization of the goal that proves optimality only against (a)–(c) schedules, against schedules with integer start times, or for one fixed tie-breaking order proves less than Theorem 5.

Contributions welcome: lemmas about step functions of resource usage on half-open intervals, a left-shifting lemma for unit-time schedules on two machines, and the exchange steps of Theorem 5 as separate lemmas.

Selected references

• J. Błażewicz, J.K. Lenstra, A.H.G. Rinnooy Kan, Scheduling subject to resource constraints: classification and complexity, Discrete Applied Mathematics 5 (1983) 11–24. https://doi.org/10.1016/0166-218X(83)90012-4
• M.R. Garey, D.S. Johnson, Complexity results for multiprocessor scheduling under resource constraints, SIAM Journal on Computing 4 (1975) 397–411. https://doi.org/10.1137/0204035
• R.L. Graham, E.L. Lawler, J.K. Lenstra, A.H.G. Rinnooy Kan, Optimization and approximation in deterministic sequencing and scheduling: a survey, Annals of Discrete Mathematics 5 (1979) 287–326. https://doi.org/10.1016/S0167-5060(08)70356-X
• S. Even, O. Kariv, An O(n^{2.5}) algorithm for maximum matching in general graphs, Proc. 16th IEEE FOCS (1975) 100–112. https://doi.org/10.1109/SFCS.1975.23

Bound $L_4$: $33,070,982 \le R$

This mission formalizes the lower bound $33,070,982 \le R$ on the number of reversible binary cellular automata on the $3 \times 3$ Moore neighborhood. Extending the conserved-landscape marker families to both centered and off-centered rules.