Motivation

A sorting network is a sorting procedure whose sequence of comparisons is fixed in advance, independently of the data. Its depth, the number of rounds of simultaneous comparisons on disjoint pairs, is the parallel running time. Sorting networks are used in parallel and hardware sorting, in switching networks, and in cryptography, where a data-independent (oblivious) sequence of operations is required. How small the depth can be as a function of the number of inputs $n$ is a basic question of parallel computation.

Timeline:

• 1968. Batcher's odd-even merge sort and bitonic sort give networks of depth $O((\log n)^2)$ and size $O(n(\log n)^2)$ (K. E. Batcher, Sorting networks and their applications, AFIPS Spring Joint Computer Conference, 1968). For $n$ a power of two they remain the best explicit networks in practice.
• 1973. Knuth's The Art of Computer Programming, Vol. 3, §5.3.4, surveys sorting networks. A simple counting argument gives the lower bound: every sorting network has depth at least $\log_2 n$, since each output depends on at most $2^{\text{depth}}$ inputs.
• 1983. Ajtai, Komlós and Szemerédi construct networks of depth $O(\log n)$ and size $O(n\log n)$ (Combinatorica 3 (1983) 1–19, doi:10.1007/BF02579338), matching the lower bound up to a constant. The constant is not computed in the paper and is known to be very large.
• 1990. Paterson simplifies the construction and gives the first explicit, still very large, depth constant (M. S. Paterson, Improved sorting networks with O(log N) depth, Algorithmica 5 (1990) 75–92, doi:10.1007/BF01840378).
• 2014. Goodrich gives Zig-zag sort, a simpler deterministic data-oblivious sorting algorithm with $O(n\log n)$ comparisons that avoids the AKS machinery but is not of logarithmic depth (arXiv:1403.2777).

Setting

There are $n$ registers $R_1,\dots,R_n$ holding elements of a linearly ordered set. An elementary step (a comparator) $(i,j)$ with $i\neq j$ compares the contents of $R_i$ and $R_j$ and exchanges them if the content of $R_i$ is larger. Afterwards $R_i$ holds the minimum and $R_j$ the maximum of the two, and every other register is unchanged. A parallel step is a set of comparators in which no register occurs twice, so it has at most $n/2$ comparators. A comparator network $N$ is a finite sequence of parallel steps, fixed before the input is seen. Its depth $\operatorname{depth}(N)$ is the number of parallel steps and its size $\operatorname{size}(N)$ the total number of comparators. $N$ sorts if for every input $x=(x_1,\dots,x_n)$ the output $N(x)$ satisfies $N(x)_1\le\cdots\le N(x)_n$.

The construction runs on the tree $T$ of finite $0$-$1$ sequences, whose levels are ordered lexicographically. A chain on level $i$ assigns to every node of that level a set of registers, with the sets pairwise disjoint and of a common size $N(C)$. A ⟨k, ε⟩ expander on ⟨A, B⟩, for disjoint register sets $A$ and $B$, is a bipartite graph between $A$ and $B$ of maximum degree $k$ in which every nonempty $X\subseteq A$ has more than $(1-\varepsilon)\varepsilon^{-1}\min\{|X|,\varepsilon|B|\}$ neighbours, and symmetrically for $B$. The Lean development uses the names ComparatorNetwork, compareExchange, IsChain, chainN, IsExpander, IsLowerSection for these objects.

Formalization targets

Goal: the AKS theorem (Abstract and §1, p. 1)

$$\exists\, c>0\ \ \forall n\ge 2\ \ \exists N:\quad N \text{ sorts},\qquad \operatorname{depth}(N)\le c\log_2 n,\qquad \operatorname{size}(N)\le c\,n\log_2 n .$$

The constant is absolute and is not fixed. Any explicit value would be invalidated by the next improvement, and the paper gives none.

Milestones (the paper's numbered lemmas that hold as stated)

• Lemma 3 (p. 6): for $0<\varepsilon<1$ and $c\ge1$ there is $k(\varepsilon,c)$ such that every pair of disjoint sets with $1/c\le|A|/|B|\le c$ carries a $\langle k,\varepsilon\rangle$ expander.
• Lemma 4 (p. 7): performing every comparator of such an expander once, in any order, from $A$ to $B$ leaves all but an $\varepsilon$-fraction of any lower section $S$ with $|S|\le|A|$ in $A$, and symmetrically for upper sections in $B$:

$$|S\setminus\mathrm{Cont}(A)|\le\varepsilon|S| .$$

• Lemma 1 (pp. 3–4): the splitting $V(C,k)$ of a chain, which moves one register of each leaf set up the tree, produces chains with properties (1.1)–(1.5).
• Lemma 2 (p. 4): chains $W(C,k)$ with $a_k-1\le N(W(C,k))\le a_k$ exist under conditions (2a), (2.b).
• Lemma 12(a) (p. 14): a violation of the order relation $R^\beta_G$ between two nodes of a level is witnessed by two consecutive nodes.

Significance

The result. The AKS theorem settles the asymptotic depth of sorting networks at $\Theta(\log n)$ and their size at $\Theta(n\log n)$. It gives an $O(\log n)$-time sorting algorithm with $n$ processors that performs only data-independent comparisons. It is the standard reference point for oblivious sorting in parallel algorithms, circuit complexity (sorting is in $\mathsf{NC}^1$ via comparators) and oblivious RAM constructions. Lemma 4, the ε-halver property of expander comparisons, is the component that later constructions (Paterson) reuse.

Formalizing it. The theorem has been proved since 1983. No Lean proof of the AKS theorem is known. Mathlib has no expander graphs in the ⟨k, ε⟩ sense and no sorting networks. The mission asks for a formal proof of the headline theorem by any route (the AKS construction or Paterson's variant), and for formal proofs of the paper's verified lemmas as reusable components. The expander lemma needs either an explicit family (Margulis; Gabber–Galil) or a probabilistic existence argument, both substantial on their own.

Difficulty

Every elementary argument stalls at depth $O((\log n)^2)$: recursive merging needs $\log n$ merge rounds, and merging two sorted lists by a comparator network needs depth $\Omega(\log n)$. A depth of $O(\log n)$ therefore cannot come from exact merging. It must come from constant-depth approximate operations (ε-halvers, which require bounded-degree expanders) combined with a mechanism that corrects the errors they leave. In the paper this mechanism is a movement of registers up and down a binary tree, controlled by a family of constants chosen in a fixed order ("$\varepsilon_1\ll q_2\ll1-g\ll q_1\ll 1/c_1\ll1$", p. 2). The accounting that shows the misplaced elements decay geometrically is the hard part. Several intermediate lemmas of the paper are false as printed, so the paper's text is not a checklist to transcribe.

Formalization scope

Conventions committed to in Lean:

• Registers are Fin n, and contents lie in an arbitrary linearly ordered type. A network is a List of layers, each a List (Fin n × Fin n) of comparators with distinct endpoints, and no register occurs twice in a layer. A comparator $(i,j)$ puts the minimum into $i$, and both directions $i<j$ and $i>j$ are allowed. Sorts means the output is monotone for every linearly ordered type and every input, not only for permutations.
• $\log_2 n$ is Real.logb 2 n, and the goal is stated for $n\ge2$. The constant $c$ is quantified before $n$.
• Tree levels are Fin (2^i), with numeric order equal to lexicographic order. A chain is a Fin (2^i) → Finset R.
• Definition 2.2 of the paper, read literally, requires $|\Gamma_\emptyset|>0$, which fails, so no graph would be an expander. The expansion inequalities are imposed on nonempty sets only, and the strict inequality is kept.

Trivializing formalizations are ruled out. The goal is not "for every $n$ there is a network of depth $O(\log n)$" with the constant chosen after $n$, which is true for trivial reasons. Layers without the disjointness condition would let a single layer contain a whole insertion sort. A bound on the number of comparisons alone, with unbounded depth, is a different and much older result; the goal states both the depth and the size bound.

The mission states the AKS theorem and the paper's lemmas that are correct as stated. It does not formalize the AKS algorithm itself ($S^\alpha$, $P^\alpha$, the operations CH1–CH4, IMP) or its intermediate Lemmas 5–11 and 13–15. Those depend on unspecified constants constrained only by "sufficiently small" chains, and Lemmas 5, 10 and 12(b) are false as printed. A solver may of course define the algorithm, with pinned constants, as part of a proof.

Contributions welcome: a library of comparator networks (composition, the 0-1 principle, depth of Batcher's networks), existence of bounded-degree bipartite expanders, the ε-halver lemma, and any complete proof of the goal. The network and expander definitions are independent of this paper and reusable.

Selected references

• M. Ajtai, J. Komlós, E. Szemerédi, Sorting in c log n parallel steps, Combinatorica 3(1) (1983) 1–19. doi:10.1007/BF02579338
• K. E. Batcher, Sorting networks and their applications, Proc. AFIPS Spring Joint Computer Conference 32 (1968) 307–314. doi:10.1145/1468075.1468121
• D. E. Knuth, The Art of Computer Programming, Vol. 3: Sorting and Searching, Addison-Wesley, 1973, §5.3.4.
• G. A. Margulis, Explicit constructions of concentrators, Problems of Information Transmission 9 (1973) 325–332.
• O. Gabber, Z. Galil, Explicit constructions of linear-sized superconcentrators, J. Computer and System Sciences 22(3) (1981) 407–420. doi:10.1016/0022-0000(81)90040-4
• M. S. Paterson, Improved sorting networks with O(log N) depth, Algorithmica 5 (1990) 75–92. doi:10.1007/BF01840378
• M. T. Goodrich, Zig-zag sort: a simple deterministic data-oblivious sorting algorithm running in O(n log n) time, STOC 2014. arXiv:1403.2777

Motivation

A maximal independent set (MIS) of a graph is a set of pairwise non-adjacent vertices to which no further vertex can be added. Sequentially an MIS is found greedily in linear time, but the greedy scan is inherently serial. Whether an MIS can be computed by a fast parallel algorithm was a central question of parallel complexity in the early 1980s: Karp and Wigderson gave the first NC algorithm (STOC 1984), and Luby's paper, SIAM J. Comput. 15(4):1036–1053, 1986, gave a much simpler one. MIS is a subroutine of many parallel and distributed graph algorithms (colouring, matching, symmetry breaking), and Luby's randomized algorithm remains the standard one in distributed computing.

The paper's second contribution, the subject of this mission, is a general method for removing randomness: analyse the randomized algorithm under pairwise independence only, then realize pairwise independent random variables on a sample space of polynomial size and try every sample point in parallel. The same method, often attributed jointly to Luby (1986) and to Alon, Babai and Itai (J. Algorithms 7, 1986), became a standard tool of derandomization.

Setting

Let $G = (V, E)$ be a finite simple graph with $n = |V|$ vertices labelled $0, \dots, n-1$. The algorithm keeps a set $I$ (initially empty) and the current graph $G' = (V', E')$, the subgraph of $G$ induced on $V'$ (initially $V' = V$). For $W \subseteq V'$ the neighbourhood is $N(W) = \{ i \in V' : \exists j \in W, (i,j) \in E' \}$. Each execution of the loop body selects an independent set $I' \subseteq V'$, adds it to $I$, and deletes $I' \cup N(I')$ from $V'$; the loop runs while $V' \ne \emptyset$. Write $d(i)$ for the degree of $i$ in $G'$, $Y_k$ for the number of edges of $G'$ before the $k$-th execution, and $\mathrm{sum}(i) = \sum_{j \in \mathrm{adj}(i)} 1/d(j)$.

Algorithm B's select step draws a coin $\mathrm{coin}(i) \in \{0,1\}$ for each vertex, with $\Pr[\mathrm{coin}(i) = 1] = 1/2d(i)$, puts $X = \{ i : \mathrm{coin}(i) = 1 \}$, and removes from $X$ the endpoint of smaller degree of every edge inside $X$ (both endpoints on a tie).

The sample space. Fix a prime $q$ with $n \le q \le 2n$. The sample points are the pairs $(x, y)$ with $0 \le x, y \le q-1$, each of probability $1/q^2$. With $n(i) = \lfloor q/2d(i) \rfloor$, the coin of vertex $i$ at $(x,y)$ is $1$ iff $(x + y \cdot i) \bmod q < n(i)$, so $\Pr[\mathrm{coin}(i) = 1] = p'_i = \lfloor q/2d(i) \rfloor / q$, and distinct coins are pairwise independent.

Algorithm D. Each execution of the loop body first moves the isolated vertices of $G'$ into $I$. Then:

• Case 1. If a vertex $i$ of maximum degree has $d(i) \ge n/16$, it joins $I$, and $\{i\} \cup N(\{i\})$ is deleted.
• Case 2. Otherwise all $q^2$ sample points are tried, the one whose coins make Algorithm B's select step eliminate the most edges is kept, and its $I'$ is used.

No random bits are used.

Formalization targets

Goal: the round bound and correctness of Algorithm D

For every graph $G$ on $n$ vertices, every prime $q$ with $n \le q \le 2n$, and every run of Algorithm D (every tie-break among maximum-degree vertices and every maximizing sample point), the loop body is executed exactly $k$ times, with

$$k \ \le\ \frac{\log(n^2)}{\log(18/17)} + 16 \ \le\ 25 \cdot \log_2 n + 16,$$

and the output $I$ is a maximal independent set of $G$.

Milestones

1. The sample space: Lemma 1, $\Pr[X_i = R_j] = n_{ij}/q$, and Lemma 2, $\Pr[X_i = R_j, X_{i'} = R_{j'}] = n_{ij} n_{i'j'}/q^2$ for $i \ne i'$.
2. The Technical Lemma: for $p_1 \ge \dots \ge p_n \ge 0$ and $c > 0$, $\max_l (\alpha_l - c\beta_l) \ge \tfrac12 \min\{\alpha_n, 1/c\}$.
3. The two steps of the proof of Theorem 1: $E[Y_k - Y_{k+1}] \ge \tfrac12 \sum_i d(i) \Pr[i \in N(I')]$, and $\tfrac12 \sum_{\mathrm{sum}(i) \le 2} d(i)\,\mathrm{sum}(i) + \sum_{\mathrm{sum}(i) > 2} d(i) \ge |E'|$.
4. Lemma C and Theorem 2: with pairwise independent coins of law $1/2d(i)$,

$$\Pr[i \in N(I')] \ge \tfrac18 \min\{\mathrm{sum}(i), 1\}, \qquad E[Y_k - Y_{k+1}] \ge \tfrac{1}{16} Y_k .$$

5. The rounding bound $\tfrac89 p_i \le p'_i \le p_i$ when $d(i) < n/16$.
6. Lemma D and Theorem 3: with pairwise independent coins of law $p'_i$ and all $d(i) < n/16$,

$$\Pr[i \in N(I')] \ge \tfrac19 \min\{\mathrm{sum}(i), 1\}, \qquad E[Y_k - Y_{k+1}] \ge \tfrac{1}{18} Y_k .$$

7. In Case 2 some sample point eliminates at least $1/18$ of the edges; Case 1 occurs at most 16 times in any run before it terminates.

Significance

The goal is the deterministic half of Luby's result: an MIS is computed in $O(\log n)$ parallel rounds with no randomness, which places MIS in deterministic NC. The pairwise-independent analysis (Lemmas C, D, Theorems 2, 3) is the reusable part: it shows that the Monte Carlo algorithm's progress guarantee survives when mutual independence is weakened to pairwise independence, which is what makes a sample space of size $q^2 = O(n^2)$ sufficient. Lemmas 1 and 2 are the standard construction of pairwise independent variables with prescribed rational marginals.

All of these results are proved in the paper. None is formalized on the platform. A related but different object is the platform's dot-product hash family (AlmostLossless.pairwiseIndependent_dotHash), which has uniform marginals over a field and is not the $q^2$-point matrix space with prescribed marginals $n_{ij}/q$. The companion mission A Simple Parallel Algorithm for the Maximal Independent Set Problem I formalizes Theorem 1, the mutually independent analysis of Algorithms A and B.

Difficulty

The obvious route to Theorem 2 repeats the proof of Lemma B, which lower-bounds $\Pr[i \in N(I')]$ by a product over independent events. Under pairwise independence the probability of an intersection of three or more coin events is not determined by the marginals, so that product argument fails, and the constant degrades from $\tfrac18$ to $\tfrac1{16}$.

The round bound needs a separate argument for high-degree vertices. The rounded probabilities $p'_i$ are close to $p_i$ only when $q/2d(i)$ is large, which is why vertices of degree at least $n/16$ are handled by Case 1. Counting the Case 1 rounds uses the vertex count $n$ of the original graph, not of the current one. Correctness at termination requires an invariant linking $I$, $V'$ and $G$ across both kinds of rounds and the deletion of isolated vertices.

Formalization scope

Vertices are Fin n with labels $0, \dots, n-1$, which is §4.2's indexing of $X_0, \dots, X_{n-1}$; the label enters $\mathbb{Z}/q\mathbb{Z}$ as a residue, and labels are distinct mod $q$ because $n \le q$. The current graph is the induced subgraph kept on the full vertex type, with deleted vertices isolated. One execution of the loop body is a relation between states $(I, V')$ that leaves the maximizing vertex (Case 1) and the maximizing sample point (Case 2) free, as the page does, and a run is any sequence of states starting at $(\emptyset, V)$ that follows the relation while $V' \ne \emptyset$. The goal asks for the first index $k$ with $V' = \emptyset$, so a statement about a later state or a bound on $k$ without termination does not meet it.

The conditions $d(i) \ge n/16$ and $d(i) < n/16$ are encoded exactly as $n \le 16\,d(i)$ and $16\,d(i) < n$ in $\mathbb{N}$. $\lfloor q/2d(i) \rfloor$ is natural-number division. The printed code tests $(x + y\cdot i) \bmod q \le n(i)$, which puts $n(i) + 1$ residues in $X$ and contradicts $p'_i = \lfloor p_i q \rfloor / q$ stated on the same page; the formalization uses the strict test.

Lemmas C, D and Theorems 2, 3 quantify over every probability space carrying measurable, pairwise independent (IndepFun for each pair of distinct vertices) coins with the stated marginals at vertices of positive degree. Replacing pairwise by mutual independence, or fixing the probability space, would weaken them. They are stated for a fixed current graph, that is, as the expectation conditional on the state before the round, which is what their proofs establish. Expectations are Bochner integrals of a function with finitely many values and are therefore genuine. Lemma 2 carries the hypothesis $i \ne i'$, implicit on the page.

The development needs the induced subgraph and degree bookkeeping from Mathlib's SimpleGraph, pairwise independence from ProbabilityTheory.IndepFun, finite counting in ZMod q, and real logarithms. The pairwise-independent analysis (Lemma C to Theorem 3) and the sample-space lemmas are reusable beyond this mission. Contributions to any milestone are welcome.

Selected references

• M. Luby, A Simple Parallel Algorithm for the Maximal Independent Set Problem, SIAM J. Comput. 15(4):1036–1053, 1986. https://doi.org/10.1137/0215074
• R. M. Karp and A. Wigderson, A Fast Parallel Algorithm for the Maximal Independent Set Problem, J. ACM 32(4):762–773, 1985. https://doi.org/10.1145/4221.4226
• N. Alon, L. Babai and A. Itai, A Fast and Simple Randomized Parallel Algorithm for the Maximal Independent Set Problem, J. Algorithms 7(4):567–583, 1986. https://doi.org/10.1016/0196-6774(86)90019-2

Motivation

Bin packing asks for the fewest unit-capacity bins that hold a given list of item sizes. It models table formatting, the placement of program segments on pages, and the allocation of files to disc tracks, and it is NP-complete, so exact solutions require search in general. Johnson, Demers, Ullman, Garey and Graham (SIAM J. Comput. 3 (1974)) therefore studied four simple placement heuristics and bounded how far each can be from the optimum in the worst case. Their paper is one of the founding results of the worst-case analysis of approximation algorithms.

This mission concerns the two decreasing heuristics, which sort the items from largest to smallest before placing them. For them the paper proves that at most $\tfrac{11}{9}$ of the optimum, plus an additive constant, is ever used, and that the factor $\tfrac{11}{9}$ cannot be improved.

Timeline.

• 1973: D. S. Johnson's MIT thesis proves $FFD(L)\le \tfrac{11}{9}L^*+4$; the argument exceeds 75 pages.
• 1974: Johnson, Demers, Ullman, Garey and Graham publish the bound for FFD and BFD, with a complete proof of the reduction from BFD to FFD and an outline of the FFD argument.
• 1985: B. S. Baker gives a shorter proof of $FFD(L)\le\tfrac{11}{9}L^*+3$ (J. Algorithms 6).
• 1991: M. Yue publishes a proof of $FFD(L)\le\tfrac{11}{9}L^*+1$.
• 2007: G. Dósa determines the tight additive constant, $FFD(L)\le\tfrac{11}{9}L^*+\tfrac{6}{9}$ (ESCAPE 2007, LNCS 4614).

Setting

A list is a finite sequence $L=(a_1,a_2,\dots,a_n)$ of real numbers in $(0,1]$; values may repeat. A bin has capacity $1$; its level is the sum of the numbers placed in it. The optimum $L^*$ is the least number of bins into which the elements of $L$ can be distributed so that no bin has level exceeding $1$.

The bins $B_1,B_2,\dots$ start empty and the elements are placed one at a time, in list order.

• First-Fit (FF) places $a_i$ into the bin $B_j$ of least index whose level $\beta$ satisfies $\beta\le 1-a_i$.
• Best-Fit (BF) places $a_i$ into a bin whose level $\beta$ satisfies $\beta\le 1-a_i$ and is as large as possible, the one of least index among ties.
• First-Fit Decreasing (FFD) and Best-Fit Decreasing (BFD) first arrange $L$ into nonincreasing order and then apply FF, respectively BF.

$FFD(L)$ and $BFD(L)$ are the numbers of bins that receive at least one element.

Two auxiliary notions from the paper's proof also appear among the milestones. The position $(j,k)$ of an element in a packing means that it is the $k$-th element placed into bin $j$. The weight $W(X)$ of a collection of elements is defined through $k$-pieces, the elements in $(\tfrac1{k+1},\tfrac1k]$. Each element has the weight $w_1(x)=\lfloor 1/x\rfloor^{-1}$. A pair $(x,y)$ with $x$ a $k$-piece and $kx+y\le1$ has the discounted weight $w_2(x,y)=w_1(x)+\tfrac{k-1}{k}w_1(y)$, and any other pair has $w_1(x)+w_1(y)$. $W(X)$ is the least total weight over all ways of grouping $X$ into singletons and pairs.

Formalization targets

Goal: Theorem 3.2

For every list $L$,

$$FFD(L)\le \frac{11}{9}L^*+4\qquad\text{and}\qquad BFD(L)\le\frac{11}{9}L^*+4 .$$

The constants are the paper's. Both halves are part of the goal.

Milestones, in the order the argument uses them

1. Lemma 3.3. If $FFD(L)>rL^*+d$ with $r,d\ge1$, the list $L'$ keeping only the elements exceeding $(r-1)/r$ also has $FFD(L')>rL'^*+d$; the same for BFD. With $r=\tfrac{11}{9}$ this reduces the goal to lists in $(\tfrac2{11},1]$.
2. Claims 3.4.5 and 3.4.6, two steps of the proof of Theorem 3.4 that concern only the FFD packing $PF$ and the BFD run. On $[\tfrac16,1]$, BFD places every element exceeding $\tfrac13$ exactly where FFD does. Among the remaining positions of $PF$, the lexicographic order of positions respects the order of the sorted list.
3. Theorem 3.4. If $L\subseteq[\tfrac16,1]$, then $BFD(L)\le FFD(L)$. This transfers the bound from FFD to BFD on $(\tfrac2{11},1]$.
4. Lemma 4.2. For every integer $N\ge4$ and $L\subseteq(\tfrac1N,\tfrac12]$,

$$W(L)\ge FFD(L)-N+2 .$$

5. The reduced assertion (Section 4, p. 314). If $L\subseteq(\tfrac2{11},1]$, then

$$FFD(L)\le\frac{11}{9}L^*+4 .$$

6. Theorem 3.1, the matching lower bound: for each $k\ge1$ there is a list with $L^*=k$ and $FFD(L)=BFD(L)>\tfrac{11}{9}L^*-2$.

Significance

The bound makes FFD and BFD, which run in $O(n\log n)$ time, the reference heuristics for off-line bin packing. The $\tfrac{11}{9}$ bound and its proof technique of weighting functions were the model for the analysis of many later packing and scheduling heuristics. Theorem 3.1 shows that the factor is exact, so together with the goal it determines $\lim_{k\to\infty}R_{FFD}(k)=\lim_{k\to\infty}R_{BFD}(k)=\tfrac{11}{9}$, where $R_A(k)$ is the largest ratio $A(L)/L^*$ over lists with $L^*=k$.

The result is proved, but the source proves it only in part. The paper gives complete proofs of Lemma 3.3, Theorem 3.4 and Theorem 3.1. For the reduced assertion it gives only an outline, whose central inequalities involve maps the paper never defines, and it refers to the thesis for the details. Lemma 4.2 is proved in the paper through two claims. A formal proof of the goal must therefore either formalize one of the later complete proofs (Baker 1985, Yue 1991, Dósa 2007) or reconstruct the thesis argument. No machine-checked proof of the $\tfrac{11}{9}$ bound is present in Mathlib or on the platform.

Difficulty

The obvious approach, used for First-Fit in Section 2 of the same paper, assigns each element a weight depending only on its size, so that every bin of the algorithm's packing weighs at least $1$ and every bin of an optimal packing weighs at most the target ratio. For FFD no weighting of single elements works at ratio $\tfrac{11}{9}$. Summing $w_1$ over the elements overcharges the FFD packing: a set of elements fitting into one bin can carry total $w_1$-weight well above $\tfrac{11}{9}$. The paper's remedy is a weight defined on pairs, $W(X)$, which discounts elements that could share a bin with a larger one. Even with $W$, the bins of FFD whose largest element exceeds $\tfrac12$ do not fit the scheme. Handling them requires a case analysis that the paper only sketches and that runs to more than 75 pages in the thesis.

The BFD half cannot be obtained by bounding BFD by FFD in general: there are lists with $BFD(L)=\tfrac{10}{9}FFD(L)$. Theorem 3.4 works only because Lemma 3.3 first removes all elements below $\tfrac2{11}$.

Formalization scope

Lists are L : List ℝ with the predicate IsList L ($0<a\le1$ for every element), assumed by every statement. $L^*$ is optBins L, the least b : ℕ admitting a map from the items to Fin b with every bin sum at most $1$. A run keeps the nonempty bins as a List (List ℝ) in index order and opens a new bin at the end exactly when no nonempty bin fits, which matches the paper's "least $j$" over infinitely many empty bins. The fit test is non-strict. FFD and BFD are FF and BF applied to sortDesc L, a stable merge sort into nonincreasing order. They are defined for every list, so the goal is stated for arbitrary, unsorted $L$. Positions are $0$-based pairs (bin, place in bin) read off the run.

$W$ sorts its argument into nonincreasing order, so index is the position in that order. It then minimizes over involutions of the positions, which encode the partitions into one- and two-element sets. Weights are real-valued; the paper's use of rationals is incidental. The range hypotheses are exactly the paper's: $[\tfrac16,1]$ is closed in Theorem 3.4, $(\tfrac2{11},1]$ is open at $\tfrac2{11}$, and Lemma 4.2 has $\tfrac1N<a\le\tfrac12$.

A weakened goal, such as $FFD(L)\le\tfrac{11}{9}L^*+c$ with a larger $c$, a bound for sorted lists only, or the FFD half alone, is a different theorem and does not close the mission. Claims 3.4.1–3.4.4 and 3.4.7 and the inequalities $(*)$, $(**)$ of the outline are not stated: they concern the paper's step-by-step construction and the undefined maps $f$, $g$.

A complete development needs basic lemmas about FF and BF runs (levels stay at most $1$, a new bin opens only when nothing fits, runs on prefixes). It also needs invariance of FFD and BFD under permutations of equal elements, the monotonicity of $L^*$ under deletion, and $L^*\ge\sum_i a_i$. These are reusable in the other missions of this series. Proofs of individual milestones, alternative complete proofs of the goal, and sharper additive constants are all welcome.

Selected references

• D. S. Johnson, A. Demers, J. D. Ullman, M. R. Garey, R. L. Graham, Worst-Case Performance Bounds for Simple One-Dimensional Packing Algorithms, SIAM Journal on Computing 3(4):299–325, 1974. https://doi.org/10.1137/0203025
• D. S. Johnson, Near-Optimal Bin Packing Algorithms, Ph.D. thesis, Massachusetts Institute of Technology, 1973 (reference [8] of the paper above).
• B. S. Baker, A new proof for the first-fit decreasing bin-packing algorithm, Journal of Algorithms 6(1):49–70, 1985. https://doi.org/10.1016/0196-6774(85)90018-5
• M. Yue, A simple proof of the inequality FFD(L) ≤ 11/9 OPT(L) + 1, ∀L, for the FFD bin-packing algorithm, Acta Mathematicae Applicatae Sinica 7(4):321–331, 1991.
• G. Dósa, The tight bound of first fit decreasing bin-packing algorithm is FFD(I) ≤ 11/9 OPT(I) + 6/9, ESCAPE 2007, LNCS 4614:1–11, 2007. https://doi.org/10.1007/978-3-540-74450-4_1

Motivation

Bin packing asks for the fewest unit-capacity bins that hold a given list of item sizes. It is one of the first problems studied through the worst-case analysis of approximation algorithms, and it models storage allocation, paging and file placement on tracks, as well as cutting-stock problems in operations research. Deciding the optimum exactly is NP-hard, so the practical question is how badly simple rules can do. The two simplest on-line rules, First-Fit and Best-Fit, are still the baseline against which every later bin-packing heuristic is measured.

Timeline:

• 1972. Garey, Graham and Ullman announce that First-Fit uses at most about $1.7$ times the optimal number of bins (Proc. 4th ACM STOC, 1972); Johnson's thesis (MIT, 1973) develops the analysis.
• 1974. Johnson, Demers, Ullman, Garey and Graham prove $FF(L)\le 1.7L^*+2$ and $BF(L)\le 1.7L^*+2$ for every list, and give lists with $FF(L)=BF(L)>1.7L^*-8$ for every optimum $L^*=k$, so the asymptotic worst-case ratio of both rules is exactly $\tfrac{17}{10}$ (SIAM J. Comput. 3(4)). This paper is the source of the mission.
• 1976–2014. The additive constant is lowered: Garey, Graham, Johnson and Yao (1976) show $FF(L)\le\lceil 1.7L^*\rceil$, and Dósa and Sgall prove the tight bound $FF(L)\le\lfloor 1.7L^*\rfloor$ (STACS 2013) and the same bound for Best-Fit (ICALP 2014).

Setting

A list is a finite sequence $L=(a_1,a_2,\dots,a_n)$ of real numbers in $(0,1]$; values may repeat. A bin has capacity $1$, and its level is the sum of the numbers in it. The optimum $L^*$ is the minimum number of bins into which the elements of $L$ can be placed so that no bin contains numbers whose sum exceeds $1$.

Both rules place $a_1,\dots,a_n$ in this order into bins $B_1,B_2,\dots$, each initially at level $0$, and never move an element once placed.

1. First-Fit (FF) places $a_i$ into the bin $B_j$ of least index whose level $\beta$ satisfies $\beta\le 1-a_i$.
2. Best-Fit (BF) places $a_i$ into a bin whose level $\beta$ satisfies $\beta\le 1-a_i$ and is as large as possible, taking the least index among ties.

$FF(L)$ and $BF(L)$ are the numbers of nonempty bins at the end. The worst-case ratio at optimum $k$ is

$$R_{FF}(k)=\sup\Bigl\{\frac{FF(L)}{L^*}:L^*=k\Bigr\},\qquad R_{BF}(k)=\sup\Bigl\{\frac{BF(L)}{L^*}:L^*=k\Bigr\}.$$

The analysis also uses a weighting function $W:[0,1]\to[0,1]$, piecewise linear with $W(\alpha)=\tfrac65\alpha$ on $[0,\tfrac16]$, $\tfrac95\alpha-\tfrac1{10}$ on $(\tfrac16,\tfrac13]$, $\tfrac65\alpha+\tfrac1{10}$ on $(\tfrac13,\tfrac12]$ and $1$ on $(\tfrac12,1]$, and the coarseness of a bin of a completed packing: the largest $1-\operatorname{level}(B')$ over the bins $B'$ of smaller index, and $0$ for the first bin.

Formalization targets

Goal: the asymptotic ratio (Corollary of Section 2, p. 306)

$$\lim_{k\to\infty}R_{FF}(k)=1.7\qquad\text{and}\qquad\lim_{k\to\infty}R_{BF}(k)=1.7.$$

The goal fixes only the asymptotic ratio and leaves the additive constants free, so it is the statement that survives the later improvements of the constants.

Milestones, in the order the proof uses them

• Claim 2.2.1 (p. 304): a bin with total size at most $1$ has $\sum_i W(b_i)\le\tfrac{17}{10}$.
• Claim 2.2.2 (p. 305): in an FF or BF packing, every element placed into a bin before the bin was more than half full exceeds the bin's coarseness.
• Claim 2.2.3 (p. 305): a bin of coarseness $\alpha<\tfrac12$ whose level exceeds $1-\alpha$ has weight at least $1$.
• Claim 2.2.4 (p. 306): a bin of coarseness $\alpha<\tfrac12$ with weight $1-\beta$, $\beta>0$, either holds a single element at most $\tfrac12$ or has level at most $1-\alpha-\tfrac59\beta$.
• Theorem 2.2 (p. 304): $FF(L)\le 1.7L^*+2$ and $BF(L)\le 1.7L^*+2$ for every list.
• Theorem 2.1 (p. 301): for every $k\ge1$ there is a list with $L^*=k$ and $FF(L)=BF(L)>1.7L^*-8$.

A companion item, not a milestone, records the explicit list of Fig. 3 (p. 307) with $L^*=10$ and $FF(L)=BF(L)=17$.

Significance

The result fixes the worst-case behaviour of the two simplest bin-packing heuristics: neither ever uses more than about $70\%$ more bins than an optimal packing, and both can be forced to. The weighting-function technique introduced for this bound became the standard method for analysing bin-packing heuristics, including First-Fit Decreasing, Harmonic-type algorithms and on-line lower bounds, and the constant $\tfrac{17}{10}$ is the reference point for later on-line algorithms.

The theorem is proved, and its constants have since been sharpened. No machine-checked proof of any of these results is known. This mission produces a Lean model of on-line bin packing (the optimum, the First-Fit and Best-Fit runs with their placement history, and the worst-case ratio) that the other missions of this paper and later bin-packing formalizations can reuse. It also produces formal proofs of the weighting-function bounds, of the $1.7L^*+2$ upper bound and of the lower-bound construction.

Difficulty

The first idea, charging each bin its level, gives only $FF(L)\le 2L^*+1$: at most one bin is at most half full. The ratio $\tfrac{17}{10}$ comes from bins that are more than half full but far from full, and a bound on the total size of the elements cannot see them. No property of the final packing alone suffices: the bins that are far from full can only be controlled through the order in which the rule opened and filled them, so the argument depends on the dynamics of the run. On the lower-bound side, the natural periodic list (sizes near $\tfrac16,\tfrac13,\tfrac12$, p. 301) gives only the ratio $\tfrac53$; reaching $\tfrac{17}{10}$ needs a list on which both rules waste space in every medium bin, for every $k$, while $L^*$ is still known exactly.

Formalization scope

A list is L : List ℝ with the hypothesis IsList L (every element in $(0,1]$), and every statement assumes it. $L^*$ is optBins L, the least b : ℕ for which some assignment Fin L.length → Fin b has every bin sum at most $1$. A run is a fold over the list that keeps only the nonempty bins, in index order, each with its contents in placement order. A new bin is opened at the end exactly when no nonempty bin fits, which is the paper's "least $j$" over infinitely many initially empty bins, since elements are positive. The fit test is the non-strict $\beta+a_i\le1$, and Best-Fit breaks ties by least index. The placement history (the bin chosen for each element and that bin's level just before) is read off the run on the prefix of the list. Indices are $0$-based. Coarseness is computed in the completed packing. $W$ is a function ℝ → ℝ and is only ever applied to elements of $(0,1]$. $R_{FF}(k)$ and $R_{BF}(k)$ are suprema in the extended nonnegative reals $[0,\infty]$, and the limit is taken there.

A real-valued supremum would be $0$ on an empty or unbounded family, and the limit statement would then say nothing about the algorithms. The extended-real supremum rules this trivialization out. Every claim is stated for the concrete First-Fit run and the concrete Best-Fit run, not for an abstract rule with the properties used in the proof.

Claim 2.2.4 is printed with alternative (i) "$m=1$ and $b_1<\tfrac12$", which is false: First-Fit on $(0.6,0.5)$ gives a counterexample. The mission states it with $b_1\le\tfrac12$, which is what the paper's proof establishes and what the main proof uses. The milestone text keeps the printed version.

The model definitions are reusable for any on-line bin-packing rule, since the run is parameterized by the choice rule. Contributions welcome: proofs of the milestones, general lemmas about the runs (levels stay at most $1$, at most one bin is at most half full, the history determines the final packing), and the computation of $L^*$ for the explicit lists of Theorem 2.1 and Fig. 3.

Selected references

• D. S. Johnson, A. Demers, J. D. Ullman, M. R. Garey, R. L. Graham, Worst-Case Performance Bounds for Simple One-Dimensional Packing Algorithms, SIAM Journal on Computing 3(4):299–325, 1974. https://doi.org/10.1137/0203025
• M. R. Garey, R. L. Graham, J. D. Ullman, Worst-case analysis of memory allocation algorithms, Proc. 4th ACM STOC, 1972.
• D. S. Johnson, Near-Optimal Bin Packing Algorithms, PhD thesis, MIT, 1973.
• M. R. Garey, R. L. Graham, D. S. Johnson, A. C. Yao, Resource constrained scheduling as generalized bin packing, J. Combinatorial Theory Ser. A 21, 1976.
• G. Dósa, J. Sgall, First Fit bin packing: A tight analysis, STACS 2013, LIPIcs 20:538–549. https://doi.org/10.4230/LIPIcs.STACS.2013.538
• G. Dósa, J. Sgall, Optimal analysis of Best Fit bin packing, ICALP 2014, LNCS 8572.

Motivation

A branching in a directed graph is a set of edges that contains no cycle (even ignoring directions) and in which no two edges point to the same node; a connected branching is an arborescence, a tree rooted at one node with all edges directed away from the root. The optimum branching problem asks, for real weights on the edges, for a branching of maximum total weight. It contains the minimum-cost spanning arborescence problem (the directed analogue of the minimum spanning tree), which appears in network design, in the analysis of broadcast and routing structures, in phylogenetics, and in dependency parsing in computational linguistics, where maximum spanning arborescences are the standard decoding step of graph-based parsers.

J. Edmonds solved the problem in Optimum branchings (J. Res. Nat. Bur. Standards 71B (1967) 233–240). The paper gives an algorithm (the shrinking algorithm usually attributed to Chu–Liu and Edmonds) and, proved together with it, a polyhedral theorem: the linear system that every branching obviously satisfies has no other vertices. This was one of the first integral polyhedron theorems beyond bipartite matching and network flows, and together with Edmonds' matching polytope (1965) it set the pattern of polyhedral combinatorics: describe the convex hull of the combinatorial objects by linear inequalities, and prove optimality by a linear programming dual.

Timeline:

• 1965: Y. J. Chu and T. H. Liu describe the shrinking algorithm for the maximum arborescence.
• 1965: Edmonds, Paths, trees, and flowers and Maximum matching and a polyhedron with 0,1-vertices: the matching polytope.
• 1967: Edmonds, Optimum branchings: the algorithm, Theorem 2 (vertices of the branching polyhedron), and the dual certificate built along the algorithm.
• 1970–1971: Edmonds' matroid intersection theorem, which contains the branching polyhedron theorem as the intersection of a graphic matroid and a partition matroid.
• 1977–1986: faster implementations (Tarjan; Gabow, Galil, Spencer and Tarjan).

Setting

A graph $G$ consists of a finite set $V$ of nodes and a finite set $E$ of edges. Each edge $e$ is directed toward a node $\mathrm{front}(e)$, its front end, and away from a different node $\mathrm{rear}(e)$, its rear end. Parallel edges are allowed; loops are not.

For $F\subseteq E$, a node $v$ meets $k$ edges of $F$ if $\#\{e\in F:\mathrm{front}(e)=v\}+\#\{e\in F:\mathrm{rear}(e)=v\}=k$. A set $B\subseteq E$ is a forest if it contains no polygon, i.e. no nonempty $F\subseteq B$ in which every node meets zero or two edges of $F$; it is a branching if in addition distinct edges of $B$ have distinct front ends. The incidence vector $x^B\in\mathbb R^E$ of $B$ has $x^B_e=1$ for $e\in B$ and $0$ otherwise.

The branching polyhedron $P_G\subseteq\mathbb R^E$ is the set of $x$ with

• $(L_1)$ $x_e\ge0$ for every edge $e$;
• $(L_2)$ $\sum_{e:\,\mathrm{front}(e)=v}x_e\le1$ for every node $v$;
• $(L_3)$ $\sum_{e:\,\mathrm{front}(e),\mathrm{rear}(e)\in S}x_e\le|S|-1$ for every set $S$ of two or more nodes.

A vertex of a set $P\subseteq\mathbb R^E$ is a point of $P$ that is the unique maximizer over $P$ of some linear function $x\mapsto\sum_e c_ex_e$.

For weights $c\in\mathbb R^E$, the dual variables are $y_h$ for each node $v_h$ and $y_S$ for each $S$ with $|S|\ge2$; write $w_e=\sum_{S\ni\mathrm{front}(e),\mathrm{rear}(e)}y_S$ and $(b,y)=\sum_hy_h+\sum_S(|S|-1)y_S$. Edmonds' conditions are (15) $y_h\ge0$, (16) $y_S\ge0$, (17) $y_{\mathrm{front}(e)}+w_e\ge c_e$ for every edge, and, for a branching $B$, (18) $y_h\ne0\Rightarrow$ some edge of $B$ enters $v_h$, (19) $y_S\ne0\Rightarrow$ exactly $|S|-1$ edges of $B$ lie inside $S$, (20) $y_{\mathrm{front}(e)}+w_e=c_e$ for $e\in B$.

Formalization targets

Goal: Theorem 2 (p. 235)

$$\{x:\ x\text{ is a vertex of }P_G\}\;=\;\{x^B:\ B\text{ is a branching of }G\}.$$

Both inclusions, for every finite loopless directed multigraph.

Milestones

1. §5, p. 236: for every branching $B$, $x^B\in P_G$.
2. §5, p. 236: for every branching $B$, $x^B$ is a vertex of $P_G$.
3. §6, (12)–(14): if $B$ is a branching and $y$ satisfies (15)–(20), then $(c,x^B)=(b,y)$, $x^B$ maximizes $(c,x)$ over $P_G$, and $y$ minimizes $(b,y)$ subject to (15)–(17).
4. §7, p. 237: for every $c\in\mathbb R^E$ there are a branching $B$ and a $y$ satisfying (15)–(20).
5. Lemma 1, p. 236: for every $c\in\mathbb R^E$ some branching vector lies in $P_G$ and maximizes $\sum_ec_ex_e$ over $P_G$.

Significance

Theorem 2 says that the linear program $\max\{(c,x):x\in P_G\}$ always has an optimal solution that is a branching, and that every vertex of $P_G$ is one. Consequently optimum branchings, and after the reductions of the paper's §2 optimum spanning and rooted arborescences, can be computed by linear programming, and their optimality is certified by a dual vector satisfying (15)–(20). The same statement underlies the separation-based treatment of arborescence constraints in integer programming formulations of network design and of the asymmetric travelling salesman problem. The integrality of the dual for integer weights (the paper's §8) yields min–max theorems of König type for branchings.

The result is proved and classical; no machine-checked proof of it in a proof assistant is known. The mission asks for the paper's own proof chain: branching vectors are points and vertices of $P_G$, linear programming optimality from complementary slackness, existence of a dual certificate for every weight vector, and the deduction of Theorem 2. Proofs through matroid intersection or total dual integrality would also establish the goal and are welcome as alternative routes.

Difficulty

The inclusion "branching vectors are vertices" and the certificate criterion are short. The substance is Milestone 4: for arbitrary real weights, a branching and a dual vector satisfying the complementary slackness conditions must exist simultaneously. Finiteness gives an optimum branching at once, but that says nothing about optimality over the fractional points of $P_G$; the difficulty is the dual. The natural attempt, taking $y_S=0$ for all sets and $y_h$ the largest positive weight entering $v_h$, violates (20) as soon as the greedy choice closes a circuit: the $(L_3)$ duals of nested node sets, arising from repeatedly shrinking circuits, are needed, and they must be kept nonnegative through weight changes of the form $c_3+c_0-c_4$ on edges entering a shrunk circuit.

Formalization scope

A graph is a structure Graph V E with front rear : E → V and a proof that front e ≠ rear e; V and E carry Fintype and DecidableEq. Edge sets are Finset E; vectors are E → ℝ; the linear function with weights c is ∑ e, c e * x e. A branching is defined combinatorially (no nonempty edge subset in which every node meets zero or two edges, and distinct front ends), never by counting edges inside node sets, and $P_G$ is the solution set of $(L_1)$–$(L_3)$, never a convex hull; either shortcut would make half of Theorem 2 true by definition. A vertex is a unique maximizer of a linear function, as on p. 236 (Mathlib's Set.exposedPoints has the same content); the set variables of the dual are a function Finset V → ℝ whose values on sets of fewer than two nodes are ignored. The right side of $(L_3)$ is the real number $|S|-1$.

Implicit conventions made explicit: the no-loop condition is part of the graph (with a loop $e$, the vector of $\{e\}$ is a vertex of $P_G$ but not a branching); parallel edges are allowed; weights have arbitrary sign and the empty branching is allowed. The mission does not model the algorithm of §4 or Theorem 1's notion of a "good" algorithm; Milestone 4 states only the existence of a certificate, which is what Lemma 1 uses.

Useful reusable infrastructure: finite directed multigraphs with an edge type, forests via polygons, and a finite LP duality lemma for $\max\{c^\top x: x\ge0,\ Ax\le b\}$; contributions of either are welcome.

Selected references

• J. Edmonds, Optimum branchings, J. Res. Nat. Bur. Standards Sect. B 71B (1967), 233–240. https://doi.org/10.6028/jres.071b.032
• Y. J. Chu and T. H. Liu, On the shortest arborescence of a directed graph, Scientia Sinica 14 (1965), 1396–1400.
• J. Edmonds, Maximum matching and a polyhedron with 0,1-vertices, J. Res. Nat. Bur. Standards 69B (1965), 125–130. https://doi.org/10.6028/jres.069B.013
• R. E. Tarjan, Finding optimum branchings, Networks 7 (1977), 25–35. https://doi.org/10.1002/net.3230070103
• H. N. Gabow, Z. Galil, T. Spencer and R. E. Tarjan, Efficient algorithms for finding minimum spanning trees in undirected and directed graphs, Combinatorica 6 (1986), 109–122. https://doi.org/10.1007/BF02579168
• A. Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Springer (2003), Chapter 52.

Motivation

The stable set problem asks for a largest set of pairwise non-adjacent vertices in a graph; its size is the stability number $\alpha(G)$. It is NP-hard in general, and a standard way to attack it in integer programming is to write down linear inequalities valid for all stable sets and solve the resulting linear program. The weakest such relaxation uses only the edge inequalities $x_v+x_w\le 1$; its optimum can be as large as $|V|/2$ on graphs with small $\alpha(G)$. Adding, for every odd circuit $C$, the inequality $\sum_{u\in C}x_u\le\frac12(|C|-1)$ gives the odd-cycle relaxation, the first strengthening that cuts off the fractional point $x\equiv\frac12$ on odd cycles.

Section 7 of V. Chvátal, On certain polytopes associated with graphs (J. Combin. Theory Ser. B 18 (1975) 138–154, doi:10.1016/0095-8956(75)90041-6) identifies a graph class on which this relaxation is exact for the all-ones objective, with an integral certificate on the dual side: the series-parallel networks. The paper conjectures (Conjecture 7.3) that for these graphs the odd-cycle inequalities describe the whole stable set polytope; graphs with that property were later called t-perfect.

Timeline:

• 1960: G. A. Dirac, in "In abstrakten Graphen vorhandene vollständige 4-Graphen und ihre Unterteilungen" (Math. Nachr. 22), proves that graphs containing no subdivided $K_4$ have at least two vertices of degree at most two.
• 1975: Chvátal introduces the system (7.1) and proves Theorem 7.1 (this mission): on series-parallel networks, $\max\sum_u x_u$ subject to (7.1) and its dual both have zero–one optima. He conjectures the full polyhedral statement.
• 1979: M. Boulala and J.-P. Uhry, "Polytope des indépendants d'un graphe série-parallèle" (Discrete Math. 27), prove the conjecture: (7.1) defines the stable set polytope of every series-parallel graph.
• 1986: A. M. H. Gerards and A. Schrijver, "Matrices with the Edmonds–Johnson property" (Combinatorica 6), extend this to graphs with no odd-$K_4$ subdivision.

Setting

All graphs $G=(V,E)$ are finite, undirected and loopless, with no parallel edges. A stable set is a set of vertices no two of which are adjacent. We write $d(u)$ for the degree of $u$.

A set $C\subseteq V$ induces an odd circuit if the induced subgraph $G[C]$ is a cycle of length $2k+1$ with $k\ge1$; triangles count, and such a cycle has no chords. $Z(G)$ is the set of all such $C$. The odd-cycle system of $G$ is

$$\begin{aligned} 0\le x_u&\le 1 && (u\in V),\\ x_v+x_w&\le 1 && (vw\in E),\\ \textstyle\sum_{u\in C}x_u&\le \tfrac12(|C|-1) && (C\in Z(G)). \end{aligned}\tag{7.1}$$

Its linear programming dual for the objective $\sum_u x_u$, with $x\ge0$ read as sign constraints, has variables $y_u\ge0$, $z_e\ge0$, $w_C\ge0$ and reads

$$\min\ \sum_{u}y_u+\sum_{e}z_e+\sum_{C\in Z(G)}\tfrac12(|C|-1)\,w_C\quad\text{s.t.}\quad y_u+\sum_{e\ni u}z_e+\sum_{C\ni u}w_C\ge 1\ \ (u\in V).$$

A homeomorph of $K_4$ is a graph obtained from $K_4$ by subdividing its edges into paths through new vertices of degree two. $G$ is a series-parallel network if no subgraph of $G$ is a homeomorph of $K_4$.

Formalization targets

Goal: Theorem 7.1

For every series-parallel network $G$,

$$\exists\,x\in\{0,1\}^V\ \text{feasible for (7.1)}:\ \ \sum_u x_u=\max\Big\{\sum_u x'_u : x'\in\mathbb R^V\text{ satisfies (7.1)}\Big\},$$

and there is a zero–one dual feasible $(y,z,w)$ whose dual objective equals the minimum over all real dual feasible points. Both optimality claims are against real points. Chvátal's statement has no constants to improve; the formal goal is his theorem as printed.

Milestones

1. Dirac's theorem (§7, p. 150): a series-parallel network with at least two vertices has two distinct vertices of degree at most two.
2. Case 4 closure (p. 151): if $d(u)=2$ and the neighbours $v,w$ of $u$ are non-adjacent, deleting $u$ and identifying $v$ with $w$ yields a series-parallel network.
3. The combinatorial core (p. 151, (i)–(ii)): there are a stable set $S$ and a spanning subgraph $F\le G$ whose components are isolated vertices, isolated edges and odd circuits, such that with $a$ isolated vertices, $b$ isolated edges and $c_k$ circuits of length $2k+1$,

$$a+b+\sum_k k\,c_k=|S|.$$

Significance

The result. Theorem 7.1 says that on series-parallel networks the odd-cycle relaxation computes $\alpha(G)$ exactly, and that the optimum is certified by a covering of the vertex set by single vertices, edges and chordless odd circuits whose total weight equals $|S|$. This is a min–max theorem of König type for a non-bipartite, non-perfect class: odd cycles of length at least five are series-parallel and not perfect, so the clique inequalities of the perfect-graph theory (mission I of this series) do not suffice here. The statement is the unweighted case of the later polyhedral results of Boulala–Uhry and Gerards–Schrijver, and the combinatorial core (milestone 3) is the basis of a polynomial algorithm for $\alpha(G)$ on this class, as the paper remarks.

Formalizing it. The theorem has been proved since 1975; neither Mathlib nor the Prove2Me library contains a formal proof of it. A formal proof needs a working notion of graph subdivision (topological minor), which Mathlib does not have, Dirac's degree theorem, the induction of the paper with its four cases, and the passage from the combinatorial core to a pair of LP optima through weak duality. Each of these is reusable: topological minors and the $K_4$-subdivision-free class appear throughout structural graph theory.

Difficulty

The combinatorial core is proved by induction on $|V|$ removing a vertex of degree at most two, and three of the four cases are routine. The obstacle is Case 4 ($d(u)=2$, neighbours non-adjacent): deleting $u$ alone loses the information needed to recover $S$ and $F$, so the proof identifies the two neighbours. That requires the class to be closed under this identification, a statement about subdivisions that is not a local edge count, and a lifting of $(S',F')$ from the reduced graph with a case split on the component of $F'$ containing the merged vertex. A second gap is between $F$ and the dual: an odd-circuit component of $F$ may have chords in $G$ and so need not lie in $Z(G)$, and the zero–one dual solution must be extracted from it. Finally, Dirac's theorem itself is the one place where the absence of $K_4$ subdivisions is used positively, and it is not a consequence of a degree-counting argument.

Formalization scope

Graphs are SimpleGraph V on a Fintype V with decidable equality and decidable adjacency. $Z(G)$ is a Finset (Finset V) whose members induce a subgraph isomorphic to Mathlib's cycleGraph (2k+1), $k\ge1$. The dual variables are indexed by V, by the edge set G.edgeSet, and by the subtype of $Z(G)$; $x\ge0$ is a sign constraint with no dual variable. "Contains a homeomorph of $K_4$" is encoded by four distinct branch vertices and six paths (Walk.IsPath) that avoid other branch vertices and meet only at common endpoints; it is not the $K_4$-minor notion and not the series–parallel composition notion, whose equivalence with it is not part of the paper.

Conventions and implicit hypotheses made explicit:

• Dirac's theorem is stated with $|V|\ge 2$; as printed it fails for graphs with fewer than two vertices.
• In Case 4 the identified graph has vertex set $V\setminus\{u,w\}$, with $v$ representing $v\equiv w$; parallel edges merge.
• Optimality in the goal is against every real feasible point of each program. A statement comparing the zero–one points only with other zero–one points would reduce the primal half to $\alpha(G)\le\alpha(G)$ and is ruled out.
• In milestone 3 the sum $a+b+\sum_k k c_k$ is written as a sum over the connected components of $F$ of $1$ (one or two vertices) or $(n-1)/2$ ($n\ge3$ vertices).

Corollary 7.2 (stated without proof) and Conjecture 7.3 are not part of this mission. Contributions welcome: a general topological-minor library, Dirac's theorem, and a proof of the combinatorial core.

Selected references

• V. Chvátal, On certain polytopes associated with graphs, J. Combin. Theory Ser. B 18 (1975) 138–154. https://doi.org/10.1016/0095-8956(75)90041-6
• G. A. Dirac, In abstrakten Graphen vorhandene vollständige 4-Graphen und ihre Unterteilungen, Math. Nachr. 22 (1960) 61–85 (reference [6], Satz 5, of the paper).
• R. J. Duffin, Topology of series-parallel networks, J. Math. Anal. Appl. 10 (1965) 303–318 (reference [7] of the paper).
• M. Boulala, J.-P. Uhry, Polytope des indépendants d'un graphe série-parallèle, Discrete Math. 27 (1979) 225–243.
• A. M. H. Gerards, A. Schrijver, Matrices with the Edmonds–Johnson property, Combinatorica 6 (1986) 365–379.

Motivation

The combinatorial diameter of a polyhedron is the largest distance, in its vertex-edge graph, between two vertices. It is a lower bound on the number of pivots any edge-following method such as the simplex method needs in the worst case, which is why the polynomial Hirsch conjecture — the diameter of $P = \{x \in \mathbb{R}^n : Ax \le b\}$ is bounded by a polynomial in $m$ and $n$ — is a central open question of linear optimization and discrete geometry. The best general upper bound is quasi-polynomial, $m^{1+\log n}$ (Kalai–Kleitman 1992); the original Hirsch bound $m - n$ is false for polytopes (Santos 2012).

A different line of work bounds the diameter by the arithmetic of the constraint matrix instead of its size. For an integer matrix $A$ let $\Delta$ be the largest absolute value of a sub-determinant of $A$. Dyer and Frieze (1994) showed that for totally unimodular $A$ ($\Delta = 1$) the diameter is polynomial, $O(m^{16} n^3 (\log mn)^3)$. Bonifas, Di Summa, Eisenbrand, Hähnle and Niemeier (SoCG 2012; Discrete Comput Geom 52, 2014) improved and generalized this to $O(\Delta^2 n^4 \log n\Delta)$ for all polyhedra and $O(\Delta^2 n^{3.5} \log n\Delta)$ for polytopes, bounds that do not depend on the number $m$ of inequalities. This mission formalizes the polytope case.

Setting

Let $A \in \mathbb{Z}^{m\times n}$ with rows $a_1,\dots,a_m$, let $b \in \mathbb{R}^m$, and let $P = \{x \in \mathbb{R}^n : Ax \le b\}$. A vertex of $P$ is an extreme point; for a polyhedron this is a point of $P$ at which $n$ linearly independent inequalities are tight. Two vertices $u \ne v$ are adjacent if the segment $[u,v]$ is an edge (a one-dimensional face) of $P$. This gives the polyhedral graph $G_P = (V, E)$, and the diameter of $P$ is at most $B$ if every two vertices are joined by a walk of at most $B$ edges.

$A$ has sub-determinants bounded by $\Delta$ if every $k\times k$ submatrix, for every $k \ge 1$, has determinant in $[-\Delta, \Delta]$. In particular every entry is at most $\Delta$ in absolute value.

For a vertex $v$ the normal cone $C_v$ is the set of objectives $c$ for which $v$ maximizes $c^T x$ over $P$. With $B_n$ the closed unit ball, the volume of a set $U \subseteq V$ of vertices is

$$\mathrm{vol}(U) = \mathrm{vol}\Big(\bigcup_{v\in U} C_v \cap B_n\Big),$$

and the neighbourhood $\mathcal N(I)$ of $I \subseteq V$ is the set of vertices outside $I$ adjacent to a vertex of $I$. A spherical cone is $S = C \cap B_n$ with $C$ closed under non-negative scaling; its dockable surface $D(S)$ is the $(n-1)$-dimensional measure of the part of its boundary inside the open ball. A cone of revolution of angle $0<\theta\le\pi/2$ is $\{x \in B_n : v^T x \ge \cos\theta\,\|v\|\,\|x\|\}$. $P$ is non-degenerate if every vertex has exactly $n$ tight inequalities.

Formalization targets

Goal: Theorem 2 (p. 105)

If $A \in \mathbb{Z}^{m\times n}$ has all sub-determinants bounded by $\Delta$ and $P$ is bounded, then

$$\operatorname{diam}(P) \le 2\Big\lfloor \sqrt{2\pi}\,\Delta^2 n^{5/2}\ln\!\big(2^n\, n!\, n^{n/2}\,\Delta^n\big)\Big\rfloor + 2 \;=\; O(\Delta^2 n^{3.5}\log n\Delta).$$

No non-degeneracy, full-dimensionality or rank condition is assumed, and the bound is uniform in $m$ and $b$.

Milestones

1. Lemma 3 (p. 108): for a vertex $v$ of a non-degenerate polytope, $D(S_v) \le \Delta^2 n^3\,\mathrm{vol}(S_v)$, where $S_v = C_v \cap B_n$.
2. Lemma 4 (p. 109): among spherical cones of a given volume, a cone of revolution has minimum dockable surface.
3. Lemma 5 (p. 110): for a cone of revolution, $D(S) \ge \sqrt{2n/\pi}\,\mathrm{vol}(S)$.
4. Lemma 6 (p. 111): for every measurable spherical cone with $\mathrm{vol}(S) \le \frac12 \mathrm{vol}(B_n)$, $D(S) \ge \sqrt{2n/\pi}\,\mathrm{vol}(S)$.
5. Lemma 1 (p. 105): for a non-degenerate polytope and $I \subseteq V$ with $\mathrm{vol}(I) \le \frac12\mathrm{vol}(B_n)$,

$$\mathrm{vol}(\mathcal N(I)) \ge \sqrt{\tfrac{2}{\pi}}\,\frac{1}{\Delta^2 n^{2.5}}\,\mathrm{vol}(I).$$

6. Eq. (1) (p. 105): if $I_j$ is the set of vertices at graph distance at most $j$ from a vertex $v$ and $\mathrm{vol}(I_j) \le \frac12\mathrm{vol}(B_n)$, then $j \le \sqrt{2\pi}\,\Delta^2 n^{2.5}\ln(2^n/\mathrm{vol}(I_0))$.

Significance

The result. Theorem 2 bounds the diameter of every integral polytope by a polynomial in the dimension and the largest sub-determinant, independently of the number of facets. For totally unimodular matrices, which cover network-flow, bipartite matching and transportation polytopes, it gives $O(n^{3.5}\log n)$, improving the Dyer–Frieze bound by a large polynomial factor. It shows that the obstruction to a polynomial Hirsch bound, if any, must come from matrices with large sub-determinants. The volume-expansion method — measuring breadth-first search by the volume of the normal fan it has covered — was later refined, for instance in the shadow-vertex analysis of Dadush–Hähnle, which improves the dependence on $n$.

Formalizing it. The theorem is proved (2012/2014); no machine-checked proof is known. A formal development needs, on top of Mathlib, the normal fan of a polytope and its relation to the vertex-edge graph, a Hausdorff-measure calculus for cones (surface of a cone in terms of its base), Lévy's isoperimetric inequality on the sphere in a measure-theoretic form, and explicit Gamma-function estimates. Each of these is reusable well beyond this paper.

Difficulty

The combinatorial side is short; the geometry is not. Lemma 4 is the spherical isoperimetric inequality of Lévy, which Mathlib does not have in any form, and which the paper cites rather than proves; the relations between the volume of a spherical cone, the area of its base, its lateral surface and the length of the base's boundary (Eq. (3), "basic integration") are also absent. Lemma 3 depends on the structure of the normal cone of a vertex of a non-degenerate polytope (full-dimensional, simplicial, generated by rows of $A$), none of which is available for Mathlib's extreme points. Lemma 1 depends on the normal fan of a polytope: the normal cones have pairwise disjoint interiors, cover $\mathbb{R}^n$, and share a facet exactly when their vertices are adjacent. The step from non-degenerate to arbitrary polytopes perturbs $b$ and needs the diameter not to decrease, a statement about the vertex-edge graph under perturbation. A shortcut through a finite graph abstraction is not available: the constant depends on the geometry of the normal cones, not only on the graph.

Formalization scope

The polyhedron is Hirsch.Hpoly (rowVec A) b, with rowVec A i the $i$-th row of $A \in$ Matrix (Fin m) (Fin n) ℤ as a vector of EuclideanSpace ℝ (Fin n). Vertices are Set.extremePoints ℝ P, adjacency is Hirsch.Adj, "diameter at most $B$" is Hirsch.DiamLE P B, all from the published Hirsch_model. The normal cone is the published FirstOrderOpt.ConvexTheory.normalCone. Volumes are Lebesgue measure with values in $[0,\infty]$; the dockable surface uses μHE[n-1], the Hausdorff measure normalized to agree with Lebesgue measure on hyperplanes, applied to frontier S ∩ Metric.ball 0 1. $\Delta$ is a natural number and the sub-determinant bound ranges over all sizes $k \ge 1$.

Explicit constants. The paper writes $O(\Delta^2 n^{3.5}\log n\Delta)$ in Theorem 2; the proof on pp. 105–106 yields $2\lfloor K\rfloor + 2$ with $K = \sqrt{2\pi}\,\Delta^2 n^{5/2}\ln(2^n n!\, n^{n/2}\Delta^n)$, from Eq. (1), the bound $\mathrm{vol}(I_0) \ge 1/(n!\,n^{n/2}\Delta^n)$ and the fact that the diameter is at most twice the number of breadth-first-search iterations needed to cover more than half of $B_n$. This explicit bound is the goal. The ratios $D/\mathrm{vol}$ of Lemmas 3, 5, 6 are stated in multiplicative form.

Non-degeneracy is a hypothesis of Lemma 3, Lemma 1 and Eq. (1) only, as in the paper's §1.1, and never of Theorem 2. The neighbourhood $\mathcal N(I)$ excludes $I$; including it would make Lemma 1 trivial, since its constant is below $1$. Lemma 4 is stated against every competitor: for every measurable spherical cone $S$ and every cone of revolution $S^*$ of the same volume, $D(S^*) \le D(S)$; it does not assert existence of a cone of a prescribed volume. The goal is Theorem 2 about the polytope and its graph, not an abstract statement about set families with a volume-expansion property; integrality of $A$ and the bound on minors of every size are both essential (scaling a real matrix down makes $\Delta$ arbitrarily small), and the raw Hausdorff measure μH[n-1] would put Lemmas 3 and 6 on incompatible scales.

Contributions are welcome at every level: the normal fan and its adjacency structure, cone surface formulas, the Gamma estimate $\Gamma(x+\frac12)/\Gamma(x) \ge \sqrt{x-\frac14}$, and a formal Lévy inequality.

Selected references

• N. Bonifas, M. Di Summa, F. Eisenbrand, N. Hähnle, M. Niemeier, On Sub-determinants and the Diameter of Polyhedra, Discrete Comput Geom 52 (2014) 102–115. https://doi.org/10.1007/s00454-014-9601-x
• M. Dyer, A. Frieze, Random walks, totally unimodular matrices, and a randomised dual simplex algorithm, Math. Program. 64 (1994) 1–16. https://doi.org/10.1007/BF01582563
• G. Kalai, D. J. Kleitman, A quasi-polynomial bound for the diameter of graphs of polyhedra, Bull. Amer. Math. Soc. 26 (1992) 315–316. https://doi.org/10.1090/S0273-0979-1992-00285-9
• F. Santos, A counterexample to the Hirsch conjecture, Annals of Math. 176 (2012) 383–412. https://doi.org/10.4007/annals.2012.176.1.7
• T. Figiel, J. Lindenstrauss, V. Milman, The dimension of almost spherical sections of convex bodies, Acta Math. 139 (1977) 53–94 (Lévy's isoperimetric inequality, Theorem 2.1). https://doi.org/10.1007/BF02392234
• D. Dadush, N. Hähnle, On the shadow simplex method for curved polyhedra, Discrete Comput Geom 56 (2016). https://arxiv.org/abs/1412.6705