Graph Theory

Motivation

Deciding whether a graph has a perfect matching, and finding one, are basic problems of combinatorial optimization; Edmonds' blossom algorithm solves them sequentially in polynomial time. The question behind this paper is whether they can also be solved in parallel, in polylogarithmic time on polynomially many processors (the class NC, or RNC when random bits are allowed).

The algebraic route to that question goes through the Tutte matrix. Tutte (1947) showed that a graph has a perfect matching if and only if its Tutte matrix, a skew-symmetric matrix of indeterminates, has a nonzero determinant. Substituting random numbers for the indeterminates turns this into a randomized parallel decision procedure, but it does not say which perfect matching exists, and a graph may have exponentially many.

Mulmuley, Vazirani and Vazirani (Combinatorica 7 (1987) 105–113) resolve this with the isolating lemma: random small integer weights make the minimum weight member of an arbitrary set family unique with probability at least one half. Once a single perfect matching is isolated, one determinant and one adjugate of an integer matrix reveal it. The isolating lemma has since become a standard tool in randomized algorithms and complexity theory, well beyond matchings.

Timeline:

• 1947, Tutte: a graph has a perfect matching iff the determinant of its Tutte matrix is a nonzero polynomial (doi:10.1112/jlms/s1-22.2.107).
• 1979, Lovász: random substitution into the Tutte matrix gives a randomized algorithm for deciding whether a perfect matching exists (Fundamentals of Computation Theory, LNCS 1979).
• 1986, Karp, Upfal and Wigderson: the first RNC algorithm that finds a perfect matching, with RNC³ running time (Combinatorica 6 (1986) 35–48).
• 1987, Mulmuley, Vazirani and Vazirani: the isolating lemma and an RNC² algorithm that inverts one integer matrix (this paper).
• 2016–2017, Fenner, Gurjar and Thierauf (arXiv:1601.06319) for bipartite graphs, and Svensson and Tarnawski (arXiv:1704.01929) for general graphs, partially derandomize the isolation step and place perfect matching in quasi-NC. Whether perfect matching is in NC remains open.

Setting

A set system $(S, F)$ is a finite set $S$ of elements together with a family $F$ of subsets of $S$. Given a weight $w_x \in \mathbb{N}$ for each element $x$, the weight of $T \subseteq S$ is $w(T) = \sum_{x \in T} w_x$, and $F$ has a unique minimum weight set if one member of $F$ is strictly lighter than every other member.

A graph $G$ has vertices $v_1, \dots, v_n$ (in Lean, Fin n, in their natural order) and edge set $E$, with $m = |E|$. A perfect matching is a set $M \subseteq E$ such that every vertex lies in exactly one edge of $M$. The edges and the perfect matchings of $G$ form a set system.

Given edge weights $w_{ij} \in \mathbb{N}$, the integer matrix $B$ is obtained from the Tutte matrix by substituting $2^{w_{ij}}$ for its indeterminates:

$$b_{ij} = 2^{w_{ij}} \ \text{if } (v_i, v_j) \in E,\ i < j; \qquad b_{ij} = -2^{w_{ij}} \ \text{if } (v_i, v_j) \in E,\ i > j; \qquad b_{ij} = 0 \ \text{otherwise}.$$

$|B|$ is its determinant, $B_{ij}$ the submatrix with row $i$ and column $j$ removed, and $\operatorname{adj}(B)$ its adjugate, whose $(j, i)$ entry is $\pm|B_{ij}|$.

The algorithm of §4 is:

1. Step 1. Compute $|B|$ and obtain $w$, the exponent for which $2^{2w}$ is the highest power of 2 dividing $|B|$.
2. Step 2. Compute $\operatorname{adj}(B)$.
3. Step 3. Output every edge $(v_i, v_j)$ for which the integer $|B_{ij}|\,2^{w_{ij}}/2^{2w}$ is odd.

Formalization targets

Goal: Steps 1–3 find a minimum weight perfect matching with probability at least 1/2

For every graph $G$ that has a perfect matching, with edge weights drawn uniformly and independently from $\{1, \dots, 2m\}$,

$$\Pr\bigl[\text{the output of Steps 1–3 is a perfect matching of } G \text{ of minimum weight}\bigr] \ \ge\ \tfrac12 .$$

This is the correctness half of the paper's Theorem (p. 109). The probability is a fraction of the $(2m)^m$ weight functions.

Milestones

1. Lemma 1 (isolating lemma): for a nonempty family $F$ over an $n$-element set, weights uniform in $[1, 2n]$ give a unique minimum weight set with probability $\ge 1/2$.
2. Isolation for perfect matchings (§4): with edge weights uniform in $[1, 2m]$, the minimum weight perfect matching is unique with probability $\ge 1/2$.
3. Odd-cycle cancellation (proof of Lemma 2): for a skew-symmetric integer matrix, only permutations all of whose cycles have even length contribute to the determinant.
4. Lemma 2: if the minimum weight perfect matching is unique, of weight $w$, then $|B| \neq 0$ and $2^{2w}$ is the highest power of 2 dividing $|B|$.
5. Lemma 3: under the same hypothesis, $(v_i, v_j) \in M$ iff $|B_{ij}|\,2^{w_{ij}}/2^{2w}$ is odd.
6. Steps 1–3, deterministic core: under the same hypothesis, Step 1 obtains the weight of $M$ and Steps 2–3 output exactly $M$.

Two companion items are included but are not on the goal's path: the maximum weight version of Lemma 1 (the remark after its proof, p. 107) and Lemma 4 (p. 110): the lexicographically largest matching set, for vertices sorted by decreasing weight, is a heaviest matching set.

Significance

The isolating lemma is a statement about arbitrary set families with no structure assumed, which is why it transfers: it is used for isolating satisfying assignments, for parallel algorithms for exact matching and minimum weight matchings with small weights, and in the derandomization program that led to the quasi-NC matching algorithms cited above. Lemmas 2 and 3 are the bridge from a combinatorial object (a unique minimum weight perfect matching) to arithmetic facts about one integer matrix (2-adic valuations of its determinant and adjugate entries), which is what makes the algorithm reducible to matrix inversion.

All results of this mission are proved in the paper. What the mission adds is machine-checked proofs: Mathlib at the pinned revision contains Tutte's barrier theorem but neither the isolating lemma nor the Tutte-matrix determinant arguments, and a search of Prove2Me (September 2026) found no formalization of them. A complete development yields a reusable isolating lemma for finite set systems and a reusable determinant expansion for skew-symmetric matrices.

Difficulty

The probabilistic step is a union bound over elements, but the event bounded for each element, "the element is ambiguous", is defined through a threshold that depends on all the other weights; the argument needs independence of that threshold from the element's own weight, which is a product-space (Fubini-type) counting statement rather than a one-line estimate. In a counting formalization over $\{1, \dots, 2n\}^S$, each fibre must be handled separately.

The determinant steps require a genuine combinatorial involution on permutations: reversing an odd cycle must be well defined (a canonical choice of cycle) and self-inverse, preserve the sign, negate the value, and in Lemma 3 also preserve the constraint $\sigma(i) = j$, which is where "since $n$ is even, there are at least two odd cycles" enters. Relating a permutation with only even cycles to a pair of perfect matchings whose union is its trail is the second nontrivial bijection. Divisibility must be tracked exactly: $2^{2w}$ divides every term, and every term other than the one of $M$ is divisible by $2^{2w+1}$.

Formalization scope

Vertices are Fin n and the graph is G : SimpleGraph (Fin n) with decidable adjacency. Edge weights are functions G.edgeSet → ℕ; perfect matchings are Finset G.edgeSet in which every vertex lies in exactly one edge. The matrix is weightedTutteMatrix G w : Matrix (Fin n) (Fin n) ℤ, with the positive entry above the diagonal. Probabilities are ratios of counts over Fintype.piFinset (fun _ => Finset.Icc 1 (2m)), stated without division as $(2m)^m \le 2 \cdot \#\{\dots\}$; the weight range is exactly $[1, 2m]$ (resp. $[1, 2n]$ in Lemma 1). "$x/2^k$ is odd" means $2^k \mid x$ and $x/2^k$ is an odd integer. The minor $|B_{ij}|$ is taken as Mathlib's signed cofactor adjugate B j i; parity and divisibility do not see the sign. Step 1's $w$ is $\lfloor \nu_2(|B|)/2\rfloor$.

Added hypotheses: Lemma 1 and its maximum version assume $F$ nonempty (the printed lemma omits it and is false for $F = \emptyset$); the goal and the isolation milestone assume $G$ has a perfect matching, which is the paper's own input assumption. Lemmas 2 and 3 allow arbitrary natural weights, as printed.

The algorithm's output is defined from $B$, $|B|$, $\operatorname{adj}(B)$, the 2-adic valuation and parity only; a definition of the output that refers to perfect matchings or to minimality would trivialize the goal and is ruled out. The complexity half of the Theorem (RNC², $O(n^{3.5}m)$ processors), which rests on Pan's matrix-inversion algorithm, is not formalized, nor are §5a–b and §6.

Contributions welcome: proofs of the milestones in any order, general lemmas about the permutation expansion of skew-symmetric determinants, and a counting form of the union bound over product spaces, all of which are reusable outside this mission.

Selected references

• K. Mulmuley, U. V. Vazirani, V. V. Vazirani, Matching is as easy as matrix inversion, Combinatorica 7(1) (1987) 105–113. https://doi.org/10.1007/BF02579206
• W. T. Tutte, The factorization of linear graphs, J. London Math. Soc. 22 (1947) 107–111. https://doi.org/10.1112/jlms/s1-22.2.107
• R. M. Karp, E. Upfal, A. Wigderson, Constructing a perfect matching is in random NC, Combinatorica 6(1) (1986) 35–48. https://doi.org/10.1007/BF02579407
• L. Lovász, On determinants, matchings, and random algorithms, Fundamentals of Computation Theory (FCT '79), 1979, 565–574.
• S. Fenner, R. Gurjar, T. Thierauf, Bipartite perfect matching is in quasi-NC, STOC 2016. https://arxiv.org/abs/1601.06319
• O. Svensson, J. Tarnawski, The matching problem in general graphs is in quasi-NC, FOCS 2017. https://arxiv.org/abs/1704.01929

Motivation

The stable set problem (find a largest, or maximum-weight, set of pairwise non-adjacent nodes in a graph) is NP-hard, and its linear programming relaxations have been studied since the 1970s as a test bed for polyhedral combinatorics. Lovász and Schrijver (SIAM J. Optim. 1991) introduced a general lift-and-project procedure for 0–1 programs: lift a relaxation to a cone of $(n+1)\times(n+1)$ matrices, impose conditions every 0–1 solution satisfies, and project back. Its semidefinite version, the operator $N_+$, is one of the first systematic uses of positive semidefinite constraints in combinatorial optimization, and it is the ancestor of the Sherali–Adams, Lasserre and sum-of-squares hierarchies used today in approximation algorithms and proof complexity.

For the stable set problem the paper measures the strength of the operators by an index: how many rounds are needed before a given valid inequality is implied. This mission formalizes the paper's result that one round of $N_+$ already implies four of the classical families of facets of the stable set polytope.

Timeline:

• 1975: Chvátal shows that the rank constraint of a connected α-critical graph defines a facet of its stable set polytope (Chvátal 1975); clique, odd hole and odd antihole constraints are special rank constraints.
• 1981–88: Grötschel, Lovász and Schrijver show that the weighted stable set problem is solvable in polynomial time for perfect and $h$-perfect graphs, through the theta body $\mathrm{TH}(G)$ (Grötschel, Lovász, Schrijver 1988).
• 1991: Lovász and Schrijver define the operators $N$ and $N_+$ and prove Corollary 2.15: clique, odd hole, odd wheel and odd antihole constraints have $N_+$-index 1.

Setting

Vectors live in $\mathbb R^{n+1}$ with coordinates $x_0, x_1, \dots, x_n$. The polar cone of $K$ is $K^* = \{u : u^{\mathsf T}x \ge 0 \ \forall x \in K\}$. Let $Q$ be the cone spanned by the 0–1 vectors with $x_0 = 1$. For a convex cone $K \subseteq Q$, the matrix cone $M_+(K)$ consists of the symmetric positive semidefinite matrices $Y = (y_{ij})$ with $y_{ii} = y_{0i}$ for $1 \le i \le n$ and $u^{\mathsf T}Yv \ge 0$ for all $u \in K^*$, $v \in Q^*$. The operator is

$$N_+(K) = \{Ye_0 : Y \in M_+(K)\},$$

and $N_+^0(K) = K$, $N_+^t(K) = N_+(N_+^{t-1}(K))$.

Let $G = (V, E)$ be a finite graph with no isolated nodes (the paper's standing assumption for Section 2). $\mathrm{STAB}(G)$ is the convex hull of incidence vectors $\chi^A$ of stable sets $A$. $\mathrm{FRAC}(G)$ is the polytope given by $x_i \ge 0$ and $x_i + x_j \le 1$ for $ij \in E$. $\mathrm{FR}(G) \subseteq \mathbb R^{V\cup\{0\}}$ is the cone $x_i \ge 0$, $x_i + x_j \le x_0$. The relaxations are

$$N_+^r(G) = \{x \in \mathbb R^V : (1, x) \in N_+^r(\mathrm{FR}(G))\},$$

so $N_+^0(G) = \mathrm{FRAC}(G) \supseteq N_+^1(G) \supseteq \dots \supseteq \mathrm{STAB}(G)$. The $N_+$-index of an inequality $a^{\mathsf T}x \le b$ valid for $\mathrm{STAB}(G)$ is the least $r$ with $a^{\mathsf T}x \le b$ valid for $N_+^r(G)$.

The four constraint families are:

• clique: $\sum_{i\in B} x_i \le 1$ for a clique $B$;
• odd hole: $\sum_{i\in C} x_i \le \frac12(|C|-1)$ for $C$ inducing a chordless odd cycle;
• odd wheel: $\sum_{i\in U\setminus\{u_0\}} x_i + \frac{|U|-2}{2}x_{u_0} \le \frac{|U|-2}{2}$ for $U$ inducing an odd wheel with center $u_0$ (an odd hole plus a node adjacent to all of it);
• odd antihole: $\sum_{i\in D} x_i \le 2$ for $D$ inducing a chordless odd cycle in the complement of $G$.

The contraction of a node $v$ turns $a^{\mathsf T}x \le b$ into the inequality with the coefficients of $v$ and its neighbours removed and right-hand side $b - a_v$.

Formalization targets

Goal: Corollary 2.15

For every graph $G$ without isolated nodes, each clique constraint (clique of size at least 3), odd hole constraint, odd wheel constraint and odd antihole constraint has $N_+$-index exactly 1:

$$a^{\mathsf T}x \le b \text{ holds on } N_+^1(G) \quad\text{and fails somewhere on } \mathrm{FRAC}(G).$$

Milestones

1. Lemma 1.5: for a closed convex cone $K \subseteq Q$ and $a$ with $a_i \le 0$ ($i \ge 1$), $a_0 \ge 0$, if $a^{\mathsf T}x \ge 0$ holds on $K \cap G_i$ (where $G_i = \{x_i = x_0\}$) for every $i$ with $a_i < 0$, then it holds on $N_+(K)$.
2. Lemma 2.14: if $a^{\mathsf T}x \le b$ is valid for $\mathrm{STAB}(G)$, and the contraction of every node with positive coefficient is valid for $N_+^r(G)$, then $a^{\mathsf T}x \le b$ is valid for $N_+^{r+1}(G)$.
3. Bipartite support (Section 2.c): an inequality valid for $\mathrm{STAB}(G)$ whose nonzero-coefficient nodes induce a bipartite graph is valid for $\mathrm{FRAC}(G)$.
4. Contraction property (Section 2.d): contracting a node with positive coefficient in any of the four constraints leaves positive-coefficient nodes that induce a bipartite subgraph.

Further result

Corollary 2.19 (first sentence): the $N_+$-index of a $\mathrm{STAB}(G)$-valid inequality $a^{\mathsf T}x \le b$ is at most the independence number of the subgraph induced by the nodes with positive coefficient.

Significance

Corollary 2.15 shows that a single round of $N_+$, a relaxation over which one can optimize in polynomial time for each fixed number of rounds (the paper's Theorem 2.1), captures all clique, odd hole, odd wheel and odd antihole inequalities at once. Consequently $N_+(G) = \mathrm{STAB}(G)$ for every $h$-perfect graph, in particular for perfect and $t$-perfect graphs. The result is a standard reference point when comparing lift-and-project hierarchies, and the lemmas behind it (Lemma 1.5 and Lemma 2.14) are the paper's general tools for bounding $N_+$-ranks.

The theorem was proved in 1991. To our knowledge it has not been machine-checked: this mission would produce the first formal development of the Lovász–Schrijver $N_+$ operator, its iterates, and the stable set relaxations $\mathrm{STAB}$, $\mathrm{FRAC}$, $\mathrm{FR}$ in Lean.

Difficulty

The lower bound (each constraint fails on $\mathrm{FRAC}(G)$) is a direct computation; the upper bound is where the work lies. The obvious approach, deriving each constraint from the linear conditions on the lifted matrix $Y$ alone, cannot succeed: those conditions define the linear operator $N$, and the goal is specifically about what positive semidefiniteness adds. The general lemmas are stated for arbitrary cones and require a working theory of polar cones and closedness in $\mathbb R^{n+1}$, including closedness of the iterates $N_+^r(\mathrm{FR}(G))$, which the paper uses without comment. The graph-theoretic steps require facts about the stable set and fractional stable set polytopes of bipartite graphs and a careful case analysis of chordless odd cycles in a graph and in its complement, none of which is in Mathlib.

Formalization scope

• Coordinates of $\mathbb R^{n+1}$ are indexed by Option ι, with none the special coordinate $x_0$. For graphs, ι := V.
• $M$ is defined by condition (iii) with polar cones, not by its reformulations. Only $M_+$, $N_+$ and their iterates are defined; the linear operator $N$ is not used.
• Lemma 1.5 carries the hypothesis that $K$ is closed. The paper takes it tacitly (all its cones are polyhedral); without it the lemma fails, since $N_+(K)$ depends only on the closure of $K$.
• $\mathrm{FR}(G)$ is defined by its constraints, which agree with the paper's "cone spanned by the vectors $(1,x)$, $x \in \mathrm{FRAC}(G)$" because $G$ has no isolated nodes. Every graph statement carries the no-isolated-nodes hypothesis.
• Contraction is written on the same graph $G$ as a zeroed coefficient vector, rather than on the subgraph $G - \Gamma(v) - v$.
• Odd holes include triangles; odd antiholes have at least 5 nodes (a 3-node "antihole" is a stable set, for which the constraint is false); odd wheels are an odd hole plus a center adjacent to all its nodes.
• Clique constraints in the goal are restricted to cliques with at least 3 nodes: cliques of size 1 or 2 give inequalities already valid on $\mathrm{FRAC}(G)$, of index 0.
• "$N_+$-index at most $r$" is stated as validity on $N_+^r(G)$; the index itself is stated with IsLeast, never with an infimum that would default to 0 on an empty set.

A formalization asserting only validity on $N_+^1(G)$, or only for one fixed graph, would be weaker than the paper's statement and is ruled out: the goal states the exact index for all graphs without isolated nodes and all four families.

Not formalized: the linear operator $N$ and its results, the polynomial-time separation results (Theorem 2.1, Corollaries 2.20–2.21), the theta-body results (Lemma 2.17, Corollary 2.18), graph indices (Corollary 2.16), and the second sentence of Corollary 2.19.

Reusable infrastructure includes the polar cone, the matrix cone $M_+$ and the $N_+$ operator (usable for any 0–1 program), the polytopes $\mathrm{STAB}$ and $\mathrm{FRAC}$, and odd holes, antiholes and wheels as finite-set predicates. Contributions proving closedness of the iterates, the integrality of $\mathrm{FRAC}$ for bipartite graphs, or the $M$-cone reformulations (iii′)–(iii″) are welcome.

Selected references

• L. Lovász and A. Schrijver, Cones of matrices and set-functions and 0–1 optimization, SIAM Journal on Optimization 1(2), 1991, 166–190. https://doi.org/10.1137/0801013
• M. Grötschel, L. Lovász and A. Schrijver, Geometric Algorithms and Combinatorial Optimization, Springer, 1988 (2nd ed. 1993). https://doi.org/10.1007/978-3-642-78240-4
• V. Chvátal, On certain polytopes associated with graphs, Journal of Combinatorial Theory B 18, 1975, 138–154. https://doi.org/10.1016/0095-8956(75)90041-6

Let $u_1, \dots, u_n$ be unit vectors in a Euclidean space such that among any three of them some two are orthogonal. How large can $\|u_1 + \dots + u_n\|$ be?

The answer is $\Theta(n^{2/3})$.

Attribution, which is commonly given wrong in both halves

Lovasz posed the question, as Problem 11.8 of Combinatorial Problems and Exercises (North Holland, 1979). Konyagin proved the $O(n^{2/3})$ upper bound in Systems of vectors in Euclidean space and an extremal problem for polynomials, Mat. Zametki 29 (1981) 63-74, doi:10.1007/BF01142512. Alon gave a matching lower bound in Explicit Ramsey graphs and orthonormal labelings, Electron. J. Combin. 1 (1994) R12, doi:10.37236/1192. The two together pin the exponent exactly.

Where the proof comes from

The hypothesis is a graph condition in disguise. Join $i$ to $j$ when $\langle u_i, u_j \rangle \ne 0$; then "among any three some two are orthogonal" says that graph is triangle-free.

The proof does not run through Ramsey counting, which is the natural first guess and does not reach the right exponent. It runs through the Lovasz theta function. Kashin and Konyagin bound $\theta = O(n^{1/3})$ for graphs of independence number less than 3, that is for complements of triangle-free graphs, and Cauchy-Schwarz turns that into the bound on the norm of the sum. The orthonormal labeling of a graph by unit vectors is not a coincidence of notation: it is the definition of $\theta$ that the argument uses.

What this mission will cost

State this honestly rather than discover it later. The Lovasz theta function, orthonormal graph labeling, and Shannon capacity are all absent from Mathlib. So the milestone chain that the upper bound needs cannot be written yet, and this proposal ships with exactly one milestone, which is Alon's lower bound.

google-deepmind/formal-conjectures contains an SDP-form definition of the theta function, with basic bounds such as lovaszThetaFunction_le_card since PR #6100 of 2026-09-18. The proof here needs the orthonormal-labeling form instead, so that file is a starting point rather than a foundation. Building the theta function, proving that the two forms agree, and getting the Kashin-Konyagin bound is the real content of this mission and is larger than the statement of the goal suggests.

The lower bound is the tractable half. It needs explicit Ramsey graphs and an orthonormal labeling of one, and it does not need $\theta$ at all.

Notes on the formalization

Both items are stated in Mathlib primitives alone, so the mission omits definition items. The triangle-free hypothesis is written as a condition on triples of indices rather than through SimpleGraph.CliqueFree 3, so that a reader auditing the statement does not have to unfold a graph construction to see what is assumed. Anyone proving it is free to build the graph and use the Mathlib predicate.

Motivation

The nearest common ancestor problem asks, for a rooted tree and two of its vertices $v$ and $w$, for the deepest vertex that is an ancestor of both, written $\operatorname{nca}(v,w)$. It is a subroutine in string and graph algorithms.

Harel and Tarjan (Fast Algorithms for Finding Nearest Common Ancestors, SIAM J. Comput. 13, 1984) preprocess a static tree of $n$ vertices in linear time on a random-access machine so that each query takes constant time. For a complete binary tree the queries reduce to bit arithmetic on vertex numbers (§3). An arbitrary tree is first reduced, in §4, to a compressed tree $C$ whose sizes double along every edge, and $C$ is cut by rank into three plies. Lemma 9 bounds the size of each ply, and those bounds are what make the tables of the method fit in linear space. This mission formalizes the structural lemmas of §4 about $C$ and Lemma 9.

Timeline.

• 1976: Aho, Hopcroft and Ullman give an $O(\log\log n)$-per-query random-access algorithm for static trees.
• 1979: Tarjan (Applications of path compression on balanced trees, J. ACM 26) uses the decomposition of a tree by the doubling rule on subtree sizes to compute functions on paths; Lemmas 5–7 of Harel–Tarjan are cited from there without proof.
• 1983: Sleator and Tarjan (A data structure for dynamic trees, J. Comput. System Sci. 26) use the same heavy/light split of edges for dynamic trees.
• 1984: Harel and Tarjan give the $O(n)$-preprocessing, $O(1)$-query algorithm, with the compressed tree and its plies (§4).

Setting

A rooted tree $T$ (Appendix, p. 354) consists of a finite vertex set $V$ with $n = |V|$, a root $r \in V$ and a parent map $p_T$, defined for $v \ne r$, such that every vertex reaches $r$ by iterating $p_T$. The edges of $T$ are the pairs $v \to p_T(v)$ for $v \ne r$. If $p_T^i(v) = w$ for some $i \ge 0$, then $v$ is a descendant of $w$ and $w$ an ancestor of $v$. Every vertex is its own ancestor and descendant. The depth of $v$ is the number of edges from $v$ to $r$. $\mathrm{size}_T(v)$ is the number of descendants of $v$, including $v$.

An edge $v \to p_T(v)$ is light if $2\cdot\mathrm{size}_T(v) \le \mathrm{size}_T(p_T(v))$ and heavy otherwise. At most one heavy edge enters each vertex, so the heavy edges partition $V$ into heavy paths. A vertex with no heavy edge entering or leaving it forms a heavy path by itself. The apex of a heavy path is its vertex of smallest depth, and $\mathrm{apex}(v)$ denotes the apex of the heavy path containing $v$.

The compressed tree $C$ has the same vertices and root as $T$, and its edges are

$$\{\, v \to \mathrm{apex}(p_T(v)) : v \ne r \,\}.$$

Write $p_C(v) = \mathrm{apex}(p_T(v))$, and let $\mathrm{size}_C(v)$ be the number of descendants of $v$ in $C$. The rank of $v$ is $\mathrm{rank}(v) = \lfloor \lg \mathrm{size}_C(v)\rfloor$, where $\lg = \log_2$. Let $\lg^{(i)}$ denote the $i$-fold iterate of $\lg$. Ply three is the set of vertices of rank at least $\lfloor\lg^{(2)} n\rfloor$. Ply two is the set of vertices whose rank lies between $\lfloor\lg^{(3)} n\rfloor$ and $\lfloor\lg^{(2)} n\rfloor - 1$, inclusive. Ply one is the set of vertices of rank below $\lfloor\lg^{(3)} n\rfloor$.

Formalization targets

Goal: Lemma 9 in the explicit form of its proof

For every rooted tree on $n \ge 4$ vertices:

$$|\text{ply three}| \le \frac{4n}{\lg n}, \qquad |\text{ply two}| \le \frac{4n}{\lg^{(2)} n},$$

and for every vertex $v$ in ply one, every $C$-descendant of $v$ lies in ply one and $\mathrm{size}_C(v) \le \lg^{(2)} n$.

The paper states the first two bounds as $O(n/\log n)$ and $O(n/\log^{(2)} n)$. The constants $4$ and $4$ are the ones its proof on p. 345 establishes. The third clause is the paper's "each connected component of ply one is a subtree of $C$ containing at most $\log^{(2)} n$ vertices", read vertex by vertex. Ply one is closed under $C$-descendants, so the component of a ply-one vertex is the $C$-subtree of its shallowest ply-one ancestor.

Milestones

1. Lemma 5 (p. 344): $\mathrm{size}_C(v) = \mathrm{size}_T(v)$ if $v$ is an apex, and $\mathrm{size}_C(v) = 1$ otherwise.
2. Lemma 6 (p. 344): $2\cdot\mathrm{size}_C(v) \le \mathrm{size}_C(p_C(v))$ for every $v \ne r$.
3. Lemma 8 (p. 344): for every $i$, at most $n/2^i$ vertices have rank $i$.
4. Proof of Lemma 9, first sentence (p. 345): at most $n/2^{k-1}$ vertices have rank $k$ or greater.

A further item states Lemma 7 (p. 344): $C$ has depth at most $\lfloor\lg n\rfloor$. The paper uses it to bound the tables of ply three, not in the proof of Lemma 9.

Significance

Lemma 9 is the counting step of the linear-time preprocessing. Ply three has $O(n/\log n)$ vertices, each with $O(\log n)$ ancestors in $C$ by Lemma 7, so storing every vertex's ply-three ancestors takes $O(n)$ space. Ply two has $O(n/\log^{(2)} n)$ vertices, each with $O(\log^{(2)} n)$ ply-two ancestors, which again gives $O(n)$. Ply one splits into subtrees of at most $\lg^{(2)} n$ vertices, and these are small enough to be embedded in complete binary trees and answered by the bit arithmetic of §3.

Lemmas 5–8 and the proof of Lemma 9 are proved or cited in the paper, and none of them is open. As far as a search of the platform shows, none has a machine-checked proof, and Mathlib has no parent-map rooted trees, subtree sizes or heavy-path decompositions. The mission produces a reusable formal account of heavy paths and of the size-doubling compressed tree, with the paper's explicit constants.

Difficulty

The paper states Lemmas 5–7 without proof, citing Tarjan (1979). Lemma 5 requires identifying the $C$-descendants of an apex with its $T$-descendants. That identification needs a clean description of heavy paths: at most one heavy edge enters each vertex, a vertex's heavy path runs up to its apex, and the heavy paths do not overlap. Lemma 8 needs the observation that two vertices of equal rank are unrelated in $C$, so that their descendant sets are disjoint and the sizes add up to at most $n$. Lemma 9 turns floors of iterated real logarithms into bounds on powers of two. The step $2^{\lfloor \lg^{(2)} n\rfloor} > \tfrac12 \lg n$ loses a factor $2$, and this is where the constant $4$ comes from; a proof that expects the constant $2$ fails at this step.

Formalization scope

• Trees. A rooted tree is a structure over a Fintype vertex type $V$ with a root, a total parent map and the axiom that every vertex reaches the root. The paper's partial map is made total by $p_T(r) = r$. Every statement about an edge $v \to p(v)$ assumes $v \ne r$, since for $v = r$ Lemma 6 would read $2n \le n$. The Appendix's printed "$p^0(v) = 0$" is read as $p^0(v) = v$.
• Heavy edges and apex. A heavy edge is $v \ne r$ with $\mathrm{size}_T(p_T(v)) < 2\,\mathrm{size}_T(v)$, the strict negation of light. $\mathrm{apex}(v)$ is computed by climbing heavy edges from $v$ until the first edge that is not heavy, which is the apex of the heavy path containing $v$. The root is always an apex.
• Compressed tree. $p_C(v) = \mathrm{apex}(p_T(v))$ for $v \ne r$ and $p_C(r) = r$. Ancestors and sizes in $C$ are defined through iterates of $p_C$.
• Logarithms. The rank is Nat.log 2 of $\mathrm{size}_C$, which is exactly $\lfloor\lg\mathrm{size}_C\rfloor$. The ply thresholds are iterated Nat.log 2, which equal the real floors $\lfloor\lg^{(2)} n\rfloor$ and $\lfloor\lg^{(3)} n\rfloor$ for $n \ge 4$. The bounds of the goal use Real.logb 2.
• Added hypothesis $n \ge 4$ in the goal. It makes $\lg n \ge 2$ and $\lg^{(2)} n \ge 1$, so the divisions are honest (Lean's $x/0 = 0$), and it makes $\lg^{(3)} n \ge 0$. On the page it is hidden in the $O(\cdot)$.
• Division-free milestones. Lemma 8 is stated as $\#\{\mathrm{rank} = i\}\cdot 2^i \le n$, and the rank-$\ge k$ count as $\#\{\mathrm{rank} \ge k\}\cdot 2^k \le 2n$.
• Ruled out. The goal is not an $\exists C$ statement. Replacing the paper's $4$ by an existential constant, or bounding ply three by $n$, would discard the content of the lemma.
• Welcome contributions. A library of facts about heavy paths is welcome: uniqueness of the entering heavy edge, apex characterizations, and the descendants of an apex in $C$. So are proofs of Lemmas 5–8 and proofs that the iterated Nat.log thresholds agree with the real ones. It is reusable for heavy-light decompositions generally.

Selected references

• D. Harel, R. E. Tarjan, Fast Algorithms for Finding Nearest Common Ancestors, SIAM J. Comput. 13(2):338–355, 1984. https://doi.org/10.1137/0213024
• R. E. Tarjan, Applications of path compression on balanced trees, J. ACM 26(4):690–715, 1979. https://doi.org/10.1145/322154.322161
• A. V. Aho, J. E. Hopcroft, J. D. Ullman, On finding lowest common ancestors in trees, SIAM J. Comput. 5(1):115–132, 1976. https://doi.org/10.1137/0205011
• D. D. Sleator, R. E. Tarjan, A data structure for dynamic trees, J. Comput. System Sci. 26(3):362–391, 1983. https://doi.org/10.1016/0022-0000(83)90006-5

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 minimum-cost circulation problem is a central problem of network optimization: transportation, assignment, shortest-path and maximum-flow problems are all special cases, and it is one of the few classes of linear programs with fast combinatorial algorithms. The oldest algorithm for it, the cycle-canceling algorithm of Klein (1967), repeatedly finds a residual cycle of negative cost and pushes as much flow as possible around it. With an arbitrary choice of cycle it can take exponentially many iterations even on integer data, and it need not terminate at all when capacities are irrational.

Goldberg and Tarjan (J. ACM 36(4), 1989) showed that one simple selection rule repairs this: always cancel a residual cycle whose mean cost (cost divided by number of arcs) is as small as possible. The resulting algorithm is strongly polynomial: its number of iterations is bounded by a polynomial in the number of vertices and arcs alone, independent of the magnitudes of capacities and costs. This mission formalizes that bound.

Timeline:

• 1967, Klein: the cycle-canceling algorithm, without an iteration bound.
• 1972, Edmonds and Karp: the first polynomial algorithm for minimum-cost flow (capacity scaling), polynomial in the bit length of the capacities.
• 1985, Tardos: the first strongly polynomial algorithm, introducing the arc-fixing idea that Theorem 3.8 generalizes.
• 1987–1989, Goldberg and Tarjan: generalized cost scaling and ε-optimality; in this paper, minimum-mean cycle canceling terminates after O(nm² log n) iterations for real costs (Theorem 3.9) and O(nm log(nC)) for integer costs bounded by C (Theorem 3.7).

Setting

A circulation network is a finite directed graph $G=(V,E)$ with $n=|V|$ vertices and $m=|E|$ arcs, which is symmetric ($(v,w)\in E$ iff $(w,v)\in E$, so $m$ counts both directions), together with real capacities $u(v,w)$ and real costs $c(v,w)$, the cost being antisymmetric: $c(v,w)=-c(w,v)$.

A circulation is a real function $f$ on arcs satisfying $f(v,w)\le u(v,w)$, $f(v,w)=-f(w,v)$ on every arc, and conservation $\sum_{v:(w,v)\in E} f(v,w)=0$ at every vertex $w$. Its cost is $\operatorname{cost}(f)=\tfrac12\sum_{(v,w)\in E}c(v,w)f(v,w)$, and $f$ is minimum-cost (optimal) if no circulation has smaller cost.

The residual capacity of an arc is $u_f(v,w)=u(v,w)-f(v,w)$; arcs with $u_f>0$ are residual arcs. A residual cycle is a simple cycle of residual arcs; its capacity is the minimum residual capacity along it, its cost $c(\Gamma)$ is the sum of its arc costs, and its mean cost is $c(\Gamma)/|\Gamma|$. Canceling a residual cycle raises the flow on each of its arcs by its capacity (and lowers the flow on each reverse arc by the same amount).

The minimum-mean cycle-canceling algorithm starts from any circulation and, while some residual cycle has negative cost, cancels a residual cycle whose mean cost is minimum among all residual cycles. Ties are broken arbitrarily, so the algorithm is a nondeterministic process; a run of length $K$ is any sequence $f_0,\dots,f_K$ of circulations produced by $K$ such iterations.

The analysis uses a price function $p:V\to\mathbb R$, the reduced cost $c_p(v,w)=c(v,w)+p(v)-p(w)$, and ε-optimality: for $\varepsilon\ge0$, $f$ is ε-optimal if some $p$ gives $c_p(v,w)\ge-\varepsilon$ on every residual arc. The quantity $\varepsilon(f)$ is the least such $\varepsilon$, and an arc is ε-fixed if all ε-optimal circulations carry the same flow on it.

Formalization targets

Goal: Theorem 3.9, with the proof's constant

For every circulation network with $n\ge2$ vertices, $m$ arcs, arbitrary real capacities and arbitrary real antisymmetric costs, every run of the minimum-mean cycle-canceling algorithm has length

$$K\ \le\ n\,m^2\,\lceil \ln n+1\rceil .$$

The statement quantifies over all starting circulations, all tie-breaking choices and all real data; it is the paper's $O(nm^2\log n)$ with the constant its proof establishes.

Milestones

In the order the proof uses them: Theorem 2.1 (optimal iff no negative residual cycle), Theorem 3.1 (optimal iff some price function has $c_p\ge0$ on residual arcs), Theorem 3.3 ($\varepsilon(f)=-\mu(f)$ for nonoptimal $f$, where $\mu(f)$ is the minimum cycle mean of the residual graph), Lemma 3.5 (a minimum-mean cancellation does not increase $\varepsilon(f)$), Lemma 3.6 ($m$ cancellations shrink $\varepsilon(f)$ by a factor $1-1/n$), and Theorem 3.8 (an arc with $|c_p(v,w)|\ge2n\varepsilon$ is ε-fixed).

Significance

Theorem 3.9 shows that a classical, natural algorithm is strongly polynomial: its iteration count depends only on the combinatorial size of the network. Combined with Karp's $O(nm)$ minimum-mean cycle algorithm it yields an $O(n^2m^3\log n)$ strongly polynomial algorithm (Theorem 3.10), and its method, measuring progress by the minimum cycle mean and fixing arcs once $\varepsilon(f)$ is small, underlies the faster cancel-and-tighten algorithm of Section 4 and later strongly polynomial analyses of network-flow and related algorithms.

The theorem has been proved since 1989; this mission's contribution is a machine-checked proof. To the best of the platform's catalogue, no cycle-canceling bound, minimum cycle mean or ε-optimality statement has been formalized. The platform does hold the negative-cycle optimality criterion in a different model (LinearOptimization.network_no_negative_cycle_optimal, Bertsimas–Tsitsiklis Theorem 7.6, with nonnegative flows and supplies) and a flow decomposition theorem (LinearOptimization.network_flow_decomposition); both are related to milestones here but are stated for a different network model.

Difficulty

The obvious potential function, the cost of the circulation, decreases at every iteration but by amounts that depend on the data, so it yields no bound independent of the capacities and costs. The analysis instead has to track $\varepsilon(f)$, an infimum over price functions, and relate it to the minimum cycle mean of a residual graph that changes after each cancellation, including arcs that appear only because of earlier cancellations. The strongly polynomial part needs a second ingredient: showing that the flow on some arc never changes again, which requires comparing the current circulation with all other ε-optimal circulations of the network, not only those the algorithm visits.

Formalization scope

Vertices form a finite type V; the arc set is E : Finset (V × V); capacities, costs and flows are real functions V → V → ℝ read only on E. $n$ is Fintype.card V and $m$ is E.card, counting $(v,w)$ and $(w,v)$ separately, as in the paper. Cycles are nonempty duplicate-free vertex lists, whose arcs are the cyclically consecutive pairs; one- and two-vertex cycles are allowed and have cost $0$. Minimum mean is taken over all residual simple cycles of the current circulation. $\varepsilon(f)$ is an infimum (sInf) over a set that is nonempty and bounded below for every circulation; its attainment is to be proved, never assumed.

Explicit constants replacing the paper's $O(\cdot)$:

• Theorem 3.9: the paper prints $O(nm^2\log n)$; its proof uses groups of $k=m\,n\lceil\ln n+1\rceil$ iterations, at most $m$ of them, so the goal states $K\le n\,m^2\lceil\ln n+1\rceil$ with the natural logarithm.
• The standing assumption $n\ge2$ (p. 874) is kept on the goal; the standing assumption $m\ge n$ is not used by the proof and is omitted.

"Terminates after at most $B$ iterations" means that every run has length at most $B$. Asserting only that some run is short, or that the process eventually stops, does not formalize the theorem; nor does a step relation that drops negativity, simplicity of the cycle, minimality of the mean over all residual cycles, or the update by exactly the cycle's capacity.

A complete development needs cycle decomposition of the difference of two circulations, LP duality for circulations (Theorem 3.1), and bookkeeping for the residual graph under cancellation. These are reusable for any cycle-canceling or cost-scaling analysis, and contributions of that infrastructure as separate lemmas are welcome. Theorem 3.7 (the integer-cost bound) and Section 4 are outside this mission.

Selected references

• A. V. Goldberg, R. E. Tarjan, Finding Minimum-Cost Circulations by Canceling Negative Cycles, J. ACM 36(4):873–886, 1989. https://doi.org/10.1145/76359.76368
• M. Klein, A primal method for minimal cost flows with applications to the assignment and transportation problems, Management Science 14(3):205–220, 1967. https://doi.org/10.1287/mnsc.14.3.205
• É. Tardos, A strongly polynomial minimum cost circulation algorithm, Combinatorica 5(3):247–255, 1985. https://doi.org/10.1007/BF02579369
• A. V. Goldberg, R. E. Tarjan, Finding minimum-cost circulations by successive approximation, Mathematics of Operations Research 15(3):430–466, 1990. https://doi.org/10.1287/moor.15.3.430
• R. M. Karp, A characterization of the minimum cycle mean in a digraph, Discrete Mathematics 23(3):309–311, 1978. https://doi.org/10.1016/0012-365X(78)90011-0
• J. Edmonds, R. M. Karp, Theoretical improvements in algorithmic efficiency for network flow problems, J. ACM 19(2):248–264, 1972. https://doi.org/10.1145/321694.321699

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