Many vehicles, one depot

The vehicle routing problem asks for the cheapest set of delivery routes from a depot to a set of customers when each vehicle can carry only so much. It generalizes the traveling salesman problem, which is the case of a single vehicle of unlimited capacity, and it is the operational problem behind every distribution fleet. Exact methods reach a few hundred customers; the questions that shape fleet design are structural: how does the optimal routing cost compare with the cost of a single grand tour, and how does it grow with the number of customers? Haimovich and Rinnooy Kan (1985) answered both for unit demands by bounding the optimal cost above and below in terms of the optimal TSP tour and the average distance to the depot. Chapter 11 of Snyder and Shen's Fundamentals of Supply Chain Theory (2019) presents that result with its full proof as Theorem 11.6, and it is the goal of this mission.

Setting

Nodes are the depot $0$ and customers $1, \dots, n$, with distances $c_{ij}$ that are symmetric, nonnegative and satisfy the triangle inequality (VRPMetric). Every customer has demand $1$ and every vehicle capacity $C$, so a route is a sequence of at most $C$ distinct customers, served by one vehicle that leaves the depot, visits them in order and returns; its length is routeCost c L. A solution is a family of routes visiting every customer exactly once (IsVRPSolution), with total length solutionCost; the number of routes is free. The optimal VRP value $z^*$ (vrpOpt c C) is the least total length, the optimal TSP value $z_T$ (tspOpt c) is the least length of a single route through all customers, and $\bar c$ (avgDepotDist) is the average distance from the depot to a customer.

Formalization targets

Goal: Theorem 11.6

For every metric instance with $n \ge 1$ customers and capacity $C \ge 1$,

$$\max\Big\{2\frac{n}{C}\bar c,\ z_T\Big\} \;\le\; z^* \;\le\; 2\Big\lceil\frac{n}{C}\Big\rceil\bar c + \Big(1 - \frac{1}{C}\Big)z_T.$$

This is vrp_tsp_bounds.

Supporting targets

The three steps of the book's proof: the radial bound $2\frac{n}{C}\bar c \le z^*$, obtained route by route from the triangle inequality and the capacity; the routing bound $z_T \le z^*$; and the iterated optimal tour partition bound (11.59), that for any tour $\Gamma$ through all customers some partition of its customer sequence into $\lceil n/C\rceil$ consecutive routes costs at most $2\lceil n/C\rceil\bar c + (1 - \lceil n/C\rceil/n)\,z(\Gamma)$.

The chapter's other numbered results are not targets: Proposition 11.1 (state-space relaxation of the routing dynamic program) and Theorem 11.2 (the capacitated comb inequality, proof omitted, which needs the bin-packing function $v(S)$), and Theorems 11.3, 11.5, 11.7 and Lemma 11.4 (almost-sure asymptotics of random instances and the location-based heuristic), whose proofs the book cites.

Significance

Theorem 11.6 is the quantitative link between routing and the two things a planner can estimate without solving anything: the TSP length, which grows like $\sqrt{n}$ for random customers, and the average depot distance. It says that the VRP cost is the TSP cost plus a radial term $2\bar c$ per vehicle, and that this decomposition is exact up to a factor bounded by the capacity. The radial term explains Theorem 11.7, that the optimal cost grows linearly in $n$ for fixed capacity, and the tour partition heuristic in the proof is a practical route-first-cluster-second method with a provable guarantee. The bounds are the basis of the continuous approximation formulas used in strategic distribution design.

None of these results has a machine-checked proof. The book proves Theorem 11.6 in full. The formal treatment of routes as lists and of the averaging argument over rotations of a tour is reusable for the capacitated heuristics of Sect. 11.3.

Difficulty

The upper bound is an averaging argument that is easy to state and fiddly to formalize: for each of the $n$ rotations of the tour's customer sequence, the sequence is cut into blocks of $C$, and one must count, across all rotations, how often each customer is the first or last of a block and how often each tour edge is cut. The counts, $\ell = \lceil n/C\rceil$ each, hold only after the rotations are indexed carefully, and the passage from the average to the best rotation needs the sum of the $n$ solution costs computed exactly.

The lower bound has two parts with different flavors. The radial part needs, for each route, that the closed route from the depot is at least twice the largest depot distance among its customers, which is the triangle inequality applied along the route, followed by an averaging step that uses the capacity. The routing part is a shortcutting argument: the routes of a solution concatenate into a closed walk that revisits the depot, and removing the repeated depot visits must not increase the length. The obvious idea, that a VRP solution is itself a tour, is false, and the shortcut has to be constructed.

Formalization scope

Routes are lists of customers, solutions are lists of routes, and the feasibility predicate requires nonempty routes of length at most $C$ avoiding the depot, with the concatenation of all routes a duplicate-free list containing every customer. Costs use the closed walk through the depot followed by the route. The optimal values are infima of finite nonempty sets of reals, nonempty because singleton routes are feasible when $C \ge 1$. The ceiling $\lceil n/C\rceil$ is Mathlib's Nat.ceil of the real quotient. The number of vehicles is unrestricted, as the section assumes; the fixed-fleet version of the problem is not modeled.

The TSP value $z_T$ is defined as the least route cost over all orderings of the customers, so no separate tour model is needed and the mission does not depend on the TSP mission of this series.

The definition module is shared by all five items. Problem 11.18 (tightness of both bounds) and Theorem 11.7 for deterministic instance families are natural extensions on the same definitions.

Selected references

• L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Chapter 11. https://doi.org/10.1002/9781119584445
• M. Haimovich and A. H. G. Rinnooy Kan, Bounds and heuristics for capacitated routing problems, Mathematics of Operations Research 10(4), 1985. https://doi.org/10.1287/moor.10.4.527
• P. Toth and D. Vigo (eds.), Vehicle Routing: Problems, Methods, and Applications, 2nd ed., SIAM, 2014. https://doi.org/10.1137/1.9781611973594

The problem every routing model contains

A salesman must visit $n$ cities and return home by the shortest route. The traveling salesman problem is the prototype of combinatorial optimization: easy to state, NP-hard (Karp 1972), and solved to optimality on instances with tens of thousands of nodes by branch-and-cut. In a supply chain it is the core of every vehicle routing model and of the location-routing models of the chapters that follow. Chapter 10 of Snyder and Shen's Fundamentals of Supply Chain Theory (2019) covers the symmetric metric TSP, in which distances satisfy the triangle inequality: the cutting planes of branch-and-cut (comb inequalities), the construction heuristics with their worst-case guarantees, culminating in Christofides' (1976) 3/2-approximation, and the lower bounds of Little et al. and of Held and Karp (1970). This mission formalizes those results, with Christofides' theorem as its goal.

Setting

Nodes are $N = \{1, \dots, n\}$ with distances $c_{ij}$ that are symmetric, nonnegative, zero on the diagonal and satisfy the triangle inequality $c_{ij} \le c_{ik} + c_{kj}$ (IsMetric). A tour is a visiting order $\tau$ of all the nodes, of length $z(\tau) = \sum_k c(\tau_k, \tau_{k+1})$ with indices mod $n$ (tourLength); $z^*$ is the least tour length (optTourLength). A tour has an edge set (tourEdges), and for a node set $S$ the counts of tour edges inside $S$ and leaving $S$ (edgesWithin, edgesLeaving) are the sums $\sum_{i,j \in S} x_{ij}$ and $\sum_{i \in S, j \notin S} x_{ij}$ of the integer programming formulation. A comb is a handle $H$ with an odd number $s \ge 3$ of pairwise disjoint teeth, each meeting both $H$ and its complement (IsComb); when every tooth has exactly two nodes the comb is a 2-matching configuration.

The nearest neighbor heuristic always moves to a nearest unvisited node (IsNearestNeighborTour); the nearest insertion heuristic grows a partial tour by inserting the unvisited node nearest to it at the cheapest position (IsNearestInsertionRun, with cycleLength and distToTour). The minimum spanning tree heuristic doubles an MST (IsMST, graphWeight), takes an Eulerian tour of the doubled tree and shortcuts it, visiting the nodes in order of first appearance (IsShortcut). Christofides' heuristic instead adds to the MST a minimum-weight perfect matching on its odd-degree nodes (oddNodes, IsMinMatchingOn) before taking the Eulerian tour. A 1-tree rooted at $r$ is a spanning tree on the other nodes plus two edges at $r$ (Is1Tree); the revised distances $c'_{ij} = c_{ij} + \lambda_i + \lambda_j$ (revisedCost) define the Held-Karp bound.

Formalization targets

Goal: Theorem 10.13

For every metric instance, every minimum spanning tree $T^*$, every minimum-weight perfect matching $M$ on the odd-degree nodes of $T^*$, every Eulerian tour of $T^* + M$ and its shortcut $\tau$,

$$z(\tau) \;\le\; \tfrac{3}{2}\, z^*.$$

This is christofides_bound.

Supporting targets

Theorem 10.1, the reduced-matrix bound $\sum_i \rho_i + \sum_j \kappa_j \le z^*$; Theorem 10.2, Proposition 10.3 and Theorem 10.4, the 2-matching and comb inequalities valid for every tour; Theorem 10.6, $z_{NN} \le \frac{1}{2}(\lceil\log_2 n\rceil + 1) z^*$; Theorem 10.7, $z_{NI} \le 2z^*$; Lemma 10.9, $z(T^*) \le z^*$; Theorem 10.10, Euler's theorem; Theorem 10.11, $z_{MST} \le 2z^*$; Lemma 10.12, the handshaking lemma; Lemma 10.15, the 1-tree bound; Lemma 10.16, the revised distance identities; Theorem 10.17, the Held-Karp bound. Theorem 10.5 (no constant-factor approximation unless P = NP), Theorem 10.8 and the second part of Theorem 10.6 (tightness instances), Lemma 10.14 (Euclidean tours do not cross), Lemma 10.18 (the integrality gap) and Theorem 10.19 (the Beardwood-Halton-Hammersley asymptotics) are not targets.

Significance

Christofides' bound was the best approximation guarantee for the metric TSP for over forty years, until the $3/2 - 10^{-36}$ of Karlin, Klein and Oveis Gharan (2021), and it is the reference point against which every heuristic in the chapter is measured: nearest neighbor has no constant bound, nearest insertion and the MST heuristic achieve $2$, Christofides $3/2$. The comb inequalities are the cuts that make branch-and-cut work, and the Held-Karp bound is the lower bound that tells a practitioner how far a heuristic tour is from optimal. Theorem 10.1 is the historical bounding rule of the first branch-and-bound algorithm.

None of these results has a machine-checked proof. The book proves Theorems 10.2, 10.11, 10.13 and 10.17 and Proposition 10.3 and Lemma 10.9, cites Theorems 10.6, 10.7 and 10.10, and leaves Theorem 10.4 and Lemmas 10.12 and 10.16 as exercises. The formal infrastructure for tours, shortcutting and Eulerian walks is reusable for the vehicle routing chapter.

Difficulty

Christofides' argument has three steps and each has a formal obstacle. The MST bound is a spanning-path argument that needs the removal of an edge from a tour to yield a tree, in Mathlib's terms a connected acyclic subgraph of the complete graph. The matching bound is the subtle one: the optimal tour shortcut to the odd-degree nodes, of length at most $z^*$ by the triangle inequality, is an even cycle whose alternate edges form two perfect matchings on those nodes, the cheaper of which costs at most $z^*/2$; formalizing the decomposition of a cycle on an even node set into two matchings, and the shortcut's length bound, is the bulk of the work. The final step, that shortcutting an Eulerian walk does not lengthen it, is an induction along the walk using the triangle inequality on the skipped stretches, and it needs the first-occurrence order to be handled explicitly.

The obvious approach to the heuristic bounds, comparing the heuristic tour directly with the optimal tour, fails; every proof goes through a spanning tree. For nearest insertion the tree is Prim's, grown in the same order as the insertions, and the bound charges each insertion cost to a tree edge; for nearest neighbor the argument of Rosenkrantz et al. bounds the sum of the $k$ largest steps by $2z^*$ for each $k$ and sums a geometric series, which is where the logarithm comes from.

The comb inequalities are counting arguments on degrees, but the general comb of Theorem 10.4 needs the case analysis of how a tour enters and leaves each tooth. Euler's theorem in the sufficiency direction is Hierholzer's construction, which is not in Mathlib.

Formalization scope

Tours are permutations of Fin n, so a tour is an ordering rather than an edge set, and every tie-breaking of a heuristic is covered by a predicate on its output rather than by an algorithm. Graphs are Mathlib SimpleGraphs on Fin n; the multigraphs of the two tree heuristics are represented by closed walks with prescribed edge multisets, and shortcutting is the first-occurrence order along the walk's node sequence. All degree and edge-set computations use classical decidability. Theorems on tours assume $n \ge 3$ where a tour must have distinct edges, $n \ge 1$ otherwise.

Theorem 10.1 is stated for the reduction of the full off-diagonal matrix, because the book's upper-triangular version is false: a random metric instance violates it, since the last row and first column of a triangular matrix are empty and the two edges at a node need not be one row and one column entry. The full-matrix version is the statement of Little et al. It is stated for $n \ge 2$, because a one-node "tour" is a self-loop that no off-diagonal entry constrains.

Theorem 10.4 is stated with the comb inequality's right-hand side corrected to $|H| + \sum_k(|T_k| - 1) - \tfrac{1}{2}(s+1)$, the standard form. The book prints $+\tfrac{1}{2}(s-1)$, which contradicts its own 2-matching special case (10.15) and is weaker by $s$. The corrected statement implies the printed one.

The $1$-tree root is an explicit node $r$, the book's node $1$. The nearest insertion run is a sequence of lists indexed by iteration, and the theorem compares the $n$-th list's closed length with $z^*$; a run always exists, so the hypothesis is satisfiable.

The definition module is shared by all fifteen items. Theorem 10.8 and Problem 10.12 (tightness of the bounds of $2$), the second part of Theorem 10.6, and Lemma 10.18 on the integrality gap are natural extensions on the same definitions.

Selected references

• L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Chapter 10. https://doi.org/10.1002/9781119584445
• N. Christofides, Worst-case analysis of a new heuristic for the travelling salesman problem, Report 388, GSIA, Carnegie Mellon University, 1976; reprinted in Operations Research Forum 3, 2022. https://doi.org/10.1007/s43069-021-00101-z
• D. J. Rosenkrantz, R. E. Stearns and P. M. Lewis II, An analysis of several heuristics for the traveling salesman problem, SIAM Journal on Computing 6(3), 1977. https://doi.org/10.1137/0206041
• M. Held and R. M. Karp, The traveling-salesman problem and minimum spanning trees, Operations Research 18(6), 1970. https://doi.org/10.1287/opre.18.6.1138
• J. D. C. Little, K. G. Murty, D. W. Sweeney and C. Karel, An algorithm for the traveling salesman problem, Operations Research 11(6), 1963. https://doi.org/10.1287/opre.11.6.972
• M. Grötschel and M. W. Padberg, On the symmetric travelling salesman problem I and II, Mathematical Programming 16, 1979. https://doi.org/10.1007/BF01582116

Motivation

Exact methods for the resource-constrained project scheduling problem — branch-and-bound over activity lists or over start-time assignments, and the lower-bound computations inside them — live or die by how much of the search space can be discarded before it is enumerated. The standard tool is constraint propagation: deducing, from the precedence, resource and time-window data, new precedence relations $i\to j$ that every feasible schedule must satisfy, and tighter time windows for the activities. Brucker and Knust's Section 3.6 (doi:10.1007/978-3-642-23929-8) presents the family of interval consistency tests — input, output, input-or-output and their negations — that constraint-programming schedulers apply at every node of the search, following Carlier and Pinson (An algorithm for solving the job-shop problem, Management Science 35, 1989, doi:10.1287/mnsc.35.2.164) and Baptiste, Le Pape and Nuijten (Constraint-Based Scheduling, Kluwer, 2001, doi:10.1007/978-1-4615-1479-4). Every test is an instance of one theorem, Theorem 3.7, and its cumulative-resource analogue, Theorem 3.8. Those two theorems, and the tests as their corollaries, are this mission.

Setting

The instance is the RCPSP of mission I: activities $0,\dots,n-1$ with integer processing times $p_i$, renewable resources $k$ with capacities $R_k$ and demands $r_{ik}$, and precedence arcs; a schedule is an integer start-time vector $S$, feasible when it meets the precedences and never exceeds a capacity. Section 3.6 adds three things.

Relations. A conjunction $i\to j$ holds in $S$ when $S_i+p_i\le S_j$. Two activities are parallel, $i\parallel j$, when they overlap for at least one time unit, and a disjunction $i-j$ is the negation of that: $i\to j$ or $j\to i$. The instance carries a set $C$ of conjunctions and a set $D$ of disjunctions that every feasible schedule must satisfy; initially $C_0$ is the precedence relation and $D_0$ the pairs whose combined demand exceeds some capacity, and propagation adds to them.

Disjunctive sets. A set $I$ of at least two activities is disjunctive when any two of its members are related by a disjunction or a conjunction, so no two are ever processed together: the activities of a unit-capacity resource, the jobs of a single machine, the operations of one job in a shop. Its total processing time is $P(I)=\sum_{i\in I}p_i$.

Time windows. Each activity has a head $r_i$ and a deadline $d_i$, and a feasible schedule has $r_i\le S_i$ and $S_i+p_i\le d_i$. An activity starts first in a set $J$ when no activity of $J$ starts earlier, and ends last when none completes later.

For a cumulative resource $k$ the work of activity $i$ is $w_i=r_{ik}p_i$ and $W(J)=\sum_{i\in J}w_i$.

Formalization targets

Goal — Theorem 3.7 (printed p. 169)

Let $I$ be a disjunctive set, $J\subseteq I$, and $J',J''$ proper subsets of $J$ with $J'\cup J''\ne\emptyset$. If

$$\max_{\substack{\nu\in J\setminus J',\ \mu\in J\setminus J''\\ \nu\ne\mu}}\bigl(d_\mu-r_\nu\bigr)<P(J),$$

then in every feasible schedule an activity from $J'$ starts first in $J$ or an activity from $J''$ ends last in $J$.

The first infeasibility test (printed p. 169)

If some nonempty $J\subseteq I$ has $\max_{\mu\in J}d_\mu-\min_{\nu\in J}r_\nu<P(J)$, no feasible schedule exists.

The input test (3.123) and the output test (3.124) (printed p. 171)

For $\Omega\subseteq I$ nonempty and $i\in I\setminus\Omega$: if $\max_{\mu\in\Omega\cup\{i\}}d_\mu-\min_{\nu\in\Omega}r_\nu<P(\Omega)+p_i$ then $i\to j$ for all $j\in\Omega$; symmetrically, if $\max_{\mu\in\Omega}d_\mu-\min_{\nu\in\Omega\cup\{i\}}r_\nu<P(\Omega)+p_i$ then $j\to i$ for all $j\in\Omega$.

The input-or-output test (printed p. 170)

For $i,j\in J\subseteq I$, $|J|\ge 2$: if $\max_{\mu\in J\setminus\{j\}}d_\mu-\min_{\nu\in J\setminus\{i\}}r_\nu<P(J)$ then $i$ starts first in $J$ or $j$ ends last in $J$, and $i\to j$ when $i\ne j$.

Theorem 3.8 (printed p. 186)

For a cumulative resource $k$, $J\subseteq I_k$ and proper subsets $J',J''$ of $J$: if $R_k\bigl(\max_{\mu\in J\setminus J''}d_\mu-\min_{\nu\in J\setminus J'}r_\nu\bigr)<W(J)$ then an activity from $J'$ starts first in $J$ or an activity from $J''$ ends last in $J$.

Significance

Theorem 3.7 is the single statement behind a whole toolbox. Every interval consistency test in the literature — the input and output tests that fix a new conjunction, the input-or-output test, the negation tests that only shrink a window — is the theorem with a particular choice of $J'$ and $J''$, and the book's Section 3.6.4 derives them one by one. A propagation engine that applies these tests to a fixpoint is what makes branch-and-bound for the job shop and the RCPSP practical; Carlier and Pinson's solution of the 10×10 job-shop instance is the historical demonstration. Theorem 3.8 extends the same reasoning from disjunctive to cumulative resources by replacing "no overlap" with "at most $R_k$ units per time unit", the energetic-reasoning viewpoint that the rest of Section 3.6.5 develops.

The results are elementary and proved; formalizing them fixes, once, what "feasible" means in the presence of the relation sets $C$ and $D$ and time windows, on top of the RCPSP model of mission I. That layer is reusable: the start-start distance matrix of Section 3.6.2 and the symmetric-triple rules of Section 3.6.3 are statements about the same schedules and the same relations. Nothing here is on the platform or in Mathlib.

Difficulty

The obvious argument for Theorem 3.7 is the correct one, and its difficulty is in the bookkeeping. If no activity of $J'$ starts first and none of $J''$ ends last, the first starter is some $\nu\in J\setminus J'$ and the last finisher some $\mu\in J\setminus J''$, and every activity of $J$ is processed inside $[S_\nu,\,S_\mu+p_\mu]\subseteq[r_\nu,d_\mu]$. Since the activities of a disjunctive set are pairwise non-overlapping, their total length $P(J)$ fits in that interval, contradicting (3.121). The formal work is the packing lemma: pairwise disjoint integer intervals inside an interval of length $L$ have total length at most $L$, which requires ordering the activities by start time and an induction that Mathlib does not supply.

The subtle point is the restriction $\nu\ne\mu$ in (3.121). The book allows it because "an activity which starts first cannot complete also last" when there are at least two activities with positive durations. The formal statement reads "starts first" and "ends last" with $\le$, which makes the theorem true without a positivity hypothesis: when the restriction empties the index set, $J\setminus J'=J\setminus J''=\{x\}$, the conclusion holds because $x$ cannot be both the unique first starter and the unique last finisher of a disjunctive set with two or more members. A solver should expect to handle that corner separately.

For the tests the extra step is turning "starts first" into a conjunction $i\to j$, which uses the disjunction between $i$ and $j$ together with positive processing times: with $p_j=0$ an activity could start at the same instant as $i$ without violating the disjunction, so the tests carry the positivity hypothesis that Theorem 3.7 itself does not need. Theorem 3.8 replaces the packing lemma by a work-counting lemma: over an interval of length $L$ a resource of capacity $R_k$ supplies at most $R_kL$ units, and every activity of $J$ consumes $r_{ik}p_i$ of them.

Formalization scope

Schedules are integer start-time vectors on Fin n, as in missions I and II, and a feasible schedule of this mission is one that is FeasibleSchedule for the RCPSP instance (mission I), respects the arcs of $C$ (RespectsArcs, mission II), satisfies the disjunctions of $D$ and lies within the time windows; these four hypotheses are the book's "feasible schedule" in Section 3.6 and are carried on every statement, although the arguments use only the last two, or, for Theorem 3.8, the resource constraint and the windows. The sets $C$ and $D$ are parameters, not derived from the instance, since propagation enlarges them.

Every inequality "$\max(\cdot)-\min(\cdot)<P$" is stated as the family of inequalities $d_\mu<r_\nu+P$ over the same index pairs. This is equivalent, avoids natural-number subtraction, and gives an empty index set the value the convention $\max\emptyset=-\infty$ would: the hypothesis is then vacuous. "Starts first" and "ends last" use $\le$. Proper-subset hypotheses $J'\subset J$, $J''\subset J$ are the book's; the first infeasibility test needs $J$ nonempty, and the input-or-output test needs $|J|\ge 2$.

A trivializing reading is ruled out on the disjunctive side by the nonemptiness hypotheses (an empty $J$ would make the infeasibility test's family vacuous and its conclusion false) and on the cumulative side by the observation that Theorem 3.8 with $J'=J''=\emptyset$ asserts infeasibility, which is the book's intended reading. Welcome contributions beyond the milestones: the input-negation and output-negation tests, the window-tightening rules of Section 3.6.4, and the SSD-matrix results of Section 3.6.2.

Selected references

• Peter Brucker and Sigrid Knust, Complex Scheduling, 2nd ed., Springer, 2012, Section 3.6. doi:10.1007/978-3-642-23929-8
• Jacques Carlier and Eric Pinson, An algorithm for solving the job-shop problem, Management Science 35 (1989). doi:10.1287/mnsc.35.2.164
• Philippe Baptiste, Claude Le Pape and Wim Nuijten, Constraint-Based Scheduling, Kluwer, 2001. doi:10.1007/978-1-4615-1479-4
• Ulrich Dorndorf, Erwin Pesch and Toàn Phan-Huy, Constraint propagation techniques for the disjunctive scheduling problem, Artificial Intelligence 122 (2000). doi:10.1016/S0004-3702(00)00040-0

Motivation

When several processors share a workload, the first question is how long the workload takes if it is spread out as well as possible. If a job may be interrupted and resumed later, possibly on another processor — preemption, the setting of operating systems, of communication links and of any resource that can be time-shared — the answer is a closed formula, and it is one of the oldest results in scheduling: McNaughton's wrap-around rule of 1959 (Scheduling with deadlines and loss functions, Management Science 6, doi:10.1287/mnsc.6.1.1) shows that on identical machines the optimal makespan is the larger of the longest job and the average load. Horvath, Lam and Sethi (A level algorithm for preemptive scheduling, Journal of the ACM 24, 1977, doi:10.1145/321992.321995) extended this to machines of different speeds, and Gonzalez and Sahni (Preemptive scheduling of uniform processor systems, Journal of the ACM 25, 1978, doi:10.1145/322047.322055) gave the fast algorithm with few preemptions. Brucker's Chapter 5 (doi:10.1007/978-3-540-69516-5) presents the level-algorithm version, and this mission formalizes the statements it proves about schedules.

Setting

There are $n$ jobs with processing requirements $p_1,\dots,p_n>0$ and $m$ uniform machines with speeds $s_1,\dots,s_m>0$: running job $i$ on machine $j$ for a period of length $\ell$ performs $s_j\ell$ units of its requirement, so the whole job would take $p_i/s_j$ time units there. Identical machines are the case $s_1=\dots=s_m=1$.

A preemptive schedule is a finite list of pieces, each a job, a machine, a start time and a stop time. It is feasible for the data $(s,p)$ when every piece lies in $[0,\infty)$, no two pieces on the same machine overlap, no two pieces of the same job overlap (a job is on at most one machine at any instant), and every job $i$ receives total work exactly $p_i$ over its pieces. Its makespan $C_{\max}$ is the largest stop time; the completion time $C_i$ of job $i$ is the largest stop time of one of its pieces. A schedule is nonpreemptive when every job consists of a single piece.

Following Section 5.1.2 the data are sorted, $p_1\ge\dots\ge p_n$ and $s_1\ge\dots\ge s_m$, with $n\ge m$, and one writes $P_j=\sum_{i\le j}p_i$, $S_j=\sum_{i\le j}s_i$. For a set $A$ of jobs, $h(A)=S_{|A|}$ if $|A|\le m$ and $h(A)=S_m$ otherwise: the largest combined speed that $|A|$ jobs can use at one instant.

Formalization targets

Goal — Theorem 5.8 (printed p. 127)

The optimal makespan of $Q\mid pmtn\mid C_{\max}$ is the bound (5.5):

$$w \;=\; \max\Bigl\{\max_{j=1}^{m-1}\frac{P_j}{S_j},\ \frac{P_n}{S_m}\Bigr\} ,$$

in the sense that some feasible preemptive schedule has makespan exactly $w$ and no feasible preemptive schedule has a smaller makespan.

The lower bound (5.5) (printed p. 125)

Every feasible preemptive schedule has makespan at least $w$.

$P\mid pmtn\mid C_{\max}$ (printed p. 108)

On identical machines, $LB=\max\{\max_i p_i,\ \tfrac1m\sum_i p_i\}$ is a lower bound on the makespan and is attained by some feasible preemptive schedule.

Condition (5.8) (printed p. 129)

The jobs can be scheduled preemptively within $[0,T]$ if and only if $\sum_{i\in A}p_i\le T\,h(A)$ for every set $A$ of jobs.

Theorem 5.7 (printed p. 121)

For $P\mid pmtn\mid\sum w_iC_i$ with nonnegative weights there is an optimal schedule without preemption.

Significance

Theorem 5.8 turns an optimization over an infinite family of schedules into a formula in the data, and the formula is tight in both directions: each of its terms is a resource bound that some schedule meets exactly. That is what makes preemptive makespan minimization one of the few parallel-machine problems that is solvable at all — its nonpreemptive counterpart $P2\parallel C_{\max}$ is NP-hard (p. 124) — and it is why the preemptive relaxation appears as a bound inside branch-and-bound methods for the nonpreemptive problems.

Condition (5.8) is the form in which the result is reused. It is a Hall-type condition, one inequality per set of jobs, and it is exactly what Section 5.1.2 needs to prove Theorem 5.9, which decides $Q\mid pmtn; r_i\mid L_{\max}$ by a maximum flow in an expanded network. Theorem 5.7 is the complementary statement for the other classical objective: for total weighted completion time preemption buys nothing, so the nonpreemptive solutions of Section 5.1.1 are optimal in the larger class too.

On status: every statement here is classical and proved, and the formalization adds a checked model of preemptive schedules. Mathlib has no scheduling material, and the platform's SchedulingAlgorithms series so far models only single-machine sequences (missions I, II, IV) and two-machine permutation flow shops (mission III), none of which allow a job to be split. The piece-list model of this mission is the first reusable object for preemptive and parallel-machine problems, and the later sections of Chapter 5 — $Q\mid pmtn; r_i\mid L_{\max}$, $P\mid pmtn\mid L_{\max}$ — are stated in it.

Difficulty

The obvious first idea for the goal is to run McNaughton's rule with the speeds ignored. It fails on uniform machines: filling machines one after another does not respect the constraint that a long job on a slow machine is not done when a short job on a fast one is. The correct idea is the level algorithm — always process the jobs of highest remaining requirement on the fastest free machines, sharing machines among tied jobs — and the difficulty is in the analysis rather than the idea. The proof of Theorem 5.8 has to show that the schedule it produces ends exactly at one of the terms of $w$: either no machine idles before the end, giving $P_n/S_m$, or the machines finish in speed order with the first $j$ jobs busy from time $0$, giving $P_j/S_j$. Making that case analysis rigorous requires tracking that the order of remaining requirements is preserved over time (the invariant (5.6)) and that ties are broken consistently.

A second, formal difficulty is that the level algorithm's output is defined by continuous-time events (the next completion, the next time two levels coincide), so producing an explicit finite list of pieces with the required properties is itself a construction. Any proof must build a concrete schedule; "the infimum of makespans equals $w$" is not the goal.

For the lower bound the trap is the opposite: it is tempting to argue only with total capacity $S_mT$, which gives $P_n/S_m$ but not $P_j/S_j$. The latter needs the rule that a job is on at most one machine at a time, so that $j$ jobs run at combined speed at most $S_j$; a model that let a job be split across machines simultaneously would make the theorem false, and the definition of feasibility rules it out explicitly.

Formalization scope

A schedule is a List of Pieces over jobs Fin n and machines Fin m, with real start and stop times. Feasibility is the three-part condition of the Setting, disjointness of two pieces meaning one stops no later than the other starts. Work is measured with the machine's speed, so the same definitions cover identical machines as the constant speed $1$. Pieces of length zero and unsorted lists are allowed; both are harmless.

The sorted orders are hypotheses Antitone p and Antitone s, the speeds and requirements are positive, $m\ge 1$ and, where the book assumes it, $n\ge m$. The book's normalization $s_1=1$ is not assumed: every statement here is invariant under scaling all speeds, and the book uses the normalization only for a running-time estimate. The bound $w$ is defined as the maximum of an explicit nonempty finite set, so no supremum of an empty or unbounded set occurs; $LB$ takes a proof that $n\ge 1$ so that $\max_i p_i$ is meaningful.

Two things are deliberately not stated. The level algorithm itself is not transcribed: Theorem 5.8 is stated as the existence of an optimal schedule of makespan $w$, which is what its proof establishes. And Theorem 5.9, the flow characterization for $Q\mid pmtn; r_i\mid L_{\max}$, is left for a later mission, since it needs release times and the expanded network on top of this model.

A trivializing reading is excluded by the existential form of the goal and of Theorem 5.7: each asserts that an optimal schedule exists, not merely that any optimal schedule has a property. A proof of the goal has to construct a schedule; a proof of Theorem 5.7 has to construct a nonpreemptive one that beats every preemptive competitor. Contributions welcome beyond the milestones: a general lemma that a feasible schedule can be normalized to sorted, positive-length pieces, and a proof that (5.8) for the sets $\{1,\dots,j\}$ is equivalent to $w\le T$.

Selected references

• Peter Brucker, Scheduling Algorithms, 5th ed., Springer, 2007, Chapter 5. doi:10.1007/978-3-540-69516-5
• Robert McNaughton, Scheduling with deadlines and loss functions, Management Science 6 (1959). doi:10.1287/mnsc.6.1.1
• E. C. Horvath, S. Lam and R. Sethi, A level algorithm for preemptive scheduling, Journal of the ACM 24 (1977). doi:10.1145/321992.321995
• Teofilo Gonzalez and Sartaj Sahni, Preemptive scheduling of uniform processor systems, Journal of the ACM 25 (1978). doi:10.1145/322047.322055

Motivation

The NRL Plasma Formulary is a standard desk reference of the plasma-physics community: a compilation of the formulas, constants and unit conversions used in daily practice. Its opening section, "Numerical and Algebraic" (p. 3 of the 2013 edition), collects the few purely mathematical identities the rest of the handbook leans on. Two of them are exact summation formulas rather than approximations, and the first is the Rothe–Hagen identity, quoted there as valid "for all complex $x$, $y$, $z$ except when singular" and attributed to H. W. Gould's work on binomial coefficient summations.

Unlike the handbook's numerical entries, this identity is a theorem with a precise hypothesis set, and it is exactly the kind of entry a reader takes on trust. It generalizes the Vandermonde convolution, it is the coefficient identity underlying the generalized binomial series, and it specializes to Abel's binomial theorem. Formalizing it turns one line of a reference handbook into a machine-checked statement and produces, as a by-product, a reusable Lean development of binomial coefficients with an arbitrary complex upper index.

Setting

For a complex number $w$ and a natural number $k$, the generalized binomial coefficient is the falling factorial divided by a factorial,

$$\binom{w}{k} \;=\; \frac{w(w-1)\cdots(w-k+1)}{k!} \;=\; \frac{1}{k!}\prod_{j=0}^{k-1}(w-j),$$

with the empty-product convention $\binom{w}{0} = 1$. It is a polynomial in $w$ of degree $k$, and it agrees with the usual binomial coefficient when $w$ is a natural number.

Fix complex parameters $x$, $y$, $z$ and, for $k \in \mathbb{N}$, consider the Rothe factor

$$A_k(x,z) \;=\; \frac{x}{x+kz}\binom{x+kz}{k},$$

which is defined whenever $x + kz \neq 0$. The factor $x+kz$ in the denominator cancels against the leading factor of the falling factorial, so $A_k(x,z)$ extends to a polynomial in $x$ and $z$: $A_0(x,z) = 1$ and, for $k \ge 1$,

$$A_k(x,z) \;=\; \frac{x\,(x+kz-1)(x+kz-2)\cdots(x+kz-k+1)}{k!}.$$

Both forms occur in the literature; the mission carries both and asks for the comparison between them, because the quotient form is the one printed in the handbook while the polynomial form is the one that carries no side condition.

Formalization targets

Goal — the Rothe–Hagen identity, as printed

For complex $x,y,z$ and $n \in \mathbb{N}$, provided $x+kz \neq 0$ and $y+kz \neq 0$ for every $0 \le k \le n$, and $x+y+nz \neq 0$,

$$\sum_{k=0}^{n} \frac{x}{x+kz}\binom{x+kz}{k}\;\frac{y}{y+(n-k)z}\binom{y+(n-k)z}{n-k} \;=\; \frac{x+y}{x+y+nz}\binom{x+y+nz}{n}.$$

This is the handbook's line, with its "except when singular" proviso made explicit as the three non-vanishing hypotheses.

Stronger — the identity with no side condition

$$\sum_{k=0}^{n} A_k(x,z)\,A_{n-k}(y,z) \;=\; A_n(x+y,z),$$

in terms of the polynomial form $A_k$ above. This version holds for all complex $x,y,z$, with no exceptional locus, and implies the printed form wherever the latter's denominators are non-zero.

Supporting targets

$$\binom{w+1}{k+1} = \binom{w}{k} + \binom{w}{k+1}, \qquad \sum_{k=0}^{n}\binom{x}{k}\binom{y}{n-k} = \binom{x+y}{n}.$$

The first is Pascal's rule for a complex upper index; the second is the Vandermonde convolution over $\mathbb{C}$, which is the case $z = 0$ of the goal.

Significance

The identity is the convolution law of the generalized binomial series: the formal power series $\mathcal{B}_z(t)$ solving $\mathcal{B} = 1 + t\,\mathcal{B}^{z}$ satisfies $\mathcal{B}_z(t)^x = \sum_{n \ge 0} A_n(x,z)\,t^n$, so the goal is the statement $\mathcal{B}_z^x \cdot \mathcal{B}_z^y = \mathcal{B}_z^{x+y}$ read off coefficientwise (Graham–Knuth–Patashnik, Concrete Mathematics, §5.4). Consequences include Abel's binomial theorem, the Lagrange-inversion count of $z$-ary trees, and ballot-type identities in lattice-path enumeration.

Mathlib provides the Vandermonde convolution for natural-number arguments (Nat.add_choose_eq), the ascending and descending Pochhammer polynomials, and Ring.choose for binomial rings; it does not contain the Rothe–Hagen identity in any form. The four statements of this mission are therefore new formal content, and the complex-upper-index binomial API they force is reusable well beyond the mission.

The identity is classical and has been proved many times since Rothe (1793) and Hagen (1891), with the modern treatment in Gould's papers; nothing here is open mathematics. What is missing is a machine-checked proof.

Difficulty

The obvious attack — induction on $n$ using Pascal's rule — does not close as stated: the summand $A_k(x,z)$ is not Pascal-stable, since shifting $x$ by $1$ moves $x+kz$ for every $k$ at once, and the induction hypothesis is about a different family. The standard proofs instead treat both sides as polynomials in $x$ and $y$ for fixed $z$ and $n$, verify the identity on an infinite set of points where a combinatorial reading is available, and conclude by the identity theorem for polynomials; or they extract coefficients from the generalized binomial series via Lagrange inversion. Either route needs infrastructure: a two-variable polynomial-identity argument over $\mathbb{C}$, or a formal-power-series compositional inverse.

A second, more prosaic difficulty is the singular locus. The printed identity divides by $x+kz$ for every $k \le n$, and in Lean division by zero returns zero rather than failing, so a formalization that drops the non-vanishing hypotheses states a different — and in general false — claim.

Formalization scope

All statements are over $\mathbb{C}$. The generalized binomial coefficient is defined as an explicit product over Finset.range k divided by (k ! : ℂ), so $\binom{w}{0} = 1$ holds definitionally and no Nat.choose coercion enters. Sums run over Finset.range (n+1), with the complementary index written as the truncated natural subtraction n - k; inside that range this is the ordinary $n-k$, so the truncation convention is never exercised.

The proviso "except when singular" is formalized as three explicit hypotheses — $x+kz \ne 0$ for all $k \le n$, $y+kz \ne 0$ for all $k \le n$, and $x+y+nz \ne 0$ — rather than by relying on Lean's junk value for division by zero. These hypotheses are satisfiable (for instance $z = 0$, $x = y = 1$), so the goal is not vacuous, and they constrain only denominators, so they do not trivialize the sum.

The singularity-free milestone commits to a total function rotheA defined by cases on $k$, with value $1$ at $k = 0$; the comparison milestone pins that function to the quotient form under the non-vanishing hypothesis, so the mission cannot be satisfied by proving facts about a differently normalized object.

Contributions welcome beyond the milestones: complex-upper-index binomial API (symmetry, negation $\binom{-w}{k} = (-1)^k\binom{w+k-1}{k}$, polynomiality in the upper index), and any formal-power-series development supporting Lagrange inversion.

Selected references

• J. D. Huba, NRL Plasma Formulary, Naval Research Laboratory, 2013, p. 3, "Numerical and Algebraic" (Rothe–Hagen identity). https://www.nrl.navy.mil/News-Media/Publications/NRL-Plasma-Formulary/
• H. W. Gould, "Note on Some Binomial Coefficient Identities of Rosenbaum", Journal of Mathematical Physics 10, 49 (1969). https://doi.org/10.1063/1.1664760
• H. W. Gould and J. Kaucky, "Evaluation of a Class of Binomial Coefficient Summations", Journal of Combinatorial Theory 1, 233–247 (1966). https://doi.org/10.1016/S0021-9800(66)80051-9
• R. L. Graham, D. E. Knuth, O. Patashnik, Concrete Mathematics, 2nd ed., Addison-Wesley, 1994, §5.4 (generalized binomial series).

Finite representations in convex geometry

A convex combination expresses a point as a weighted average of other points. Such representations connect geometric sets with finite lists of coordinates and coefficients. A point in a convex hull may initially be described using many generators, even when the ambient space has small dimension. Carathéodory's theorem gives a bound depending only on that dimension. Grünbaum presents this result as a basic theorem of convexity in Convex Polytopes, §2.3, Theorem 5, printed page 15 (the supplied source PDF, page 33).

Sets, points, and weights

Fix a natural number $d$. Real $d$-space consists of vectors with $d$ real coordinates. Let $A$ be any subset of this space. A convex combination of points of $A$ is a finite sum of those points multiplied by nonnegative real coefficients, with the coefficients adding to one. The convex hull $\operatorname{conv} A$ is the set of all such combinations; equivalently, it is the smallest convex set containing $A$.

The generating set $A$ can be finite or infinite. It need not be closed, bounded, or convex. Membership of a point $x$ in its convex hull is the sole geometric assumption. The theorem concerns exact equality of vectors, so the representation is not an approximation or a limiting expression.

A dimension bound for every hull point

For every $x\in\operatorname{conv} A$, find points $v_0,\ldots,v_d\in A$ and real numbers $w_0,\ldots,w_d$ satisfying

$$w_i\geq 0\quad(0\leq i\leq d),\qquad \sum_{i=0}^{d}w_i=1,\qquad x=\sum_{i=0}^{d}w_i v_i.$$

This is the complete target of Theorem 2.3.5. The witnesses may depend on $d$, $A$, and $x$. No single selection of points must work for every point of the hull. Repeated points are permitted, and some coefficients may be zero. Thus the fixed list of $d+1$ positions can express a combination that uses fewer distinct points.

What the representation provides

The result gives a finite certificate for membership in a convex hull whose length is controlled by dimension rather than by the size of the generating set. In the plane it gives three positions, and in three-dimensional space it gives four. Infinite generating sets remain within the same statement: once a particular hull point is chosen, only finitely many generators are needed for its certificate.

The mission asks for a formal proof of this known mathematical result in its fixed-length formulation. Its content is the existence of points and normalized coefficients together. Supplying coefficients without ensuring that their points lie in $A$, or supplying a finite representation without the dimension bound, would leave part of the target unestablished.

The constraint that must be met

The definition of the convex hull guarantees a finite representation but does not directly fix its length at $d+1$. The dimension bound must hold while preserving nonnegativity, normalization, membership in the original generating set, and exact equality with the selected point. None of these constraints can be replaced by a condition on nearby points or on the closure of $A$.

Scope and boundary conventions

The coordinate model is Fin d → ℝ. Both the point list and the coefficient list are indexed by Fin (d + 1), corresponding to the source indices from zero through $d$. The convex hull, finite sums, and real scalar multiplication have their standard mathematical meanings. No additional geometric definition is needed.

Dimension zero has one position in the representation. If $A$ is empty, its convex hull is empty, so there is no hull point to represent. A singleton generating set and sets contained in a proper affine subspace are allowed. Neither strict positivity of the weights nor affine independence of the selected points is required. The target does not assert uniqueness of a representation.

Selected reference

Branko Grünbaum, Convex Polytopes, second edition, Springer, 2003, Chapter 2, §2.3, Theorem 5, printed page 15; supplied source.pdf, page 33.

A convex set contains the segment joining any two of its points. For a bounded closed convex set in finite-dimensional real space, extreme points describe the set through convex combinations. An extreme point cannot lie strictly between two distinct points of the set. Allowing unbounded sets introduces a second ingredient: directions in which one can move indefinitely while remaining in the set.

This mission concerns that second ingredient and its interaction with extreme points. A closed convex set is line-free if it contains no entire straight line. It may nevertheless contain rays and be unbounded. Its characteristic cone consists of directions v for which x + t v stays in the set whenever x belongs to the set and t is nonnegative. For a nonempty closed convex set, checking one basepoint gives the same cone as checking every basepoint. Thus the cone records the directions of recession without singling out an origin inside the set.

The goal is Grünbaum’s Theorem 2.5.6:

$$K = \operatorname{cc} K + \operatorname{conv}(\operatorname{ext} K)$$

for every line-free, closed convex set K in real d-dimensional space. The plus sign denotes Minkowski addition: all sums of one point from each set. The equation says that every point of K is a recession vector plus a finite convex combination of extreme points. Conversely, each such sum belongs to K. There is no topological closure around the convex hull in this equation.

A ray illustrates the two ingredients. Its endpoint is its only extreme point, while its characteristic cone supplies every nonnegative displacement along the ray. A singleton has only itself as an extreme point and has zero characteristic cone. A whole straight line shows why the line-free hypothesis matters: it has no extreme points and cannot be recovered from their convex hull by this formula.

The ambient dimension is arbitrary and finite; the set need not be full-dimensional or polyhedral. The characteristic cone is defined using all basepoints, so its value on the empty set is the whole ambient space. Since the empty set has no extreme points, its convex hull and the displayed Minkowski sum are empty, and the equation remains valid. This convention extends the formula without asserting that the book defines a characteristic cone at an absent basepoint.

The source is Branko Grünbaum, Convex Polytopes, second edition (2003), §2.5, Theorem 6, printed page 25 (PDF page 43). The characteristic cone and line-free condition appear on printed page 24 (PDF page 42); extreme points are defined in §2.4 on printed page 17 (PDF page 35). These definitions supply the vocabulary for the single representation goal.

Why tree diagrams

Thompson's group $F$ is a finitely presented group of piecewise-linear homeomorphisms of the unit interval that has served since the 1960s as a standard supply of counterexamples in combinatorial group theory: its commutator subgroup is simple, every proper quotient of it is abelian, it contains no free subgroup of rank two, it is not elementary amenable, and whether it is amenable is a question Cannon, Floyd and Parry report as having been raised by Geoghegan in 1979 and still open when they wrote (CFP96, §4 and p. 227).

Almost nothing about $F$ is computed directly from that analytic definition. What makes the group tractable is a combinatorial calculus: each element is encoded by a pair of finite binary trees, and multiplication becomes a cancellation between trees. Cannon, Floyd and Parry credit the device to Brown and devote §2 of their notes to it; everything later in those notes that requires a computation — the two presentations of §3, the normal subgroup lattice of §4, the treatment of Thompson's group $T$ in §5 — runs through it.

This mission formalizes that calculus and the normal form it yields.

Setting

A real number is dyadic when it has the form $m/2^k$ with $m$ an integer and $k$ a nonnegative integer. Thompson's group $F$ consists of the increasing homeomorphisms of $[0,1]$ that are piecewise linear with finitely many breakpoints, all breakpoints dyadic and every slope an integer power of $2$, under composition. Two of its elements are

$$A(x) = \begin{cases} x/2 & 0 \le x \le \tfrac12\\ x - \tfrac14 & \tfrac12 \le x \le \tfrac34\\ 2x-1 & \tfrac34 \le x \le 1\end{cases} \qquad B(x) = \begin{cases} x & 0 \le x \le \tfrac12\\ x/2 + \tfrac14 & \tfrac12 \le x \le \tfrac34\\ x - \tfrac18 & \tfrac34 \le x \le \tfrac78\\ 2x-1 & \tfrac78 \le x \le 1,\end{cases}$$

and from them come $X_0 = A$ and $X_n = A^{-(n-1)} B A^{n-1}$ for $n \ge 1$, so that $X_1 = B$.

A standard dyadic interval is one of the form $[a/2^n, (a+1)/2^n]$ with $a$ and $n$ nonnegative integers and $a+1 \le 2^n$. A partition $0 = x_0 < \cdots < x_m = 1$ of $[0,1]$ is a standard dyadic partition when every $[x_{i-1}, x_i]$ is a standard dyadic interval.

An ordered rooted binary tree is a finite tree in which each vertex has either no children or an ordered left child and right child. Its childless vertices are its leaves, which carry a canonical left-to-right order; its right side is the path from the root always taking the right child; a caret is a vertex with its two children. Assigning $[0,1]$ to the root and splitting each interval at its midpoint between the two children gives every vertex a standard dyadic interval, and the leaves then cut out a standard dyadic partition — the sense in which such a tree is a $\mathcal{T}$-tree. The exponents of a $\mathcal{T}$-tree are one nonnegative integer per leaf, in order: the $k$th is the length of the longest arc of left edges beginning at the $k$th leaf that does not reach the right side.

A tree diagram is an ordered pair $(R,S)$ of $\mathcal{T}$-trees with equally many leaves. An element $f$ of $F$ has that diagram when $f$ is affine on each interval cut out by the leaves of $R$ and carries those intervals, in order, onto the intervals cut out by the leaves of $S$. Adjoining a caret to $R$ and to $S$ at the same leaf gives another diagram for the same $f$; a diagram admitting no such reduction — no position where both trees carry a caret — is reduced.

Formalization targets

Goal: the unique normal form

Every $f \ne 1$ in $F$ is

$$f \;=\; X_0^{b_0} X_1^{b_1} \cdots X_n^{b_n} \, X_n^{-a_n} \cdots X_1^{-a_1} X_0^{-a_0}$$

for exactly one choice of nonnegative integers $n$, $a_0, \dots, a_n$, $b_0, \dots, b_n$ subject to two conditions: exactly one of $a_n$ and $b_n$ is nonzero, and if $a_k > 0$ and $b_k > 0$ for some $k < n$ then $a_{k+1} > 0$ or $b_{k+1} > 0$.

It fixes no bound on $n$ and no normalization beyond those two conditions, so no later refinement of how the exponents are presented can invalidate it.

Along the way

The milestone list follows §2 in order: the correspondence between standard dyadic partitions and $\mathcal{T}$-trees, the bijection between $F$ and the reduced tree diagrams, the word read off the exponents of $(R,S)$, a criterion for a diagram to be reduced, generation by $A$ and $B$, and closure under multiplication of the positive elements — those of the form $X_0^{b_0} \cdots X_n^{b_n}$ with every exponent nonnegative.

What it gives

A normal form is a decision procedure: two words in the generators name the same element exactly when their normal forms agree, so the word problem for $F$ is solved by computing them. The generation statement is what licenses treating $F$ as a two-generator group, and it is the input to both presentations in §3. The positive elements and their closure under multiplication are used, with the normal form, throughout §5 on Thompson's group $T$.

The §2 results this mission targets — Lemma 2.2, the correspondence between $F$ and the reduced tree diagrams, Theorem 2.5, Corollary 2.6, Corollary-Definition 2.7 and Lemma 2.8 — are proved mathematics: Cannon, Floyd and Parry are expounding material that goes back to Thompson's unpublished notes. None of them has a machine-checked proof on this platform, and the library contains no tree-diagram machinery to build on, so the definitions published here fix the interface for anyone later formalizing Thompson's groups $T$ and $V$, which occupy the same notes and are built from the same trees.

There is also a concrete dependency. The companion mission on §4 of the same paper has eleven of its fifteen milestones machine-checked, and all four that remain wait on this section: Cannon, Floyd and Parry prove their Theorem 4.1 through Corollary 2.6 and their Theorem 4.3 through the normal form. Corollary 2.6 appears in this milestone list as the same theorem object that is open there, so closing it here closes it there.

Difficulty

The obvious way to attach a diagram to an element $f$ is to use the partition given by its breakpoints. That fails twice over: the breakpoints of $f$ need not be the division points of any $\mathcal{T}$-tree, and even when they are, their images under $f$ need not be either, since the definition of $F$ constrains the breakpoints and slopes of $f$ and says nothing about where the image partition sits. Both failures must be repaired by refining the partition before any tree appears, which is why that refinement is a milestone rather than a preliminary.

Uniqueness of the reduced diagram is a difficulty of a different kind: two reduced diagrams for the same element admit no a priori map between their trees, so they cannot be compared directly.

A third is not visible in the source. For trees with $n+1$ leaves the exponent lists always end in $0$, so the outermost factors of the word above vanish; but the normal form demands that exactly one of $a_n$, $b_n$ be nonzero. The two indexings differ, and a re-indexing step sits between the theorem producing the word and the corollary stating the normal form. The paper prints them one under the other. That step is a milestone of its own, flagged as absent from the source, so a solver working from the paper alone is not ambushed by it.

Formalization scope

Ordered rooted binary trees are an inductive type — a leaf, or a pair of subtrees — rather than graphs with a root and valence conditions. Those conditions say exactly that every non-leaf vertex has two distinguished children, so both descriptions pick out the same objects, but the inductive type is a reformulation of the paper's definition and the definition bundle says so. The infinite tree of all standard dyadic intervals is likewise never built: the subdivision of $[0,1]$ comes from a recursion halving at each node, which turns the paper's observation that the leaves of a $\mathcal{T}$-tree are the intervals of a standard dyadic partition from something given into something proved.

$F$ is imported rather than redefined, from the published definition bundle of the companion mission, where it is the subgroup generated by the piecewise-linear maps described above; membership in that subgroup is identified with the piecewise-linear description by a theorem already machine-checked there. Exponent data is carried by finite lists, and the uniqueness in the goal is uniqueness of that list data.

The goal is vacuous in neither direction: its hypothesis is met by $A$ and $B$ themselves, and a separate milestone asserts that every choice of exponent data meeting the two conditions names an element other than the identity.

The tree combinatorics — leaf counts, right sides, the subdivision map, the exponents, carets — is published here as a separate definition node that mentions $F$ nowhere and needs nothing but Mathlib, so it is reusable as it stands; the diagram vocabulary is built on it. Any milestone is open to contribution, as are routes other than the paper's.

Selected references

• J. W. Cannon, W. J. Floyd, W. R. Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Mathématique (2) 42 (1996), 215–256. doi:10.5169/seals-87877 — §2, pages 218–224, is the source for this mission; §1, page 217, defines $A$, $B$ and the $X_n$.

Within that paper tree diagrams are credited to Brown and the word-length algorithm to Fordham, cited there as [Bro1] and [Fo].

Motivation

Let $G=(V,E)$ be a finite connected graph. In Bernoulli bond percolation each edge is independently retained with probability $P$ and deleted otherwise, and one writes $\mathbb{P}_P[u \leftrightarrow v]$ for the probability that vertices $u$ and $v$ lie in the same component of the resulting random subgraph. Comparing such connection probabilities is a basic and genuinely hard problem: computing them exactly is $\#\mathsf{P}$-hard.

The bunkbed graph is built from two copies of $G$, joined by vertical edges called posts above a chosen set $T \subseteq V$ of transversal vertices. Percolation is performed on the two copies while every post is retained. Writing $v$ for a vertex in the lower copy and $v'$ for its counterpart upstairs, Kasteleyn conjectured in 1985 that being connected within a level is always at least as likely as crossing between levels.

The conjecture is intuitively compelling — crossing levels appears to require "using up" a post — and it resisted proof for forty years. A short timeline:

• 1985 — Kasteleyn formulates the conjecture; it is recorded as Remark 5 of van den Berg–Kahn (2001), which is how the source cites it.
• Positive results accumulate for special cases: wheels, complete graphs, complete bipartite graphs, graphs symmetric with respect to an automorphism exchanging $u$ and $v$, one or two transversal vertices, and in the $P \uparrow 1$ limit.
• 2024 — Hollom refutes the $3$-uniform hypergraph analogue. This alone does not settle the graph case: it is impossible to simulate a single $3$-hyperedge by bond percolation on a gadget graph.
• 2025 — Gladkov, Pak and Zimin disprove the conjecture outright, with an explicit counterexample and without computer assistance.

Section 7 of the source is a candid account of a large-scale machine-learning-guided search that failed to find a counterexample, and of why the problem is unusually ill-suited to experimental testing.

Setting

Fix a finite graph with vertex set $V$ and edge set $E$, and a retention function $w : E \to [0,1]$ (the uniform case is $w \equiv P$). A configuration is a subset $S \subseteq E$ of open edges, occurring with probability

$$\mathbb{P}(S) \;=\; \prod_{e \in S} w(e) \prod_{e \in E \setminus S} \bigl(1 - w(e)\bigr),$$

and $\mathbb{P}[u \leftrightarrow v]$ is the total probability of those $S$ for which $u$ and $v$ are connected in $(V, S)$.

Given $T \subseteq V$, the bunkbed graph has vertex set $V \times \{0,1\}$. Its edges are a copy of $E$ in each level together with a post $\{(t,0),(t,1)\}$ for every $t \in T$. In bunkbed percolation the two level-copies are percolated independently while all posts are retained; $\mathbb{P}^{\mathrm{bb}}$ denotes the resulting connection probabilities.

Formalization targets

Goal — the bunkbed conjecture is false

$$\neg\;\Bigl(\forall\,G \text{ connected},\ \forall\,T \subseteq V,\ \forall\,0<P<1,\ \forall\,u,v \in V:\quad \mathbb{P}^{\mathrm{bb}}_P[u \leftrightarrow v] \;\ge\; \mathbb{P}^{\mathrm{bb}}_P[u \leftrightarrow v'] \Bigr)$$

Supporting target — the explicit counterexample (Theorem 1.2)

$$\exists\, G,\ |V| = 7{,}222,\ |E| = 14{,}442,\ |T| = 3,\ \exists\, u,v:\qquad \mathbb{P}^{\mathrm{bb}}_{1/2}[u \leftrightarrow v] \;<\; \mathbb{P}^{\mathrm{bb}}_{1/2}[u \leftrightarrow v']$$

Supporting target — hyperedge simulation (Lemma 4.1)

For the gadget $G_n$ on $n+1$ vertices,

$$P_{abc}\,P_{a|b|c} \;-\; P_{ab|c}\,P_{ac|b} \;>\; \Bigl(n\tfrac{1-P}{1+P} - 1\Bigr) P_{a|bc}.$$

Significance

The result itself. A forty-year-old conjecture in percolation theory is false, and prior positive results are thereby sharpened rather than superseded: it becomes interesting to delimit exactly which families of graphs do satisfy the inequality. The refutation also settles the Counting, Weighted, Alternative and Computational variants listed in §8.1, and shows the random-cluster analogue cannot be pushed from $q=2$ down to $q=1$.

Formalizing it. Nothing here is open; the mission produces machine-checked versions of published results, and as a by-product the first percolation theory in Lean. Mathlib currently contains no percolation of any kind — no connection probabilities, no bunkbed graph, no hypergraph percolation. That infrastructure is reusable far beyond this mission. The source itself notes (§8.2) that its central combinatorial lemma was independently verified by computer; a formal proof would replace that check with a certificate.

Difficulty

The obvious approach — exhibit a small graph and compute both probabilities — is hopeless, and the source explains why at length. A graph with $m$ edges has $2^m$ configurations; for the counterexample here the probability gap is on the order of $10^{-4331}$, so no sampling argument can detect it, and exact enumeration is out of reach. Section 7 records a substantial computational search that found nothing and, in hindsight, could not have.

The proof is instead structural, and its difficulty is concentrated in one place. Hollom's refutation of the hypergraph version cannot be transferred directly, because a single $3$-hyperedge cannot be simulated by bond percolation on any gadget graph. The source's answer is to prove a robust version of Hollom's lemma (Lemma 3.3) which survives the inexact simulation that gadget graphs do provide, and this robustness is what Lemma 4.1's inequality quantifies. Lemma 3.3 is proved by constructing a weight-preserving involution on a refined configuration space — the technical heart, and the milestone a solver should expect to spend the most effort on.

Formalization scope

The development commits to the following conventions.

• Everything is finite and rational-valued, hence computable: connection probabilities are ℚ and evaluate by #eval, and small instances close by decide.
• A graph is given by an explicit edge Finset and realised through SimpleGraph.fromEdgeSet; connectivity is Mathlib's SimpleGraph.Reachable.
• Percolation is a sum over the powerset of the edge set, weighted as displayed above, of a reachability indicator. Edge weights are per-edge (Sym2 V → ℚ), since the gadget $G_n$ genuinely needs two different weights: its spokes are retained with probability $1-P$ and its path edges with probability $P$.
• In the bunkbed, level 0 is the lower copy; posts over T are unconditionally present and are not percolated. The two levels are percolated independently.
• ⚠️ Planarity is omitted from the goal. Theorem 1.2 asserts the counterexample is planar, and Mathlib has no notion of a planar graph — no IsPlanar, no Euler formula, no Kuratowski. Building one is a larger project than this mission. The formalized statement of Theorem 1.2 is therefore strictly weaker than the published one, and the goal is instead the negation of the conjecture, which is exactly the source's own "In particular, the BBC is false." Contributions adding planarity are welcome and would strengthen the milestone.
• Ruling out a trivializing reading: the conjecture must be negated as stated, over all connected graphs, transversal sets and $0<P<1$. Weakening it to a fixed graph, or to $P \in \{0,1\}$, or dropping connectivity, would make the refutation vacuous.

Infrastructure. Mathlib supplies SimpleGraph, boxProd, Reachable with a DecidableRel instance, fromEdgeSet, edgeFinset and Finset.powerset. It supplies no percolation, so this mission ships two definition files: Bernoulli bond percolation with the bunkbed construction and the five triple-partition probabilities, and hypergraph percolation with Hollom's hypergraph and the Wierman–Ziff five-state model. One known gap: Mathlib's Reachable decision procedure enumerates walks and is far too slow to evaluate the $64$-configuration check of Lemma 3.1 by decide. A solver will want a linear-time reachability procedure together with a proof that it agrees with Reachable; that is itself a worthwhile reusable contribution.

Selected references

• J. van den Berg and J. Kahn, A correlation inequality for connection events in percolation, Ann. Probab. 29 (2001), 123–126 — Kasteleyn's conjecture appears as Remark 5.
• T. Hollom, A new proof of the bunkbed conjecture in the $p \uparrow 1$ limit, Discrete Math. 347 (2024), 113711.
• T. Hollom, The bunkbed conjecture is not robust to generalisation, arXiv:2406.01790 (2024).
• T. Hutchcroft, P. Nizić-Nikolac, A. Kent, The bunkbed conjecture holds in the $p \uparrow 1$ limit, Comb. Probab. Comput. 32 (2023), 363–369.
• N. Gladkov, I. Pak, A. Zimin, The bunkbed conjecture is false, Proc. Natl. Acad. Sci. USA 122 (2025), no. 24, e2420725122. doi:10.1073/pnas.2420725122; preprint arXiv:2410.02545.
• J. C. Wierman and R. M. Ziff, Self-dual planar hypergraphs and exact bond percolation thresholds, Electron. J. Combin. 18 (2011).
• G. R. Grimmett, Percolation, 2nd ed., Springer, 1999.

Motivation

Error-correcting codes protect information against corruption by adding controlled redundancy. For a code, the distribution of Hamming weights records how its words are spread across possible distances from the zero word and determines basic quantities such as its minimum distance. Linear codes also carry an algebraic duality: every linear code $C$ over a finite field has a dual code $C^\perp$ consisting of the words orthogonal to all words of $C$ under the standard coordinatewise bilinear form.

The MacWilliams identity states that the full Hamming-weight distribution of $C^\perp$ is determined by that of $C$ through one linear change of variables. It is the principal result of Chapter 5 of F. J. MacWilliams and N. J. A. Sloane's The Theory of Error-Correcting Codes. The binary identity appears there as Theorem 1, while the arbitrary-finite-field Hamming-weight-enumerator identity formalized here is Theorem 13 on p. 146. The surrounding chapter develops related transformations for complete, Lee, exact, joint, and split weight enumerators, nonlinear-code distance distributions, orthogonal arrays, and Krawtchouk polynomials.

This development isolates the arbitrary-$q$ Hamming identity as a first reusable result. Its declarations are designed to support later formalizations drawn from the same chapter and, more broadly, from the book, without enlarging the present target beyond the MacWilliams identity.

Setting

Let $F$ be a finite field of cardinality $q$, let $\iota$ be a finite coordinate type, and let a word be a function $c:\iota\to F$. A linear code $C$ is an $F$-linear subspace of the word space. The standard bilinear form is

$$\langle c,v\rangle=\sum_{i\in\iota}c_i v_i,$$

and the dual code is

$$C^\perp=\{v:\iota\to F:\langle c,v\rangle=0\text{ for every }c\in C\}.$$

The Hamming weight $\operatorname{wt}(c)$ is the number of coordinates at which $c$ is nonzero. Writing $n=|\iota|$, the homogeneous Hamming weight enumerator of $C$ is the integer-coefficient polynomial

$$W_C(X,Y)=\sum_{c\in C}X^{n-\operatorname{wt}(c)}Y^{\operatorname{wt}(c)}.$$

Thus the coefficient of $X^{n-j}Y^j$ is the number of codewords of weight $j$. The Lean development represents this object symbolically in MvPolynomial (Fin 2) ℤ; its complex-valued form is obtained by evaluation, so the symbolic and evaluated presentations share a single definition.

Formalization targets

Character orthogonality over a code

For a primitive complex additive character $\psi$ of $F$, define

$$S_C(v)=\sum_{c\in C}\psi(\langle c,v\rangle).$$

The first milestone states that $S_C(v)=|C|$ when $v\in C^\perp$ and $S_C(v)=0$ otherwise. The binary statement occurs as Problem 13 on p. 134 of MacWilliams--Sloane; Lemmas 9 and 11 on pp. 143--145 give the finite-field character and Fourier formulation.

Coordinatewise Hamming transform

For every word $c$ and all $X,Y\in\mathbb C$, the second milestone records the full character-weighted transform of the Hamming monomial:

$$\sum_{v\in F^\iota} X^{n-\operatorname{wt}(v)}Y^{\operatorname{wt}(v)} \psi(\langle c,v\rangle) = \bigl(X+(q-1)Y\bigr)^{n-\operatorname{wt}(c)} (X-Y)^{\operatorname{wt}(c)}.$$

This is a separately reusable formulation of the coordinate calculation appearing in the proofs of Theorems 10 and 13 on pp. 144--146.

MacWilliams identity

The capstone is the following equality of integer polynomials:

$$|C|\,W_{C^\perp}(X,Y) = W_C\bigl(X+(q-1)Y,\,X-Y\bigr).$$

This is the denominator-free form of Chapter 5, Theorem 13. After evaluation over a characteristic-zero field it is equivalent to the normalized textbook formula

$$W_{C^\perp}(X,Y) = \frac{1}{|C|}W_C\bigl(X+(q-1)Y,\,X-Y\bigr).$$

Significance

The identity turns duality into an enumerative operation: knowing the weight enumerator of a linear code determines the weight enumerator of its dual. It supplies immediate consistency restrictions on possible weight distributions and is a basic input to the study of self-dual codes, Krawtchouk transforms, association schemes, invariant-theoretic properties of enumerators, and linear-programming bounds.

The formalization contributes a small common interface for finite-field words, linear codes, standard duals, and homogeneous Hamming weight enumerators. These declarations are absent from the selected Mathlib environment even though Mathlib already provides Hamming weight, finite-field algebra, additive characters, finite sums, bilinear-form orthogonals, and multivariate polynomials. Establishing the interface and its first central theorem makes those general libraries directly usable for subsequent coding-theory developments.

Difficulty

The paper statement is short, but its formal representations live in several different layers. Codes are submodules whose elements are subtypes; Hamming weight is a natural-number count; duality is expressed through a bilinear form; character identities take values in $\mathbb C$; and the final result is most reusable as an equality of symbolic polynomials over $\mathbb Z$. The central formalization burden is maintaining exact agreement while transporting the same enumerative data among these layers, including finite instances for codeword subtypes and the natural-number exponents of the homogeneous monomials.

The theorem must also retain the genuine finite-field statement. Replacing the code by an arbitrary finite set, hard-coding the binary field, defining the dual by its expected cardinality, or proving only equality at one chosen pair of evaluation points would not establish the target.

Formalization scope

The coordinate type is an arbitrary finite type rather than only Fin n; its cardinality plays the role of the code length. A word is CodingTheory.Word F ι := ι → F, and a linear code is a submodule of this common word space. This representation provides the linear structure and canonical orthogonal dual required here while leaving room for a future nonlinear-code type built from finite sets of the same words.

The polynomial CodingTheory.hammingWeightEnumeratorPolynomial has coefficients in $\mathbb Z$ and variables indexed by Fin 2. Variable $0$ records zero coordinates and variable $1$ records nonzero coordinates. Its name explicitly identifies the Hamming enumerator, leaving separate stable names available for future complete, Lee, exact, joint, and split weight enumerators. Those later enumerators should be added as new declarations and connected to this one by specialization theorems rather than replacing it.

The standard dual is bilinear, not Hermitian. The code alphabet may be any finite field. The zero code, full code, and empty coordinate type are included; in the empty-coordinate case there is one word of weight zero and the identity reduces to $1=1$. The present mission does not formalize nonlinear codes, complete or other generalized enumerators, orthogonal arrays, or Krawtchouk-polynomial theory. It establishes only the definitions and two character-sum milestones required for the Hamming MacWilliams identity, with a namespace and module boundary intended for reuse by later missions in the textbook series.

Selected references

• F. J. MacWilliams and N. J. A. Sloane, The Theory of Error-Correcting Codes, North-Holland, 1977, Chapter 5, pp. 125--154; especially Problem 13 (p. 134), Lemmas 9 and 11 (pp. 143--145), and Theorem 13 (p. 146). Publisher chapter record.
• Violetta Weger, Coding Theory, Technical University of Munich lecture notes, 2025, Theorem 11.2 and Lemma 11.8, pp. 154--159.
• F. J. MacWilliams, “A Theorem on the Distribution of Weights in a Systematic Code”, Bell System Technical Journal 42 (1963), 79--94.

Motivation

Counting the trees on a fixed, labeled vertex set is one of the oldest enumeration problems in graph theory. Cayley stated the count in 1889 while enumerating isomers of saturated hydrocarbons — each tree corresponds to a possible carbon skeleton — and the same number reappears throughout combinatorics as the number of spanning trees of the complete graph $K_n$, a special case of Kirchhoff's Matrix–Tree Theorem, and as the base case against which more refined tree-counting results (trees with a prescribed degree sequence, forests, spanning trees of general graphs) are measured.

Several independent proofs of the count are known — a direct recursive argument, a determinant computation via the Matrix–Tree Theorem, a double-counting argument on increasing trees — and each exposes a different piece of structure. This mission formalizes the proof via Prüfer sequences, due to Prüfer (1918): an explicit, computable bijection between labeled trees and certain finite sequences, presented here following Gross and Yellen, Graph Theory and Its Applications, 3rd ed. (CRC Press, 2018), Section 3.7, pp. 157–162.

Setting

Fix $n \geq 2$ and take the vertex set to be $\{1, \dots, n\}$ (formalized as Fin n). A labeled tree on $n$ vertices is a simple graph $T$ on this vertex set that is connected and acyclic (Mathlib's SimpleGraph.IsTree). Two labeled trees are the same exactly when their edge sets coincide — the two 4-vertex trees in Figure 3.7.1 of the source are both paths but are different labeled trees, since the labels sit on different vertices.

A Prüfer sequence of length $n - 2$ is any sequence $(s_1, \dots, s_{n-2})$ of labels drawn from $\{1, \dots, n\}$, repetitions allowed (so there are $n^{n-2}$ of them, by the rule of product).

The encoding of a tree $T$ (Algorithm 3.7.1, p. 157) builds its Prüfer sequence by repeating, $n-2$ times: find the leaf (degree-one vertex) with the smallest label among those not yet removed, record the label of its neighbor, then delete that leaf. The decoding of a sequence (Algorithm 3.7.3, p. 159) reverses this: it rebuilds the tree edge by edge, at each step joining the smallest label not yet used and not appearing later in the sequence to the next label in the sequence, finishing by joining the two labels left over.

Formalization targets

Goal — Cayley's Tree Formula (Theorem 3.7.5, p. 162)

$$\operatorname{Nat.card}\, \{T : \text{SimpleGraph}(\text{Fin } n) \mid T.\text{IsTree}\} = n^{\,n-2}, \qquad n \geq 2.$$

This is the weakest stable statement: it is exactly the count Cayley identified, phrased without reference to any particular proof method, so it is not tied to properties of Prüfer sequences beyond what is needed to establish the count.

Significance

The identity itself is foundational: it is the base case of Kirchhoff's Matrix–Tree Theorem (which computes the analogous count for spanning trees of an arbitrary graph as a cofactor of its Laplacian) and it appears as an ingredient in random graph theory (counting spanning trees of $K_n$ bounds the number of ways a random graph process can build a tree) and in the analysis of algorithms on trees, where the Prüfer encoding itself is used as a compact serialization of a labeled tree.

The result has been proved by hand for over a century, and its most classical proof (the one formalized here) has not, to this project's knowledge, appeared as a machine-checked Lean proof; Mathlib's Combinatorics.SimpleGraph library has the tree and acyclicity infrastructure this mission builds on, but not the Prüfer bijection or the count itself. Formalizing it here means constructing the encoding and decoding maps explicitly as computable, total recursive functions, and proving they are mutually inverse — the mission's four milestones below are exactly the four supporting results the source uses for this.

Difficulty

The obvious first attempt is to define the encoding by structural recursion, peeling one leaf per step, but this immediately runs into a dependent-typing obstacle: after deleting a vertex, the "remaining graph" naturally lives on a smaller vertex type, so a naive recursive definition changes type at every step and the final sequence's type (length $n-2$) is not visible to the recursion by construction. The formalization here sidesteps this by keeping the ambient vertex type fixed at Fin n throughout and tracking the shrinking set of "active" vertices as an ordinary Finset (Fin n) parameter, so the recursion is on a natural number step-counter rather than on the type itself; the price is that every step's "leaf" and "neighbor" must be picked out by an explicit Finset.filter/Finset.min computation whose well-definedness (there is always a smallest active leaf, and it always has a unique active neighbor) is exactly the content of Propositions 3.7.1 and 3.7.3 below, rather than something the type system gives for free. The inverse direction has the dual issue in reverse: decoding recurses structurally on the sequence while tracking a shrinking label set, and showing the two recursions undo each other (Proposition 3.7.4) requires the same induction run in both directions simultaneously.

Formalization scope

Trees are SimpleGraph (Fin n) satisfying Mathlib's SimpleGraph.IsTree; no alternate, weaker notion of "tree" is used. Prüfer sequences are functions Fin (n - 2) → Fin n (equivalently, by Fintype.card_fun, exactly the $n^{n-2}$ count needed) rather than List or Vector, so that the final counting step is immediate once the bijection is established. The encoding and decoding functions (pruferEncode, pruferDecode) are supplied as noncomputable definitions in Definitions.Def_GYGraphTheory — noncomputable only because Prop-level decidability of a general SimpleGraph.Adj is classical, not because the algorithm is non-constructive; every step is the literal Prüfer procedure, junk-valued (defaulting to label 0) outside its intended domain in exactly the way a hand proof would say "this step is meaningless once fewer than two active vertices remain." The four milestones give the precise faithful statements of the source's Propositions 3.7.1, Corollary 3.7.2, Proposition 3.7.3, and Proposition 3.7.4; the goal theorem is the immediate corollary once all four are in hand, via Fintype.card_congr and Fintype.card_fun. A trivializing formalization is not available here: IsTree is Mathlib's standard, non-vacuous notion, and the milestones pin down pruferEncode and pruferDecode to the source's specific algorithm rather than leaving the bijection's existence as a free black box. Beyond the four milestones, a full development needs: basic Finset/List manipulation lemmas relating pruferPeel's step-indexed recursion to pruferDecodeAux's list-indexed recursion (reusable in any future mission touching Prüfer-style encodings); and the final cardinality argument tying the bijection to n ^ (n - 2). Contributions connecting this formula to Mathlib's general Matrix–Tree machinery (if and when it exists) would be a natural, welcome extension but are out of scope for this mission.

Selected references

• A. Cayley, A theorem on trees, Quart. J. Math. 23 (1889), 376–378.
• H. Prüfer, Neuer Beweis eines Satzes über Permutationen, Archiv der Mathematischen Physik 27 (1918), 742–744.
• J.L. Gross and J. Yellen, Graph Theory and Its Applications, 3rd ed., CRC Press, 2018, Section 3.7 "Counting Labeled Trees: Prüfer Encoding", pp. 157–162.

Assigning distinct resources under compatibility constraints

A finite allocation problem begins with a list of permitted choices. Each recipient may use some resources but not others, and a resource may be assigned at most once. Knowing that every recipient has an available resource is insufficient: several recipients may all depend on the same small pool. A useful theorem must decide whether the compatibility pattern permits all requirements to be met simultaneously.

This mission develops the matching results in the chapter on systems of distinct representatives in D. Yogeshwaran's Discrete Mathematics—Lecture Notes, §6.1. Its endpoint allows different recipients to require different numbers of resources. The classical one-resource problem, the regular-graph case, and the case in which a bounded number of assignments may remain unfilled are retained as separate source-numbered results. The project concerns established theorems, not a new conjecture about the existence of matchings.

Graphs, matchings, and demands

A finite simple graph consists of a finite set of vertices and unordered pairs of distinct vertices called edges. A bipartition is a pair of disjoint sets $L,R$ whose union is the vertex set, such that every edge joins a vertex in $L$ to a vertex in $R$. The left vertices represent recipients and the right vertices represent resources. An edge records that the resource is permitted for that recipient. These graph conventions follow Definition 1.1 of the notes.

For a vertex $x$, the neighbor set $N_G(x)$ contains the vertices joined to $x$. For a set $S$ of vertices, write $N_G(S)=\bigcup_{x\in S}N_G(x)$. A matching is an edge set in which no vertex is used twice. It is complete on $L$ if every left vertex is used, and perfect if every vertex is used. A subgraph may retain selected edges of the original graph. Its degree $\deg_H(x)$ counts the retained neighbors of $x$.

A demand is a natural number $d_x$ attached to each $x\in L$. Unlike a complete ordinary matching, the capstone may assign more than one resource to a recipient. Resources still have capacity one, and a demand may be zero.

Formalization targets

The ordinary matching criterion is Theorem 6.2:

$$\exists\text{ a complete matching on }L \quad\Longleftrightarrow\quad \forall S\subseteq L,\quad |S|\le |N_G(S)|.$$

The development also includes Exercise 6.3, asserting that a $k$-regular bipartite graph has a perfect matching when $k>0$. Proposition 6.4 states the quantitative deficit version:

$$\bigl(\forall S\subseteq L,\ |S|-d\le |N_G(S)|\bigr) \quad\Longrightarrow\quad \exists M\text{ matching},\quad |L|-d\le |E(M)|, \qquad d\ge1.$$

The capstone is the prescribed-degree equivalence of Exercise 6.5:

$$\begin{split} &\exists H\subseteq G: \bigl(\forall x\in L,\ \deg_H(x)=d_x\bigr) \land \bigl(\forall y\in R,\ \deg_H(y)\le1\bigr)\\ &\qquad\Longleftrightarrow\quad \forall S\subseteq L,\quad \sum_{x\in S}d_x\le |N_G(S)|. \end{split}$$

This statement retains the entire demand function and does not fix a uniform demand, restrict demands to positive values, or replace integral selections by real weights.

The set-theoretic interface is Corollary 6.9. A finite family of arbitrary sets $(A_i)_{i\in I}$ has a system of distinct representatives, meaning an injective choice $f(i)\in A_i$, exactly when

$$\forall J\subseteq I,\qquad |J|\le \left|\bigcup_{i\in J}A_i\right|.$$

Only the index family is finite; the sets themselves may be infinite.

What the development provides

The demand criterion characterizes feasibility entirely in terms of the original compatibility graph and the requested multiplicities. Its necessity identifies an obstruction to any assignment, while its sufficiency asserts that no other obstruction exists. The deficit theorem gives a quantitative statement when complete coverage is unavailable. The regular case gives a distinct consequence for graphs described through their degrees, rather than through a separately supplied collection of neighborhood inequalities. These are the respective contents of Exercises 6.3 and 6.5 and Proposition 6.4.

Mathlib already provides finite-family and graph versions of Hall's theorem in its Hall development and graph interface. The source-aligned development therefore reuses established infrastructure. Its additional work consists of connecting exact graph degrees and edge counts to the source statements, retaining the deficit and zero-demand cases, and supplying an arbitrary-set representatives interface. Local proofs of the five theorem statements have been checked in Lean 4.29.0-rc3 with Mathlib 777aaa6.

Where exact formalization is delicate

Independent local choices do not guarantee a matching: different choices can collide at one resource. Replacing distinct selections by nonnegative real allocations would change the conclusion. Counting total demand alone also misses obstructions carried by proper subsets of recipients.

Several representation issues matter even after the mathematics is known. A left-saturating matching need not be perfect. A subgraph's vertex set may omit isolated ambient vertices. Cardinality conventions for infinite sets can turn a superficially plausible formula into a different assertion. Finally, a theorem that assumes all neighborhood inequalities has not established those inequalities merely because a graph is regular. The individual interfaces must distinguish these obligations rather than hide them inside a definition.

Formalization scope

The graph results use finite vertex types and native SimpleGraph and Subgraph objects. Both disjointness and coverage of the bipartition are explicit. Local-finiteness instances supply finite neighbor enumerations; they impose no further restriction on finite graphs. The complete-matching predicate combines the native matching condition with inclusion of the prescribed vertex set.

Degrees in the capstone are cardinalities of finite subgraph neighbor sets. The deficit conclusion counts unordered subgraph edges. Natural subtraction is truncated at zero, an equivalent convention for these nonnegative cardinality lower bounds. Empty graphs, empty index families, and zero demands remain admissible. In the representatives theorem, arbitrary sets are measured by extended cardinality; infinity is never replaced by zero.

The reusable outputs are the source-aligned graph statements, the complete-matching interface, the prescribed-degree equivalence, and the arbitrary-set representatives criterion. Equivalent proofs and clearer reusable interfaces are within scope. Placeholder conclusions, extra assumptions that exclude the difficult cases, and fractional substitutes for the integral capstone are not.

Selected references

• D. Yogeshwaran, Discrete Mathematics—Lecture Notes, Indian Statistical Institute Bangalore, HTML edition generated 2025. Chapter 6.1; graph conventions.
• The mathlib community, Mathlib 4, revision 777aaa6, 2026. Finite-family Hall theorem; native graph Hall theorem.