Combinatorics

Why the number of augmentations matters

The maximum flow problem asks how much of a commodity can be sent from a source to a sink through a network whose arcs have capacities. It is a basic model in operations research, underlies bipartite matching, transportation and scheduling problems, and is a standard subroutine inside larger combinatorial algorithms.

The classical method for it is the labeling method of Ford and Fulkerson: starting from some flow, repeatedly find an augmenting path from source to sink along which flow can be increased, push as much as the path allows, and stop when no such path exists. When all capacities are integers, each augmentation raises the flow value by at least one, so the method terminates, but the number of augmentations can be as large as the final flow value, which is exponential in the size of the input. Edmonds and Karp give a four-node example in which the method alternates between two paths and needs $2M$ augmentations for capacities $M$ (Edmonds–Karp 1972, p. 250). With irrational capacities, Ford and Fulkerson showed that the method need not terminate at all and may converge to a non-maximum flow.

Timeline.

• 1956 — Ford and Fulkerson introduce the labeling method and the max-flow min-cut theorem (Ford–Fulkerson 1956).
• 1962 — Flows in Networks records the non-termination example for incommensurable capacities.
• 1970 — Dinic independently obtains a polynomial bound using layered (shortest-path) networks (Dinic 1970).
• 1972 — Edmonds and Karp prove that choosing each augmenting path with fewest arcs bounds the number of augmentations by $\tfrac14(n^3-n)$, for arbitrary real capacities (Edmonds–Karp 1972, Theorem 1).

Setting

A network $N$ consists of a finite set of $n$ nodes, a source $s$ and a sink $t \ne s$, and a set of arcs, which are ordered pairs $(u,v)$ with $u \ne v$; there is at most one arc from a node to another. One arc is the special return arc $(t,s)$, and $A$ denotes the set of all other arcs. Each $(u,v) \in A$ has a real capacity $c(u,v) > 0$.

A flow is a nonnegative function $f$ on the arcs of $N$ with $f(u,v) \le c(u,v)$ on $A$ and with inflow equal to outflow at every node, the return arc included. The value $f(t,s)$ is the amount sent from $s$ to $t$; a maximum flow maximizes it.

Given a flow $f$, the residual network $N^f$ has the same nodes, and $(u,v)$ is an arc of $N^f$ when $(u,v) \in A$ with $c(u,v) - f(u,v) > 0$, or $(v,u) \in A$ with $f(v,u) > 0$. An augmenting path is a sequence of distinct nodes $s = u_1, \dots, u_p = t$ whose consecutive pairs are arcs of $N^f$. Each step carries a number $\varepsilon_i > 0$ (residual capacity forward, flow backward, or their sum when both $(u_i,u_{i+1})$ and $(u_{i+1},u_i)$ lie in $A$); $\varepsilon = \min_i \varepsilon_i$, and a step with $\varepsilon_i = \varepsilon$ is a bottleneck arc. Augmenting raises $f(t,s)$ by $\varepsilon$ and shifts the flow on the path's arcs accordingly, using the paper's own rule for opposite arcs, which never exceeds a capacity.

A run with fewest-arc augmentations is a sequence $f^0, \dots, f^K$ where $f^0$ is a flow and each $f^{k+1}$ arises from $f^k$ by augmenting along a path $P^k$ with fewest arcs. The distance $\delta^k(u,v)$ is the least number of arcs of a directed path from $u$ to $v$ in $N^k = N^{f^k}$, or $\infty$.

Formalization targets

Goal — Theorem 1

For every network on $n$ nodes and every run of length $K$ with fewest-arc augmentations,

$$K \le \tfrac14\,(n^3 - n),$$

and if no augmenting path exists relative to $f^K$, then $f^K$ is a maximum flow. The capacities are arbitrary positive reals, and the initial flow is arbitrary.

Milestones

1. §1.1: augmentation yields a flow with value $f(t,s) + \varepsilon$, $\varepsilon > 0$.
2. §1.1: a flow is maximum if and only if it admits no augmenting path.
3. Proposition 1: a bottleneck arc of $P^k$ is not an arc of $N^{k+1}$.
4. Proposition 2: $(u,v) \in N^{k+1}$ implies $(u,v) \in N^k$ or $(v,u) \in P^k$.
5. Lemma 1: if $(u,v)$ is a bottleneck arc at steps $k < m$, then $(v,u) \in P^l$ for some $k < l < m$.
6. Proposition 3: $\delta^k(s,u) \le \delta^{k+1}(s,u)$ and $\delta^k(u,t) \le \delta^{k+1}(u,t)$.
7. Lemma 2: if $k < l$, $(u,v) \in P^k$ and $(v,u) \in P^l$, then $\delta^l(s,t) \ge \delta^k(s,t) + 2$.
8. Proof of Theorem 1: each pair $\{u,v\}$ occurs as a bottleneck at most $\tfrac12(n+1)$ times.

Significance

The theorem shows that one simple rule for choosing augmenting paths, which a breadth-first labeling process implements, makes the number of augmentations depend on the number of nodes alone, independent of the capacities and of their arithmetic nature. It removes both pathologies of the unrestricted labeling method at once: exponential running time for integer capacities, and non-termination for irrational ones. Together with Dinic's work it is the starting point of the theory of strongly polynomial network-flow algorithms, and the distance-monotonicity argument (Proposition 3, Lemma 2) reappears in blocking-flow and push-relabel analyses.

The result is classical and fully proved in the paper. What this mission adds is a machine-checked version of the complete argument in the paper's own model: return arc, arbitrary real capacities, and the paper's augmentation rule for pairs of opposite arcs, which differs from Ford and Fulkerson's (footnote 1, p. 249). The platform has a max-flow min-cut theorem and an integer termination theorem for the Ford–Fulkerson method in the Bertsimas–Tsitsiklis model (Introduction to Linear Optimization, missions IX–X), but no bound on the number of augmentations. No machine-checked proof of Theorem 1 in Lean is known to exist.

Difficulty

The obvious argument, "each augmentation saturates a bottleneck arc, which then disappears", fails because a saturated arc can reappear after later augmentations push flow back along its reverse. Counting augmentations therefore requires control over how often the same pair of nodes can supply a bottleneck again, and no property of a single augmentation provides it; the bound has to come from an invariant of the whole run that holds for real capacities, where no integrality argument is available. A second trap is that the converse direction of milestone 2 (no augmenting path implies maximality) is a max-flow min-cut statement that the paper cites without proof; it must be proved in the paper's model with the return arc.

Formalization scope

Nodes form a finite type V with decidable equality and $n$ = Fintype.card V counts all nodes, $s$ and $t$ included. The arc set A is a Finset (V × V) with no loops and without $(t,s)$; capacities are real and positive on A. A flow is a function V → V → ℝ whose values off the arcs are ignored. A maximum flow is the predicate "$f(t,s) \ge g(t,s)$ for every flow $g$", never a real supremum. Paths are lists of distinct nodes with every consecutive pair a residual arc, so the return arc is never on a path. Distances take values in ℕ∞. A run is a pair of ℕ-indexed sequences constrained on indices up to $K$. The explicit constants are stated as printed: $4K \le n^3 - n$ in ℕ (the truncated subtraction is harmless since $n \le n^3$) and $2\,b(u,v) \le n + 1$ for the per-pair count.

Case (b) of the paper's definition of augmenting paths is misprinted (its hypothesis repeats that of Case (c)); the formalization uses the reading $(u_i,u_{i+1}) \notin A$, $(u_{i+1},u_i) \in A$, which the paper's own description of $N^f$ on p. 251 confirms.

A trivializing formalization is ruled out: a run predicate that no sequence satisfies (for instance, one that requires paths through the return arc, or computes $\varepsilon = 0$) would make the bound vacuous; the step predicate here is satisfiable, and a concrete four-node run has been checked. Replacing the paper's augmentation rule by "increase the forward arc by $\varepsilon$" would also change the theorem, because that rule can violate capacities.

A complete development needs basic facts on simple paths in finite digraphs, shortest paths and their subpaths, and a max-flow min-cut theorem in the paper's model. These are reusable well beyond this mission, as are the network, residual-network and augmentation definitions. Contributions proving any milestone independently are welcome.

Selected references

• J. Edmonds, R. M. Karp, Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems, Journal of the ACM 19(2):248–264, 1972. https://doi.org/10.1145/321694.321699
• L. R. Ford, D. R. Fulkerson, Maximal Flow Through a Network, Canadian Journal of Mathematics 8:399–404, 1956. https://doi.org/10.4153/CJM-1956-045-5
• L. R. Ford, D. R. Fulkerson, Flows in Networks, Princeton University Press, 1962. https://doi.org/10.1515/9781400875184
• E. A. Dinic, Algorithm for Solution of a Problem of Maximum Flow in a Network with Power Estimation, Soviet Mathematics Doklady 11:1277–1280, 1970. https://www.cs.bgu.ac.il/~dinitz/D70.pdf
• D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Chapter 7 (network flow problems; formalized on the platform in missions IX–X).

Motivation

The traveling salesman problem asks for a shortest closed route visiting every node of a weighted complete graph exactly once. It is NP-hard, so practitioners use fast heuristics, and the basic question about a heuristic is how far from optimal its tour can be. Rosenkrantz, Stearns and Lewis (SIAM J. Comput. 6(3), 1977) gave the first systematic worst-case analysis of the simple constructive heuristics under the triangle inequality: nearest neighbor, the family of insertion methods, and several variants.

Insertion methods build a tour by growing it one node at a time. They are among the most widely used construction heuristics in practice and in textbooks, and they differ only in the rule that chooses which node to insert next: the nearest one, the cheapest one, the farthest one, a random one, or any other. This mission formalizes the paper's result that holds for the whole family at once, regardless of that rule: every insertion method produces a tour at most $\lceil \lg n\rceil + 1$ times longer than an optimal one (Theorem 3, p. 571).

Timeline. 1977: Rosenkrantz, Stearns and Lewis prove $\lceil\lg n\rceil+1$ for every insertion method (Theorem 3), $\tfrac12(\lceil\lg n\rceil+1)$ for nearest neighbor (Theorem 1), both from a shared counting lemma (Lemma 1), and the constant $2$ for nearest and cheapest insertion (Theorem 4). 1994: Bafna, Kalyanasundaram and Pruhs (Theoretical Computer Science 125, 1994) give instances on which some insertion methods reach ratio $\Omega(\log n/\log\log n)$, so the logarithmic growth cannot be replaced by a constant for the family as a whole.

Setting

A traveling salesman graph with $n$ nodes consists of a finite node set $N$ with $|N|=n$ and a distance $d:N\times N\to\mathbb R$ with $d(i,j)=d(j,i)$, $d(i,j)\ge 0$ and $d(i,j)+d(j,k)\ge d(i,k)$ for all nodes (the triangle inequality). A tour visits every node once and returns to its start; its length is the sum of its edge lengths, and OPTIMAL is the least length of a tour.

A subtour is a tour on a subset of the nodes; a single node is a tour without edges. Given a subtour $T$ and a node $k\notin T$, TOUR$(T,k)$ is obtained by choosing an edge $(x,y)$ of $T$ minimizing

$$d(x,k)+d(k,y)-d(x,y)$$

and replacing it by the edges $(x,k)$ and $(k,y)$; if $T$ is a single node $i$, TOUR$(T,k)$ is the two-node tour $(i,k),(k,i)$. COST$(T,k)$ is the length of TOUR$(T,k)$ minus the length of $T$.

An insertion method constructs subtours $T_1,\dots,T_n$ with $T_1=\{a_0\}$ a single node and $T_{i+1}=\mathrm{TOUR}(T_i,a_i)$ for some node $a_i\notin T_i$, $1\le i<n$. The final tour $T_n$ is the approximation, and INSERT denotes its length. No rule for choosing the $a_i$ is fixed, and ties between minimizing edges are broken arbitrarily.

Write $\lg$ for the logarithm to base 2 and $\lceil x\rceil$ for the least integer $\ge x$.

Formalization targets

Goal: Theorem 3

For every traveling salesman graph with $n\ge 1$ nodes and every run of every insertion method,

$$\mathrm{INSERT}\ \le\ \bigl(\lceil\lg n\rceil+1\bigr)\cdot\mathrm{OPTIMAL}.$$

Milestones

1. (2.2), shortcutting: visiting a subset of the nodes in the order of a tour gives a tour of the subset that is no longer.
2. (2.1): if the numbers $l_1\ge\dots\ge l_n$ satisfy $d(p,q)\ge\min(l_p,l_q)$ for distinct $p,q$, then $\mathrm{OPTIMAL}\ge 2\sum_{i=k+1}^{\min(2k,n)} l_i$ for $1\le k\le n$.
3. Lemma 1: if $d(p,q)\ge\min(l_p,l_q)$ for distinct nodes and $l_p\le\frac12\mathrm{OPTIMAL}$ for all $p$, then

$$\sum_p l_p\le\tfrac12\bigl(\lceil\lg n\rceil+1\bigr)\mathrm{OPTIMAL}.$$

4. Lemma 2: $\mathrm{COST}(T,k)\le 2\,d(k,j)$ for every node $j$ of $T$.
5. (3.7): $\mathrm{INSERT}=\sum_{i=1}^{n-1}\mathrm{COST}(T_i,a_i)$.
6. (3.10): $\mathrm{COST}(T_i,a_i)\le 2\,d(a_i,a_j)$ whenever $j<i$.
7. (3.12): $\mathrm{COST}(T_i,a_i)\le\mathrm{OPTIMAL}$ for $1\le i<n$.

Significance

The result. Theorem 3 is a guarantee for an entire class of algorithms rather than for one. Any rule for choosing the next node, including rules designed for speed or for empirical quality, inherits a worst-case ratio of $\lceil\lg n\rceil+1$ from the insertion step alone. The rule matters only for improving on that: nearest and cheapest insertion achieve the constant $2(1-1/n)$ (Theorem 4 and its corollary, the subject of the third mission of this series), while the logarithmic bound remains the best general statement for other rules, such as farthest or arbitrary insertion. Lemma 1 is reusable on its own: it converts "every node carries a charge bounded by half the optimum and by its distance to other nodes" into a logarithmic bound, and the same lemma yields the nearest neighbor bound of Theorem 1.

Formalizing it. The theorem has been proved since 1977; the work here is a machine-checked proof of the known argument together with a reusable library for subtours, insertion and insertion costs. The companion nearest neighbor bound (Theorem 1) is already on the platform as SupplyChainTheory.nearest_neighbor_bound (proved), and nearest insertion with constant 2 as SupplyChainTheory.nearest_insertion_bound; neither covers arbitrary insertion methods or states Lemma 1 separately.

Difficulty

The per-step facts are local: each insertion is cheap relative to a node already present (Lemma 2) and relative to OPTIMAL (3.12). The obvious way to combine them, adding up $n-1$ costs each at most OPTIMAL, gives only the ratio $n-1$. The logarithm comes from a global counting argument over all nodes simultaneously (Lemma 1), in which OPTIMAL is compared with tours on nested subsets of nodes of doubling size, and the per-node charges must be matched against the edges of those tours. Formally, the delicate parts are the bookkeeping of subtours as they grow (that every earlier node lies on the current subtour, and that the insertion cost equals the length increase), the shortcutting of a tour to an arbitrary subset, and the ceiling-of-logarithm arithmetic.

Formalization scope

Nodes are Fin n; a tour of all nodes is a permutation τ : Equiv.Perm (Fin n), and OPTIMAL is the minimum of the tour length over the finite, nonempty set of permutations. Subtours are duplicate-free lists of nodes, with closed length $d(x_0,x_1)+\dots+d(x_{m-1},x_0)$. TOUR$(T,k)$ is encoded as inserting $k$ at a list position whose resulting length is minimal among all positions; inserting at a position removes exactly one edge of $T$ and raises the length by exactly $d(x,k)+d(k,y)-d(x,y)$, so this is the paper's rule, with every tie-breaking allowed. COST is the minimum length increase over positions. The paper's 1-based subtour index is kept ($T_1=[a_0]$, $T_n$ final). $\lceil\lg n\rceil$ is Nat.clog 2 n. All quantities are real.

Conventions and deviations, each disclosed in the item statements:

• The distance satisfies $d(i,i)=0$, a normalization not in the paper; a loop never enters any length.
• Ratios are multiplied out ($\mathrm{INSERT}\le c\cdot\mathrm{OPTIMAL}$), so the paper's exclusion of the identically zero distance (1.1) is not needed.
• Condition a) of Lemma 1 is required for distinct nodes only. The page says "for all nodes $p$ and $q$", which for $p=q$ would force every $l_p\le 0$ and make the lemma inapplicable in the proof of Theorem 3; the proof uses the condition only on edges of a tour.
• (2.2) is stated for every subset of the nodes and every tour, which is what the shortcut argument shows; the paper applies it to one specific subset and an optimal tour.
• (2.1) uses 0-based node labels, so its range $k+1,\dots,\min(2k,n)$ becomes $k,\dots,\min(2k,n)-1$.

The goal quantifies over every run: any choice of the inserted nodes $a_i$ and any minimizing insertion position. Adding a selection rule (nearest, cheapest) or fixing a tie-breaking would state a weaker, different theorem; restricting to instances with OPTIMAL $=0$ or to a fixed small $n$ would trivialize it.

Reusable beyond this mission: the subtour and insertion library (closed length of a list, TOUR, COST, insertion runs) and Lemma 1, which also yields Theorem 1. Contributions welcome: proofs of the milestones, general lemmas about the closed length of List.insertIdx and of filtered lists, and a proof of Theorem 1 from this mission's Lemma 1.

Selected references

• D. J. Rosenkrantz, R. E. Stearns, P. M. Lewis II, An Analysis of Several Heuristics for the Traveling Salesman Problem, SIAM Journal on Computing 6(3):563–581, 1977. https://doi.org/10.1137/0206041
• V. Bafna, B. Kalyanasundaram, K. Pruhs, Not all insertion methods yield constant approximate tours in the Euclidean plane, Theoretical Computer Science 125(2):345–353, 1994.

Motivation

The edit distance between two strings is the least total cost of a sequence of single-character insertions, deletions and replacements turning one string into the other. It is the basic similarity measure of spelling correction, file comparison and biological sequence alignment. Wagner and Fischer (JACM 1974) showed that it can be computed by filling a $(|A|+1) \times (|B|+1)$ matrix in $O(|A|\cdot|B|)$ time. Masek and Paterson (J. Comput. System Sci. 1980) gave the first asymptotic improvement: for a finite alphabet and edit costs that are integral multiples of a common constant, the edit distance can be computed in time $O(|A|\cdot|B|/\max(1, |B|/\log|A|))$, that is $O(n^2/\log n)$ for two strings of length $n$.

Timeline:

• 1970: Arlazarov, Dinic, Kronrod and Faradzev compute transitive closures by precomputing all small submatrices, the "four Russians" technique that Masek and Paterson adapt.
• 1974: Wagner and Fischer give the matrix-filling algorithm, with the first row and column of the matrix and the three-term recurrence for its interior (Theorems 1 and 2 of Masek–Paterson, cited from them).
• 1980: Masek and Paterson apply the four-Russians technique to the edit matrix, working with differences of adjacent entries, and show that the restriction to discrete costs cannot simply be dropped (their Section 4, the subject of the second mission of this series).
• 2015: Backurs and Indyk (arXiv:1412.0348) show that a strongly subquadratic algorithm would refute the Strong Exponential Time Hypothesis, so a logarithmic-factor speed-up of this kind is close to the best one can expect.

Setting

Let $\Sigma$ be an alphabet and $\lambda$ the null string. For a string $A$, $|A|$ is its length, $A_n$ its $n$-th character, $A^{i,j} = A_i \cdots A_j$ and $A^i = A^{1,i}$, with $A^0 = \lambda$.

An edit operation $a \to b$ is a pair $(a, b) \ne (\lambda, \lambda)$ of strings of length at most one: a replacement ($a, b \ne \lambda$, possibly $a = b$), a deletion ($b = \lambda$) or an insertion ($a = \lambda$). $B$ results from $A$ via $a \to b$ if $A = \sigma a \tau$ and $B = \sigma b \tau$. An edit sequence $S = s_1, \dots, s_m$ takes $A$ to $B$ if there are strings $A = C_0, C_1, \dots, C_m = B$ with $C_{i-1} \to C_i$ via $s_i$. A cost function $\gamma$ assigns a nonnegative real to every edit operation, $\gamma(S) = \sum_i \gamma(s_i)$, and

$$\delta(\gamma, A, B) = \min\{\gamma(S) \mid S \text{ takes } A \text{ to } B\}.$$

Write $R_{a,b} = \gamma(a \to b)$, $D_a = \gamma(a \to \lambda)$, $I_a = \gamma(\lambda \to a)$, and $\delta_{i,j} = \delta(\gamma, A^i, B^j)$ for the entries of the edit matrix. The cost function is normalized if $\gamma(a \to b) = \delta(\gamma, a, b)$ for every edit operation.

A step is a difference of two adjacent matrix entries, $\delta_{i,j} - \delta_{i-1,j}$ (vertical) or $\delta_{i,j} - \delta_{i,j-1}$ (horizontal). The cost set is $\Omega = \{D_a\} \cup \{I_a\} \cup \{R_{a,b}\}$, and $\Omega$ is discrete if every element of $\Omega$ is an integral multiple of one constant $r > 0$.

Algorithm Y takes two strings $C, D$ of length $m$ and two step vectors $R, S$ of length $m$ (the left column and top row of an $m \times m$ block) and fills a matrix $T$ of vertical steps and $U$ of horizontal steps by the recurrence of Corollary 1, returning the right column $R'$ and bottom row $S'$. Algorithm Z cuts $A$ and $B$ into blocks of length $m$, starts from the deletion costs of $A$ and the insertion costs of $B$, obtains the steps of each block from Algorithm Y's output ("Fetch"), and returns the sum of the steps along the left column and the bottom row.

Formalization targets

Goal: correctness from a string-independent finite table

For a finite alphabet and a nonnegative, normalized cost function with discrete $\Omega$, there is a finite set $T \subset \mathbb{R}$ such that for all $m \ge 1$ and all $A, B$ with $m \mid |A|$, $m \mid |B|$,

$$\mathrm{cost}_{Z}(\gamma, m, A, B) = \delta(\gamma, A, B), \qquad \text{every entry of every } P(i,j), Q(i,j) \text{ lies in } T.$$

$T$ is fixed before $m$, $A$ and $B$. The second clause says that Algorithm Y's table need only range over $\Sigma^m \times \Sigma^m \times T^m \times T^m$, whose size does not depend on the strings; this is what the running-time bound rests on.

Milestones

1. Theorem 1 [Wagner–Fischer]: $\delta_{0,0} = 0$, $\delta_{i,0} = \sum_{r \le i} D_{A_r}$, $\delta_{0,j} = \sum_{r \le j} I_{B_r}$.
2. Theorem 2 [Wagner–Fischer]: $\delta_{i,j} = \min(\delta_{i-1,j-1} + R_{A_i,B_j}, \delta_{i-1,j} + D_{A_i}, \delta_{i,j-1} + I_{B_j})$.
3. Corollary 1: the same recurrence written in terms of steps.
4. Algorithm Y returns the final step vectors of every $m \times m$ submatrix from its initial step vectors and strings (Section 2.1).
5. Lemma 3: $-I \le \delta_{i,j} - \delta_{i-1,j} \le D$ and $-D \le \delta_{i,j} - \delta_{i,j-1} \le I$.
6. Lemma 4: if $\Omega$ is discrete, the set of possible steps is finite.

Significance

The result was the first algorithm for edit distance faster than quadratic, and its method (tabulate every possible small block of a dynamic program, described by differences rather than values) became the standard way of shaving a logarithmic factor from string dynamic programs. The discreteness hypothesis is where the method's power ends: Section 4 of the paper shows that with costs $1$ and $\pi$ the number of distinct steps grows without bound.

The results are proved in the paper; none of them is formalized. The Mathlib revision of this mission contains no edit-distance module. A formalization produces a definition of edit distance as a minimum over edit sequences, a machine-checked proof of the Wagner–Fischer recurrence for that definition under the normalization the paper assumes, and a checked proof that the four-Russians block assembly is correct and draws on a finite, string-independent table.

Difficulty

The hardest step is Theorem 2 for $\delta$ defined as a minimum over arbitrary edit sequences. An edit sequence may insert a character and later replace or delete it, or edit the same position many times, so the edit matrix's three-term recurrence does not follow by looking at the last operation. The upper bound is direct; the lower bound needs a normal form for edit sequences, and it fails without normalization: with $R_{a,c} = 10$, $R_{a,b} = R_{b,c} = 1$ and all insertions and deletions costing $100$, $\delta(\gamma, a, c) = 2$ while the recurrence gives $10$.

The goal is then an induction over blocks that must keep track of which matrix entries each block's input and output vectors represent, with block boundaries at multiples of $m$ and the first row and column handled by Theorem 1.

Formalization scope

Strings are List α; characters are 1-based in all statements, as in the paper ($A_i$ is A[i-1]). An edit operation is a structure with two Option α fields, not both none. $\delta$ is sInf of the set of costs of edit sequences taking $A$ to $B$ (nonempty, and bounded below for $\gamma \ge 0$). Costs are real-valued with an explicit nonnegativity hypothesis. Normalization is a hypothesis on Theorems 1, 2, Corollary 1, the Algorithm Y lemma and the goal; Lemmas 3 and 4 hold without it. The finite alphabet is [Fintype α] on Lemma 4 and the goal; Lemma 3 is stated for arbitrary upper bounds $I \ge I_a$, $D \ge D_a$, which implies the paper's version with maxima. The paper's standing assumption $|A| \ge |B|$ serves only the running time and is dropped. Step vectors are functions on Fin m.

Pinned statements. The paper states a running time $O(|A|\cdot|B|/\max(1,|B|/\log|A|))$ on a logarithmic-cost RAM; the goal formalizes the two facts that bound rests on, correctness and a finite table domain fixed before the strings. The RAM model, operation counts, the choice $m = \lfloor \log_k |A| \rfloor$, the padding reduction for $m \nmid |A|$, and the edit-path recovery of Section 2.3 are not formalized. Algorithm Y's result is a function (blockY); the Store/Fetch memory is not modelled.

The edit distance must stay the minimum over edit sequences: defining it by the Wagner–Fischer recurrence would make Theorems 1 and 2 true by definition and reduce the goal to a comparison of two recurrences. Algorithms Y and Z are transcribed from the pseudo-code and never refer to $\delta$.

Useful beyond this mission: the §1.1 definitions and Theorems 1–2 are a general edit-distance library (the second mission of this series defines the same objects). Contributions of lemmas about normal forms of edit sequences, the triangle inequality for $\delta$, and attainment of the minimum are welcome.

Selected references

• W. J. Masek, M. S. Paterson, A Faster Algorithm Computing String Edit Distances, J. Comput. System Sci. 20 (1980), 18–31. https://doi.org/10.1016/0022-0000(80)90002-1
• R. A. Wagner, M. J. Fischer, The String-to-String Correction Problem, J. ACM 21 (1974), 168–173. https://doi.org/10.1145/321796.321811
• V. L. Arlazarov, E. A. Dinic, M. A. Kronrod, I. A. Faradzev, On Economical Construction of the Transitive Closure of an Oriented Graph, Soviet Math. Dokl. 11 (1970), 1209–1210.
• A. Backurs, P. Indyk, Edit Distance Cannot Be Computed in Strongly Subquadratic Time (unless SETH is false), STOC 2015. https://arxiv.org/abs/1412.0348

Motivation

Many combinatorial optimization problems are linear programs over a polytope whose vertices are the zero–one incidence vectors of the feasible objects: matchings, stable sets, spanning trees. The edges of such a polytope (pairs of vertices joined by a one-dimensional face) govern the behaviour of the simplex method and of local-search procedures, which move from vertex to vertex along edges: a pivot of the simplex method on a nondegenerate basis replaces a vertex by one of its neighbours.

In December 1971 M. L. Balinski asked when two matchings $M_1, M_2$ of a graph are neighbours on the matching polyhedron determined by Edmonds (Edmonds 1965). V. Chvátal answered a more general question in §6 of On certain polytopes associated with graphs (Chvátal 1975): he characterized the neighbours on the stable set polytope of an arbitrary graph. Since matchings of $G$ are the stable sets of the line graph $L(G)$, Balinski's question is the special case of line graphs (Corollary 6.3 of the paper).

Setting

Let $G=(V,E)$ be a finite undirected loopless graph. A stable set is a set of vertices no two of which are adjacent. $S(G)$ denotes the set of all zero–one vectors $x=(x_u : u\in V)$ such that $\{u : x_u=1\}$ is stable, and the stable set polytope is

$$P(G)=\operatorname{conv} S(G)\subseteq \mathbb R^V .$$

For $y\in S(G)$ the corresponding stable set is $Y=\{u : y_u=1\}$.

For an integer-valued vector $c=(c_u : u\in V)$ write $cx=\sum_{u\in V}c_ux_u$. Two vectors $y, z$ are neighbours in $P(G)$ if there is an integer-valued $c$ such that $y$ and $z$ are the only two vectors which maximize $cx$ over $S(G)$; in particular $y\neq z$. This is the definition the paper states at the start of the proof of Theorem 6.2.

A bicoloration of a graph $T$ is a partition $V=B\cup R$, $B\cap R=\emptyset$, such that every edge joins $B$ to $R$. Every tree has one.

In the Lean development these objects are stableVectors G ($S(G)$), stablePolytope G ($P(G)$), onesSet y ($Y$), AreNeighbors G y z and IsBicoloration T B R, all in the namespace ChvatalPolytopes.Neighbors.

Formalization targets

Goal: Theorem 6.2 (p. 149)

For $y,z\in S(G)$ with corresponding stable sets $Y,Z$,

$$y \text{ and } z \text{ are neighbours in } P(G) \iff \text{the subgraph } H \text{ of } G \text{ induced by } (Y-Z)\cup(Z-Y) \text{ is connected.}$$

Milestone: Lemma 6.1 (p. 149)

For a tree $T=(V,E)$ with a bicoloration $V=B\cup R$ there are nonnegative integers $c_u$ ($u\in V$) and $m$ with

$$\sum_{u\in V}c_ux_u\le m\quad\text{for all } x\in S(T),$$

with equality exactly when $x$ is the incidence vector of $B$ or of $R$.

Milestone: the certificate of the "if" part (p. 149, proof of Theorem 6.2, (i))

If $H$ is connected with spanning tree $T$, and $c_u$ ($u\in (Y-Z)\cup(Z-Y)$), $m$ are as in Lemma 6.1 for $T$, extend $c$ by $c_u=1$ on $Y\cap Z$ and $c_u=-1$ outside $Y\cup Z$. Then

$$\sum_{u\in V}c_ux_u\le m+|Y\cap Z|\quad\text{for all } x\in S(G),$$

with equality if and only if $x=y$ or $x=z$.

Significance

Theorem 6.2 describes the 1-skeleton of the stable set polytope of every graph by a condition that can be checked in linear time, although optimizing over $P(G)$ is NP-hard in general and no complete linear description of $P(G)$ is known for general graphs. Through line graphs it gives the adjacency criterion for the matching polytope (two matchings are neighbours if and only if their symmetric difference is a single path or cycle), which settled Balinski's question. Characterizations of this type underlie the analysis of simplex-type and pivoting algorithms on combinatorial polytopes and the study of their diameters.

The result has been proved since 1975. The mission asks for a machine-checked proof of the theorem as stated in the paper; no formal proof of Theorem 6.2 or of the matching-polytope corollary is known to exist on Prove2Me or in Mathlib. The two milestones isolate the constructive half (Lemma 6.1 and the weighting built from it), which is reusable for any statement that needs an explicit objective singling out two stable sets.

Difficulty

The "only if" direction and the equality analysis are elementary; the substance lies in the "if" direction. An objective that makes both $y$ and $z$ optimal is easy to write down, for example $c=y+z$; the difficulty is to make them the only optimal vectors. Any stable set that agrees with $Y$ on some connected pieces of $H$ and with $Z$ on others ties with $y$ and $z$ under naive weightings, so the weights on $(Y-Z)\cup(Z-Y)$ must be chosen so that every mixed choice loses strictly. The integrality requirement on $c$ and the need to control all of $S(G)$, not only the stable sets contained in $Y\cup Z$, rule out a direct perturbation argument.

Formalization scope

• Graphs. $V$ is a finite type with decidable equality and $G$ is a SimpleGraph V; loops and multiple edges are excluded, as in the paper.
• $S(G)$ and $P(G)$. $S(G)$ is the set of incidence vectors in V → ℝ of stable finsets; $P(G)$ is convexHull ℝ (S G).
• Neighbours. Defined exactly as on p. 149: $y\ne z$ and, for some $c : V\to\mathbb Z$, the set of maximizers of $cx$ over $S(G)$ equals $\{y,z\}$. The face-lattice notion of an edge of $P(G)$ is not used; its equivalence with this definition is not part of the paper.
• Induced subgraph and connectedness. $H$ is G.induce of the set $(Y\setminus Z)\cup(Z\setminus Y)$, and "connected" is Mathlib's SimpleGraph.Connected, which requires at least one vertex. For $y=z$ both sides of the goal are therefore false.
• Trees. SimpleGraph.IsTree, which includes connectedness; a spanning tree of $H$ is a graph $T$ on the vertex set of $H$ with $T\le H$ and T.IsTree. In Lemma 6.1 the integers $c_u$ and $m$ are natural numbers.

A trivializing formalization — defining neighbours through the symmetric-difference condition or through Lemma 6.1's certificate, or omitting $y\neq z$ from the definition — is excluded: neighbours are defined only through unique maximizers of integer objectives over $S(G)$.

A complete development needs only finite graphs, induced subgraphs, spanning trees of connected graphs (available in Mathlib) and finite sums. Contributions welcome beyond the milestones: the equivalence of this notion of neighbours with the one-dimensional faces of $P(G)$, and Corollary 6.3 for the matching polytope via line graphs.

Selected references

• V. Chvátal, On certain polytopes associated with graphs, Journal of Combinatorial Theory, Series B 18 (1975), 138–154. https://doi.org/10.1016/0095-8956(75)90041-6
• J. Edmonds, Maximum matching and a polyhedron with 0,1-vertices, Journal of Research of the National Bureau of Standards 69B (1965), 125–130. https://doi.org/10.6028/jres.069B.013
• M. W. Padberg, On the facial structure of set packing polyhedra, Mathematical Programming 5 (1973), 199–215. https://doi.org/10.1007/BF01580121

Motivation

The stability number $\alpha(G)$ of a graph, the largest number of pairwise non-adjacent vertices, is the optimum of an integer program over the stable set polytope $P(G)$. Linear programming duality turns any explicit linear description of $P(G)$ into a certificate of optimality for $\alpha(G)$, which is why the question "which inequalities are needed to describe $P(G)$?" has been central to polyhedral combinatorics since Edmonds' description of the matching polytope (Edmonds 1965). Chvátal's 1975 paper (doi:10.1016/0095-8956(75)90041-6) initiated the systematic study of $P(G)$ for arbitrary graphs: which graph operations preserve a known description, and which inequalities are facets, i.e. indispensable in every description.

Section 4 of the paper treats one such operation, gluing two graphs along a complete subgraph, and one family of facets, the "rank" inequality $\sum_u x_u\le\alpha(G)$ for graphs whose critical edges connect all vertices. Combining the two yields a purely graph-theoretic fact about $\alpha$-critical graphs (graphs in which deleting any edge increases the stability number): no complete subgraph separates such a graph. The fact is due to Berge (Graphes et hypergraphes, 1970, Ch. 13, §3, Corollary 2); Chvátal's derivation obtains it from polyhedral arguments. $\alpha$-critical graphs were studied by Erdős and Gallai, Hajnal, Andrásfai and Lovász, and their structure is closely tied to the facets of $P(G)$.

Setting

Graphs are finite, undirected and loopless: $G=(V,E)$. A stable set is a set of pairwise non-adjacent vertices; $\alpha(G)$ is the largest size of a stable set. The incidence vector of $s\subseteq V$ is $\chi^s\in\mathbb R^V$ with $\chi^s_u=1$ for $u\in s$ and $0$ otherwise. $S(G)$ is the set of incidence vectors of stable sets and

$$P(G)=\operatorname{conv}S(G)\subseteq\mathbb R^V .$$

A finite system $\sum_{u\in V}a_{iu}x_u\le b_i$ $(i\in J)$ is a defining linear system of $P$ if its solution set is exactly $P$. An inequality $\sum_u a_ux_u\le b$ is a facet of $P$ if every defining linear system of $P$ contains, for some $t>0$, the inequality $\sum_u ta_ux_u\le tb$.

An edge $e$ of $G$ is critical if $\alpha(G-e)=\alpha(G)+1$; $E^*$ denotes the set of critical edges, $G^*=(V,E^*)$, and $G$ is $\alpha$-critical if every edge is critical. For graphs $G_1=(V_1,E_1)$, $G_2=(V_2,E_2)$ put $G_1\cap G_2=(V_1\cap V_2,E_1\cap E_2)$ and $G_1\cup G_2=(V_1\cup V_2,E_1\cup E_2)$. A vertex set $K$ is a cutset of $G$ if two vertices outside $K$ are joined by no path of $G-K$, the subgraph induced on $V\setminus K$.

In Lean, all objects live in the namespace ChvatalPolytopes.Separation: stablePolytope G, IsFacet P a b, IsCriticalEdge, criticalGraph G (for $G^*$), IsAlphaCritical G and IsCutset G K.

Formalization targets

Goal: Corollary 4.3 (p. 144)

For a finite connected $\alpha$-critical graph $G$ and any $K\subseteq V$ inducing a complete subgraph,

$$K \text{ is not a cutset of } G .$$

The goal is pure graph theory; its proof in the paper consists of the two polyhedral theorems below.

Milestones

1. Proposition 2.1 (pp. 139–140). For a finite nonempty set $S$ of solutions of $-x_u\le0$ $(u\in V)$, $\sum_u a_{iu}x_u\le b_i$ $(i\in J)$: the solution set equals $\operatorname{conv}S$ if and only if for every $c\in\mathbb Z^V$

$$\max\{cx:x\in S\}=\min\Big\{\sum_i\lambda_ib_i:\lambda\ge0,\ \sum_i\lambda_ia_{iu}\ge c_u\ (u\in V)\Big\}.$$

2. Theorem 4.1 (p. 141). If $G_1\cap G_2$ is complete, the union of defining linear systems of $P(G_1)$ and $P(G_2)$ (each containing its nonnegativity rows) is a defining linear system of $P(G_1\cup G_2)$.
3. Theorem 4.2 (p. 143). If $G^*$ is connected, then

$$\sum_{u\in V}x_u\le\alpha(G)$$

is a facet of $P(G)$.

Significance

Theorem 4.1 says that clique-sums are harmless for linear descriptions of $P(G)$: a description of a graph glued along a clique is the union of descriptions of the pieces. It underlies the later decomposition theory of stable set polytopes (clique cutsets appear throughout the study of perfect and $t$-perfect graphs). Theorem 4.2 supplies a large class of facets with a combinatorial certificate, and was the starting point of the study of rank facets. Corollary 4.3 illustrates how polyhedral statements yield structural graph theory: the facet in Theorem 4.2 cannot coexist with a clique cutset.

All three results are proved in the paper, and Berge's corollary was known before it. None of them has, to the knowledge of this mission, a machine-checked proof; Mathlib has stable sets (IsIndepSet, indepNum), cliques and convex hulls, but no stable set polytope, no notion of facet via defining systems, and no $\alpha$-critical graphs. The mission produces these definitions and the formal proofs of Proposition 2.1, Theorems 4.1, 4.2 and Corollary 4.3.

Difficulty

Proposition 2.1 requires LP duality in the form "min = max with both optima attained" together with a separation argument that reduces arbitrary objectives to integral ones; the "if" direction fails without the nonnegativity rows, so the statement is sensitive to the exact form of the system. In Theorem 4.1 the inclusion $P(G_1\cup G_2)\subseteq$ (solutions of the union) is routine; the difficulty is the converse: a point whose restrictions lie in $P(G_1)$ and in $P(G_2)$ is a convex combination of stable sets on each side, and the two combinations have to be matched on the clique $V_1\cap V_2$ to produce stable sets of $G_1\cup G_2$. Theorem 4.2 concerns every defining linear system, so it cannot be proved by exhibiting one description; the natural route via "affinely independent tight points" is a different definition of facet and needs full-dimensionality of $P(G)$ to be equivalent. Finally, the goal requires translating a cutset into a decomposition $G=G_1\cup G_2$ with complete intersection, and then showing that a union of two systems on smaller vertex sets cannot contain a positive multiple of $\sum_{u\in V}x_u\le\alpha(G)$.

Formalization scope

• Graphs are SimpleGraph V on a Fintype V with DecidableEq V. $S(G)$ is a set of functions V → ℝ (incidence vectors of stable finsets), and $P(G)$ is convexHull ℝ (stableVectors G).
• Linear systems are indexed by finite types with real coefficients. "Defining linear system" is equality of the solution set with the polytope. IsFacet quantifies over all finite index types J : Type and all real systems whose solution set equals the polytope; it is the paper's definition, not the affinely-independent-points characterization.
• Proposition 2.1: "min = max" means an attained minimum equal to the maximum; the hypothesis $S\neq\emptyset$ is added (the paper's $\max$ over $S$ needs it), and the nonnegativity rows are kept.
• Theorem 4.1: the glued graph $G$ lives on a type $V$ with finsets $V_1\cup V_2=V$; $G_1,G_2$ are the induced subgraphs on $V_1,V_2$; "$G_1\cap G_2$ complete" is encoded as "$V_1\cap V_2$ is a clique of $G$ and no edge joins $V_1-V_2$ to $V_2-V_1$", which is equivalent to the paper's hypotheses. The rows of each system are evaluated on the restriction of $x$.
• Theorem 4.2: "$G^*$ connected" is Mathlib's Connected, which requires $V\neq\emptyset$ — for $V=\emptyset$ the statement would be false. $\alpha(G)$ is indepNum, cast to $\mathbb R$.
• Corollary 4.3: "complete subgraph" is any clique set G.IsClique K, not only maximal cliques (the paper reserves "clique" for maximal complete subgraphs, but the corollary speaks of complete subgraphs), including $K=\emptyset$. "Cutset" means two vertices outside $K$ joined by no path of $G-K$. The formalization "$G-K$ is not connected" is ruled out: under Mathlib's convention it would make $K=V$ a cutset and the statement false for $K_1$ and $K_2$.
• Reusable infrastructure: the stable set polytope, facets via defining systems, Proposition 2.1 (shared with the other missions of this series), critical edges and $\alpha$-critical graphs. Contributions of intermediate lemmas (LP duality in the attained form, full-dimensionality of $P(G)$, the cutset–decomposition equivalence) are welcome.

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
• C. Berge, Graphes et hypergraphes, Dunod, Paris, 1970 (English translation: Graphs and Hypergraphs, North-Holland, 1973), Chapter 13, §3.
• 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
• M. W. Padberg, On the facial structure of set packing polyhedra, Math. Programming 5 (1973) 199–215. https://doi.org/10.1007/BF01580121
• L. Lovász, Normal hypergraphs and the perfect graph conjecture, Discrete Math. 2 (1972) 253–267. https://doi.org/10.1016/0012-365X(72)90006-4

Motivation

Many combinatorial optimization problems ask for the best subset of a finite set subject to combinatorial side conditions. The polyhedral method replaces the finite family of feasible subsets by the convex hull of their incidence vectors and asks for an explicit system of linear inequalities describing that convex hull; once such a system is known, linear programming duality gives min–max theorems and certificates of optimality. The maximum weight stable set problem is the central test case: it is NP-hard in general, so no tractable complete description of its polytope is expected for all graphs, and the question becomes for which graphs a simple description suffices.

V. Chvátal's 1975 paper On certain polytopes associated with graphs answers this question for the two simplest families of valid inequalities, and its Section 3 connects the answer to Berge's perfect graphs. The result is a standard entry point to polyhedral combinatorics and is one of the ingredients behind the later polynomial-time algorithms for stable sets in perfect graphs by Grötschel, Lovász and Schrijver.

Timeline. Berge (1961) introduced perfect graphs and conjectured that a graph is perfect if and only if its complement is. Lovász (Normal hypergraphs and the perfect graph conjecture, Discrete Math. 1972; A characterization of perfect graphs, J. Combin. Theory Ser. B 1972) proved this, together with the characterization of perfection by $\alpha(G_A)\,\omega(G_A)\ge|A|$ and the invariance of perfection under vertex duplication. Fulkerson's theory of antiblocking polyhedra (1971–72) gave a polyhedral route to the same equivalence. Chvátal (received 1972, published 1975) gave the self-contained polyhedral statement formalized here, with a proof based on Lovász's two theorems.

Setting

A graph $G=(V,E)$ is finite, undirected and loopless. A stable set is a set of vertices no two of which are adjacent. A clique is a maximal complete subgraph, and $C(G)$ is the set of vertex sets $W\subseteq V$ of the cliques of $G$.

$S(G)\subseteq\mathbb R^V$ is the set of zero–one vectors $x=(x_u:u\in V)$ such that $\{u:x_u=1\}$ is stable, and the stable set polytope is $P(G)=\operatorname{conv}S(G)$. A finite system of linear inequalities is a defining linear system of $P(G)$ if its solution set is exactly $P(G)$. For $c\in\mathbb R^V$ write $cx=\sum_{u\in V}c_ux_u$.

$G$ is perfect (the paper's $\alpha$-perfect) if for every zero–one vector $c$,

$$\max\{cx:x\in S(G)\}=\min\Big\{\sum_{W\in C(G)}\lambda_W:\ \lambda_W\in\{0,1\},\ \sum_{W\in C(G),\,u\in W}\lambda_W\ge c_u\ (u\in V)\Big\}.$$

For $A\subseteq V$, $G_A$ is the induced subgraph, $\alpha(G_A)$ its stability number and $\omega(G_A)$ its clique number. To duplicate a vertex $u$ is to add a new vertex $u'$ adjacent to all neighbours of $u$ but not to $u$.

In the Lean development these are stableVectors G, stablePolytope G, maximalCliques G, IsPerfect G and duplicate G u in the namespace ChvatalPolytopes.Perfect.

Formalization targets

Goal: Theorem 3.1 (p. 140)

For every graph $G$, the system

$$-x_u\le0\quad(u\in V),\qquad\sum_{u\in W}x_u\le1\quad(W\in C(G))$$

is a defining linear system of $P(G)$ if and only if $G$ is perfect. Both directions are required.

Milestones

1. Proposition 2.1 (pp. 139–140). For a finite nonempty set $S$ of solutions of $-x_u\le0$, $\sum_u a_{iu}x_u\le b_i$ $(i\in J)$, the solution set equals $\operatorname{conv}S$ if and only if for every $c\in\mathbb Z^V$

$$\max\{cx:x\in S\}=\min\Big\{\sum_i\lambda_ib_i:\lambda\ge0,\ \sum_i\lambda_ia_{iu}\ge c_u\ (u\in V)\Big\}.$$

2. Lovász's first theorem (§3, p. 140). Every nonperfect $G$ has $A\subseteq V$ with $\alpha(G_A)\,\omega(G_A)<|A|$.
3. Lovász's second theorem (§3, p. 140). Duplicating a vertex of a perfect graph gives a perfect graph.
4. Condition (iii) (p. 141). $G$ is perfect if and only if for every $c\in\mathbb Z^V$

$$\max\{cx:x\in S(G)\}=\min\Big\{\sum_{W\in C(G)}\lambda_W:\lambda_W\ge0,\ \sum_{W\ni u}\lambda_W\ge c_u\ (u\in V)\Big\}.$$

Significance

The result. The nonnegativity and clique inequalities are valid for $P(G)$ for every graph. Theorem 3.1 says they are complete exactly for perfect graphs, so on perfect graphs the maximum weight stable set problem is a linear program over an explicitly described polytope, and weighted min–max theorems (stable sets versus clique covers) follow from LP duality. Combined with the perfect graph theorem, it gives a polyhedral characterization of perfect graphs, and it is the model for later results that identify graph classes by the facets of their stable set polytopes (odd-cycle inequalities, $t$-perfection, Section 7 of the same paper).

Formalizing it. The result is classical and proved. No machine-checked version of it is known, and Mathlib has neither perfect graphs nor stable set polytopes. The mission produces a formal statement of the polyhedral characterization with the paper's own notion of perfection, a formal version of the convex-hull/LP min–max principle (Proposition 2.1), which is reusable for any 0–1 polytope, and formal statements of the two theorems of Lovász that the proof relies on.

Difficulty

Proposition 2.1 reduces Theorem 3.1 to the equivalence of perfection with a fractional min–max for all integer weights. The obvious approach to that equivalence fails in both directions. From perfection one only gets the min–max for zero–one weights and zero–one multipliers; general integer weights do not reduce to zero–one weights by linearity, because the minimum over clique covers is not additive in $c$. Conversely, a fractional clique cover of value $\alpha$ does not directly produce an integral one. The paper crosses this gap with two theorems of Lovász: a numerical certificate of nonperfection, and the invariance of perfection under vertex duplication. Both are substantial graph-theoretic results in their own right, and neither follows from the definitions by routine manipulation.

Proposition 2.1 itself needs separation of a point from a polytope by an integral objective and LP strong duality with the nonnegativity rows handled separately.

Formalization scope

Vertices form a finite type V with decidable equality; a graph is a SimpleGraph V. $S(G)$ is a set of functions V → ℝ, and $P(G)$ is Mathlib's convexHull ℝ of it. $C(G)$ is the finset of finsets that are maximal among cliques (Maximal), as on the page; with $V=\emptyset$ the only maximal clique is $\emptyset$. "Defining linear system" is an equality of sets. Every "max = min" is written out in full: there is a value $m$ that is the maximum over $S$ (attained and an upper bound), some feasible multiplier vector attains $m$, and every feasible multiplier vector has objective at least $m$. Clique multipliers are functions Finset V → ℝ read only on $C(G)$.

Explicit conventions and added hypotheses:

• In Proposition 2.1 the index set $J$ is a finite type, coefficients are real, the nonnegativity rows are kept as a separate conjunct $x\ge0$, and $S$ is assumed nonempty (the paper's $\max$ over $S$ needs it).
• $\alpha$ and $\omega$ are Mathlib's indepNum and cliqueNum (natural numbers) of G.induce A.
• The duplicated graph lives on Option V, with none the new vertex.

Perfection is the paper's zero–one min–max, not "the clique system defines $P(G)$" (which would make the goal a tautology) and not Berge's $\chi(G_A)=\omega(G_A)$ (a different definition, equivalent only through the perfect graph theorem). $P(G)$ is the convex hull of $S(G)$, never the solution set of an inequality system.

Needed infrastructure, all reusable: integral separation from a rational polytope and LP strong duality in the form $\max\{cx:Ax\le b,x\ge0\}=\min\{\lambda b:\lambda A\ge c,\lambda\ge0\}$; basic facts about stable sets and maximal cliques of induced subgraphs and of duplicated graphs; invariance of IsPerfect under graph isomorphism and under taking induced subgraphs. Proofs of the Lovász milestones, which have independent value for a Mathlib theory of perfect graphs, are welcome.

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
• L. Lovász, Normal hypergraphs and the perfect graph conjecture, Discrete Math. 2 (1972) 253–267. https://doi.org/10.1016/0012-365X(72)90006-4
• L. Lovász, A characterization of perfect graphs, J. Combin. Theory Ser. B 13 (1972) 95–98. https://doi.org/10.1016/0095-8956(72)90045-7
• D. R. Fulkerson, Anti-blocking polyhedra, J. Combin. Theory Ser. B 12 (1972) 50–71. https://doi.org/10.1016/0095-8956(72)90032-9
• M. Grötschel, L. Lovász, A. Schrijver, Geometric Algorithms and Combinatorial Optimization, Springer, 1988. https://doi.org/10.1007/978-3-642-97881-4

Motivation

The Shape Zero model (Shape Zero LLC, unpublished) reaches the Fano plane — the seven-point, seven-line configuration behind the seven imaginary units of the octonions — by a combinatorial route (C1 Formal Proofs, §3). Points are arranged in Steiner triple systems, and each point of each line is given one of three roles. The model's claim is that the role postulates alone force the number of points to be exactly seven. This mission proves that claim.

What this mission does NOT prove.

• Not that the system is the Fano plane. It proves the point count is $7$. That every Steiner triple system on $7$ points is the Fano plane up to relabelling is a classical result, but it is not formalized here.
• Not the modelling premise. Why lines have three points, and why there are three roles, is an input of the model, not derived here.
• Not the later steps from the Fano plane to the octonions, and from there to the node size $n = 3$ and $\mathfrak{u}(3)$.

Two corrections to C1 §3 built into this mission.

• At least one point is required. The empty system — no points, no lines — satisfies every condition vacuously and has $0$ points, so C1 Theorem 3.6 as stated is false for it. The goal carries the hypothesis $0 < n$. This is proved (in Lean, locally): the empty system is a Steiner triple system with a role colouring, so the statement without $0 < n$ is false.
• C1 Theorem 3.3(a) is not used. Its condition "any two lines meet" does not force $7$ points: it also holds for a single triple ($3$ points) and a single point, where there is no pair of lines to fail. This mission uses the role postulates instead.

Setting

Fix a natural number $n$ and take the points $\{0, \dots, n-1\}$. A Steiner triple system is a family of subsets, called lines, such that

1. every line has exactly $3$ points, and
2. every pair of distinct points lies on exactly one line.

A role colouring assigns to each point $x$ and line $\ell$ a role $\rho(x, \ell) \in \{0, 1, 2\}$ such that

1. the three points of a line get three different roles;
2. completeness: every point takes every role at least once, on some line through it;
3. minimality: every point takes every role at most once — two different lines through $x$ give $x$ different roles.

In Lean these are RolesForceSeven.STS n and RolesForceSeven.RoleColouring S role, with points Fin n and lines Finset (Fin n).

Formalization targets

Goal: the role postulates force exactly seven points

$$n \ge 1,\ \text{a Steiner triple system on } n \text{ points with a role colouring} \;\Longrightarrow\; n = 7 .$$

This is RolesForceSeven.roles_force_seven. It asserts the point count only.

Milestones

1. M1 (replication count). In any Steiner triple system, every point lies on exactly $r$ lines with $2r + 1 = n$.
2. M2 (three lines per point). Under a role colouring, every point lies on exactly $3$ lines.

Corollaries

• A — the Fano plane has a role colouring. The Fano plane on $\{0, \dots, 6\}$, with lines $\{i, i+1, i+3\}$ modulo $7$, admits a role colouring. Without this the goal could be vacuously true.
• B — AG(2, 3) is excluded (C1 Corollary 3.7): no Steiner triple system on $9$ points has a role colouring.

Significance

The result itself. It turns the model's role postulates into a precise count: whatever the Steiner triple system, if it carries a role colouring and has a point, it has exactly seven points. Corollary A shows the conditions are satisfiable, and Corollary B rules out the next Steiner triple system, AG(2, 3), explicitly.

Formalizing it. The C1 statement omits the non-emptiness hypothesis and is false for the empty system; the formal statement makes the hypothesis explicit and shows it is needed. The numerical check (Fano plane: $48$ role colourings; AG(2, 3): $0$; single triple: $0$) is replaced by a proof for every $n$.

Numerical cross-check

system	points	lines through each point	role colourings
Fano plane	7	3	48
AG(2, 3)	9	4	0
single triple	3	1	0
empty system	0	—	vacuous (all conditions hold)

Difficulty

Moderate. The central step is the replication count: the lines through a point $x$ must be shown to cover every other point exactly once, two at a time, which is a double-counting argument over the pairs through $x$. The role postulates then fix the replication number at three. The Fano plane corollary is a finite check.

Formalization scope

• Points are Fin n; lines are finite sets of points, with no ambient geometry assumed.
• The role function is total, Fin n → Finset (Fin n) → Fin 3; only its values on pairs $x \in \ell$ with $\ell$ a line matter.
• Completeness and minimality are both hypotheses; the goal uses both.
• $0 < n$ is necessary: without it the empty system is a counterexample (proved).
• The conclusion is the number $7$, not an isomorphism with the Fano plane.

Selected references

• Wikipedia, Steiner system (Steiner triple systems, replication number). https://en.wikipedia.org/wiki/Steiner_system
• Wikipedia, Fano plane. https://en.wikipedia.org/wiki/Fano_plane
• Wikipedia, Octonion (Fano plane mnemonic for the multiplication of imaginary units). https://en.wikipedia.org/wiki/Octonion

Motivation

The book has characterized learnability through uniform convergence and through stability; Chapter 30 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), gives a third sufficient condition, compression: if a learning algorithm's output can be reconstructed from a small subsequence of $k$ training examples, then the error on the remaining examples estimates the true error, and the algorithm generalizes with a bound of order $k\log(m/\delta)/m$ (Theorem 30.2, Littlestone and Warmuth). The bound is a union bound over the $m^k$ possible index sequences of a held-out estimate that follows from Bernstein's inequality (Lemma 30.1), and in the consistent case it gives $L_D \le 8k\log(m/\delta)/m$ (Corollary 30.3). Classes admitting such compression schemes include axis-aligned rectangles ($k = 2d$), homogeneous halfspaces ($k = d$, through the minimal-norm point of the convex hull and Carathéodory's theorem), separating polynomials by reduction, and any margin-separable data ($k \le 1/\gamma^2$, through the Perceptron). Whether every class of finite VC dimension has a compression scheme of size $O(d)$ is Warmuth's problem, open when the book was written.

Setting

A sample $S = (z_1, \dots, z_m)$ is drawn i.i.d. from $D$; a selection rule picks $(i_1, \dots, i_k) \in [m]^k$ (repetitions allowed), a reconstruction map $B : Z^k \to H$ produces $A(S) = B(z_{i_1}, \dots, z_{i_k})$, and $V$ is the set of positions not selected, with $L_V$ the average loss over them. The loss takes values in $[0,1]$. A class $H$ has a compression scheme of size $k$ (Definition 30.4) if for every $m \ge 1$ there are such $A$ and $B$ with $B(S_{A(S)})$ correct on every sample labeled by a member of $H$; the unrealizable version (Definition 30.5) asks $B(S_{A(S)})$ to be an empirical risk minimizer on every sample.

Formalization targets

Goal: Theorem 30.2

For a $[0,1]$-valued loss, $k \ge 1$, $m \ge 2k$, any reconstruction map $B$ and any selection rule, with probability at least $1 - \delta$ over $S \sim D^m$,

$$L_D(A(S)) \le L_V(A(S)) + \sqrt{L_V(A(S))\,\frac{4k\log(m/\delta)}{m}} + \frac{8k\log(m/\delta)}{m}.$$

Milestones

Lemma 30.1 (the held-out Bernstein bound); Corollary 30.3 (the consistent case); Lemma 30.6 (realizable schemes give unrealizable schemes); the compression scheme of size $2d$ for axis-aligned rectangles (§30.2.1); the separation property of the minimal-norm point of the convex hull (§30.2.2). Further items: the size-$d$ scheme for homogeneous halfspaces and the margin scheme of §30.2.4.

Significance

Compression bounds are the cleanest generalization argument in the book: no complexity measure of the class enters, only the number of examples needed to encode the output, and the resulting bound is data-dependent through $L_V$. They explain why support vector machines and the Perceptron generalize in terms of the number of support vectors or updates, and they underlie the sample-compression view of learning that connects to Chapters 9 and 15. Lemma 30.6 shows that compression is robust to label noise in the binary case. The halfspace scheme is a small piece of convex geometry of independent interest, and Warmuth's question about VC classes, settled in the affirmative for finite size by Moran and Yehudayoff after the book appeared, remains open in the form $O(d)$.

Difficulty

Lemma 30.1 is Bernstein's inequality for the $n$ held-out losses with variance at most $L_D(h_T)$, followed by solving the resulting quadratic in $\sqrt{L_D}$ to move the risk from the right-hand side to $L_V$; the constant $4$ comes out of that step (the exact value is about $3.19$). Theorem 30.2 is a union bound over the $m^k$ index sequences with $\delta' = m^k\delta$, using $|V| \ge m - k \ge m/2$ and $\log(m^k/\delta') \le k\log(m/\delta')$, which needs $k \ge 1$; formally the event for the learner is contained in the union of the events of Lemma 30.1 for each fixed index sequence, so no measurability of the selection rule is needed. Corollary 30.3 is immediate. Lemma 30.6 applies the realizable scheme to the subsample on which an ERM hypothesis is correct. The rectangle scheme is bookkeeping about extremal coordinates. The halfspace scheme needs three facts: the minimal-norm point of the hull separates (a one-line perturbation argument), it lies on a face and hence is a convex combination of $d$ sample points (Carathéodory's theorem, in Mathlib, applied to a face), and it is the minimal-norm point of the hull of those $d$ points (uniqueness of the projection onto a convex set); the existence of the minimizer uses compactness of the hull. The margin scheme is the Perceptron convergence theorem of Mission VI applied to the batch algorithm, whose output is the sum of the updated examples.

Formalization scope

Samples are Fin m-indexed under Mission I's iidLaw, and probability statements bound the outer measure of the failure event. Lemma 30.1 splits a sample of size $k + n$ into its first $k$ and last $n$ entries; Theorem 30.2 takes an arbitrary selection rule $\mathrm{sel} : Z^m \to [m]^k$ and reconstruction map $B$, the held-out set being the positions not in the range of the selection, and requires $k \ge 1$ and $m \ge 1$ in addition to the book's $m \ge 2k$: for $k = 0$ the bound reads $L_D \le L_V$, which fails, and the book's derivation uses $k \ge 1$ in $\log(m^k/\delta') \le k\log(m/\delta')$. Compression schemes are defined for every $m \ge 1$, since for $m = 0$ there is no index to select, with indices allowed to repeat as in $[m]^k$ and with $B$'s outputs in $H$; the unrealizable version uses Mission XXIII's multiclass 0–1 loss. The halfspace results are stated for strictly separable $\pm1$-labeled samples, $y_i\langle w^\star, x_i\rangle > 0$, the book's "w.l.o.g. all labels positive" normalization; this avoids the boundary negatives that a realizable sample may contain under the $\operatorname{sign}(0)$ convention of Mission VI, and it is the setting in which the minimal-norm argument works. The scheme is stated as the existence of $d$ indices whose signed examples have a minimal-norm hull point separating the whole sample, which is the content of $A$ and $B$ without fixing how ties among faces are broken. Rectangles are closed boxes. The margin scheme uses Theorem 9.1's normalization.

Not stated: §30.2.3 (polynomials, a reduction), the bibliographic remarks, and the intermediate Carathéodory step as a separate item.

Selected references

• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 30. doi:10.1017/CBO9781107298019
• N. Littlestone, M. K. Warmuth, Relating data compression and learnability, technical report, University of California, Santa Cruz, 1986.
• S. Floyd, M. K. Warmuth, Sample compression, learnability, and the Vapnik-Chervonenkis dimension, Machine Learning 21, 1995. doi:10.1007/BF00993593
• S. Ben-David, A. Litman, Combinatorial variability of Vapnik-Chervonenkis classes with applications to sample compression schemes, Discrete Applied Mathematics 86, 1998. doi:10.1016/S0166-218X(98)00000-6
• S. Moran, A. Yehudayoff, Sample compression schemes for VC classes, Journal of the ACM 63(3), 2016. doi:10.1145/2890490