Combinatorics

Motivation

Statistical learning theory asks when the empirical frequencies of a whole class of events converge to their probabilities uniformly over the class. Vapnik and Chervonenkis answered this question in 1971 (Theory Probab. Appl. 16 (1971) 264–280) by attaching to every class of sets a single combinatorial quantity, the growth function, and bounding the probability of a large uniform deviation in terms of it. For that bound to be useful, the growth function must grow more slowly than an exponential. The first result of the paper, Theorem 1, shows that the growth function of any class is either exactly $2^r$ or bounded by a polynomial. This dichotomy is the reason finite VC dimension (the size of the largest fully shattered sample) became the central complexity measure of learning theory.

Timeline of the combinatorial core:

• 1971–1972. The same polynomial bound appeared in three independent papers: Vapnik and Chervonenkis (this paper; announced in Dokl. Akad. Nauk SSSR 181 (1968)), N. Sauer, On the density of families of sets, J. Combin. Theory Ser. A 13 (1972) 145–147, and S. Shelah, A combinatorial problem; stability and order for models and theories in infinitary languages, Pacific J. Math. 41 (1972) 247–261. The bound $\sum_{k=0}^{n} \binom{r}{k}$ of Lemma 1 below is now called the Sauer–Shelah lemma.
• 1989. Blumer, Ehrenfeucht, Haussler and Warmuth, Learnability and the Vapnik–Chervonenkis dimension, J. ACM 36 (1989) 929–965, made finite VC dimension the characterization of PAC learnability.

Setting

Let $X$ be a set and $S$ a collection of subsets of $X$. A sample of size $r$ is a finite sequence $x_1, \dots, x_r$ of elements of $X$; repetitions are allowed. Each $A \in S$ induces in the sample the subsample of the terms that lie in $A$, which is determined by the set of positions $\{i : x_i \in A\}$.

The index $\Delta^S(x_1, \dots, x_r)$ is the number of different subsamples induced by the sets of $S$, i.e. the number of distinct sets of positions $\{i : x_i \in A\}$ with $A \in S$. It is at most $2^r$. The growth function is

the maximum over all samples of size $r$. For the rays $\{y \le a\}$ on the line $m^S(r) = r + 1$; for the open subsets of $[0,1]$, $m^S(r) = 2^r$.

The function $\Phi(n, r)$ on pairs of natural numbers is defined by the recurrence (1) of the paper,

In the Lean development these are index S x for x : Fin r → X, growthFunction S r, and Phi n r in the namespace VapnikChervonenkis.GrowthFunction.

Formalization targets

Goal: Theorem 1 (p. 267)

For a nonempty class $S$, either $m^S(r) = 2^r$ for every $r$, or, with $n \ge 1$ the first value of $r$ at which $m^S(r) = 2^r$ fails,

The exponent $n$ is pinned down by minimality: $m^S(n) \ne 2^n$ and $m^S(r) = 2^r$ for every $r < n$.

Milestones, in the order the proof uses them

1. The index is at most $2^r$ (p. 265): $\Delta^S(x_1, \dots, x_r) \le 2^r$.
2. The closed form of $\Phi$ (p. 266): $\Phi(n, r) = \sum_{k=0}^{n} \binom{r}{k}$ for $r > n$, and $\Phi(n, r) = 2^r$ for $r \le n$.
3. The polynomial bound (p. 266): $\Phi(n, r) \le r^n + 1$ for $n > 0$, $r \ge 0$.
4. Lemma 1 (p. 266): if $1 \le n \le i$ and $\Delta^S(x_1, \dots, x_i) \ge \Phi(n, i)$, some subsample $x_{i_1}, \dots, x_{i_n}$ of size $n$ satisfies $\Delta^S(x_{i_1}, \dots, x_{i_n}) = 2^n$.
5. The first display of the proof of Theorem 1 (p. 268): if $m^S(n) \ne 2^n$, then $\Delta^S(x_1, \dots, x_r) < \Phi(n, r)$ for every sample of size $r > n$.

Significance

Theorem 1 converts the distribution-free bound $\mathbf P\{\pi^{(l)} > \varepsilon\} \le 4 m^S(2l) e^{-\varepsilon^2 l/8}$ of Theorem 2 of the same paper into a convergence statement: whenever the growth function is not identically $2^r$, the right-hand side is a polynomial times a decaying exponential, so relative frequencies converge to probabilities uniformly over $S$. The same dichotomy underlies sample-complexity bounds for PAC learning, covering-number bounds for VC classes, and the notion of VC dimension itself; the exponent $n$ is the VC dimension plus one.

The results are classical and proved. Mathlib contains the Sauer–Shelah lemma for finite set families (Finset.card_shatterer_le_sum_vcDim in Mathlib/Combinatorics/SetFamily/Shatter.lean). The platform has several open formal statements of Sauer's lemma for growth functions over finite point sets (ComputationalLearning.sauer_lemma, FoundationsML.RademacherVC.sauer_lemma, HighDimProb.Chaining.sauer_shelah) and a closed form for Kearns–Vazirani's $\Phi$ (ComputationalLearning.phi_closed_form, the same recurrence). No statement of Theorem 1, and none over the paper's sequence model of samples, is formalized. This mission formalizes the paper's own route: Lemma 1 in the paper's form, the polynomial bound on $\Phi$, and the dichotomy with the minimal exponent. It also provides the growth function over sequences that the companion missions (Theorem 2, and the entropy criterion Theorem 4) are stated with.

Difficulty

The obvious argument has two steps: bound $\Delta^S$ by $\Phi(n, r)$ whenever no subsample of size $n$ is fully split, then bound $\Phi(n, r)$ by $r^n + 1$. The first step is the Sauer–Shelah lemma, and it does not follow from counting alone. A class can induce many subsamples on $r$ points without inducing all $2^n$ on any fixed $n$ of them, and no counting of subsamples one position at a time rules this out. The second step is elementary but must hold uniformly for all $r$, including $r \le n$, where $\Phi(n, r) = 2^r$ and the bound $2^r \le r^n + 1$ uses $r \le n$.

Samples are sequences, not sets. With repeated points, two positions carrying the same point can never be separated, so Lemma 1 must be applied to position sets rather than point sets. Transferring Mathlib's set-family lemma to this setting is a bookkeeping step that does not reduce to a citation.

Formalization scope

• A sample of size $r$ is x : Fin r → X with positions $0, \dots, r-1$; repetitions are allowed. A subsample of size $n$ is x ∘ e with e : Fin n → Fin i strictly increasing.
• index S x counts distinct Finset (Fin r) of positions {i | x i ∈ A} with A ∈ S. Counting point sets A ∩ {x_1, …, x_r} instead would be a different object when points repeat; the growth function over finite sets of points (as in ComputationalLearning_VC) differs from $m^S$ when $X$ has fewer than $r$ elements.
• growthFunction S r is the supremum in ℕ of index S x over all samples; the family is bounded by $2^r$, so it is a maximum. When $X$ is empty and $r \ge 1$ its value is $0$; $m^S(0) = 1$ exactly when $S$ is nonempty.
• Phi is defined by the recurrence (1). The paper introduces $\Phi(n, r)$ as the maximal number of components into which $r$ hyperplanes cut $n$-space; that geometric identity (Example 3) is not part of this mission.
• Hypothesis added to Theorem 1: $S$ nonempty. The paper calls $n$ "a positive constant"; for $S = \emptyset$ every index is $0$, the first violation is at $r = 0$ and $n$ is not positive.
• Corrections of the printed text. (a) The closed form of $\Phi$ is printed with summand $\binom{r}{n}$; it is formalized with $\binom{r}{k}$ (the printed version already fails at $\Phi(1, 2) = 3$). (b) The proof of Theorem 1 ends "for $r > 0$, $\Phi(n, r) < r^n + 1$", which fails at $n = r = 1$; the milestone is the non-strict bound stated on p. 266. The milestone texts are verbatim from the page.
• Milestone 5 states the first display of the proof of Theorem 1 with its hypothesis as printed: $n$ is the first value of $r$ with $m^S(r) \ne 2^r$.
• The goal keeps the minimality of $n$. A version stating $m^S(r) \le r^n + 1$ for an arbitrary $n$ with $m^S(n) \ne 2^n$ would be a different theorem, and a version that drops the first disjunct or allows $n = 0$ would trivialize.

No measure, σ-algebra or probability appears: the class $S$ is an arbitrary collection of subsets of a bare type. Needed infrastructure: basic API for index (monotonicity in the sample, behaviour under restriction to a subsample) and a bridge between samples and Mathlib's set families (Finset.Shatters, Finset.vcDim). Both are reusable by the two companion missions of this paper, and contributions of either are welcome.

Selected references

• V. N. Vapnik and A. Ya. Chervonenkis, On the uniform convergence of relative frequencies of events to their probabilities, Theory of Probability and Its Applications 16(2) (1971) 264–280 (English translation by B. Seckler). https://doi.org/10.1137/1116025
• N. Sauer, On the density of families of sets, Journal of Combinatorial Theory, Series A 13 (1972) 145–147. https://doi.org/10.1016/0097-3165(72)90019-2
• S. Shelah, A combinatorial problem; stability and order for models and theories in infinitary languages, Pacific Journal of Mathematics 41 (1972) 247–261. https://doi.org/10.2140/pjm.1972.41.247
• A. Blumer, A. Ehrenfeucht, D. Haussler and M. K. Warmuth, Learnability and the Vapnik–Chervonenkis dimension, Journal of the ACM 36(4) (1989) 929–965. https://doi.org/10.1145/76359.76371

Motivation

This mission is the sixteenth and last of the Disjunctive Programming series, and its goal theorem is the book's own closing result. The chapter's arc closes a loop opened at the very start of the book: Theorem 2.1 (02a-convex-hull) gave the convex hull of a union of polyhedra in the same space via lifting; this chapter's Theorem 13.13 (not drafted in this mission — see below) gives the dominant of a union of polytopes in different spaces, and the chapter's final result specializes that machinery to the case where the two polytopes are polymatroids — obtaining a fully explicit, closed-form convex hull in the original variable space, with no lifting at all. Polymatroids are among the most heavily studied objects in combinatorial optimization, from Edmonds's foundational greedy-algorithm characterization onward (J. Edmonds, Submodular functions, matroids, and certain polyhedra, in Combinatorial Structures and Their Applications, Gordon and Breach, 1970, 69–87), and a disjunction of two polymatroids — "satisfy one covering system or the other" — arises naturally whenever two competing combinatorial resource constraints interact.

Setting

Fix a ground set $N = \{1,\dots,n\}$. A set function $r : 2^N \to \mathbb{R}$ is a polymatroid rank function if $r(\emptyset)=0$, $r$ is nondecreasing, and $r$ is submodular: $r(A)+r(B) \ge r(A\cup B)+r(A\cap B)$ for all $A,B\subseteq N$. (A related but distinct condition, used earlier in the chapter for "Application 1," additionally requires $r(A)\le|A|$ on every proper subset — matroid rank functions satisfy both.) The associated polymatroid is

For two ground sets $M,N$ and set functions $r_1,r_2$, the disjoint-space union is $Z(r_1,r_2) := \{(x,y)\in[0,1]^m\times[0,1]^n : x\in P(r_1) \text{ or } y\in P(r_2)\}$. For polymatroid rank functions $r_1,r_2$ on the same ground set $N$, $\Pi := \{\pi \ge 0 : \pi x \le 1 \text{ for } x \in P(r_1)\cup P(r_2)\}$ and $U := \{u \ge 0 : \sum_A u_A r_i(A) \le 1,\ i=1,2\}$ (indexed by all subsets $A \subseteq N$) are the auxiliary polytopes the final proof reduces to.

Formalization targets

Proposition 13.16. For set functions $r_1,r_2$ satisfying the Application-1 conditions,

Corollary 13.21. The same-space specialization: $\mathrm{conv}(P(r_1)\cup P(r_2)) = \{w\in[0,1]^n : w=x+y, \text{[the same displayed inequality, } A,B\subseteq N\text{]}\}$.

Proposition 13.22. $\Pi$ is exactly the projection, onto $\pi$, of $\{\pi_j \le \sum_{A\ni j} u_A\ (j\in N),\ \sum_A u_A r_i(A)\le1\ (i=1,2),\ \pi,u\ge0\}$.

Proposition 13.23. Every extreme point of $\Pi$ arises from an extreme point of $U$ via $\pi_j = \sum_{A\ni j} u_A$.

Theorem 13.24 (goal, the book's closing theorem). For polymatroid rank functions $r_1,r_2$,

The targets trace the book's own tower: the disjoint-space specialization (13.16) and its same-space corollary (13.21) establish the lifted description; Propositions 13.22-13.23 build the blocker/projection machinery; Theorem 13.24 collapses everything into the unlifted, original-variable-space closed form that is the book's final word.

Significance

Theorem 13.24 is a genuinely rare achievement in polyhedral combinatorics: a complete, explicit, non-lifted facet description for the union of two polymatroids — objects whose individual facet structure is already exponential and only tractable via the greedy algorithm and submodular minimization. That the union of two such objects still admits a closed form, stated purely in terms of the two rank functions evaluated at pairs of subsets, is the payoff the entire chapter's machinery (dominants, blockers, upper monotonicity, disjoint-space unions) was built toward. The result strictly generalizes an earlier theorem restricted to matroid polyhedra, obtained there by different techniques specific to matroids; this proof works because polymatroid optimization (Edmonds's greedy algorithm) survives in the more general submodular, non-0/1-truncated setting.

Both directions are proved in the source (Balas's own chapter, building on Edmonds's polymatroid theory and the disjoint-union machinery developed earlier in the same chapter) but have no counterpart on this platform: nothing existing treats polymatroids, polymatroid rank functions, or a closed-form union of two polymatroids. Mathlib's Combinatorics/Matroid/* covers matroids and their rank functions but not this strictly more general polymatroid object (an integer- or real-valued submodular monotone set function, not a matroid's 0/1-truncated rank). This mission produces the first Lean statements of all five targets.

Difficulty

The obvious shortcut for Theorem 13.24 is to state only the "single active subset" family of inequalities ($x(A)\le\max\{r_1(A),r_2(A)\}$) and treat the two-subset family as a minor addendum — but the two-subset inequalities are not optional refinements, they are half of the facet system, arising from the genuinely two-dimensional case of the underlying linear program (a basic feasible solution of $U$ with two nonzero components). Dropping them, or stating them only for a special case of $A,B$, would produce a strictly weaker (and generally invalid, since it would omit real facets) description.

The condition $(r_1(A)-r_2(A))(r_1(B)-r_2(B))<0$ is easy to state but not to motivate without the underlying linear algebra: it is exactly the condition under which the $2\times2$ system $u_Ar_1(A)+u_Br_1(B)=1$, $u_Ar_2(A)+u_Br_2(B)=1$ has a solution with both $u_A,u_B>0$ — a fact the book verifies by direct computation (Cramer's rule) rather than a structural argument, which is why this mission states the condition exactly as derived rather than paraphrasing it into a more "intuitive" but unfaithful form.

Formalization scope

The ambient space is Fin n → ℝ throughout (or Fin m → ℝ / Fin n → ℝ separately for Proposition 13.16's disjoint spaces), matching the series default; subsets $A,B\subseteq N$ are Finset (Fin n), and the auxiliary variable $u$ of Propositions 13.22-13.23 is indexed by Finset (Fin n) itself (a genuine Fintype for fixed n), matching "$u_A$ for all $A\subseteq N$" directly. IsApp1SetFunction and IsPolymatroidRankFunction are kept as two distinct predicates — the goal theorem uses the latter, Proposition 13.16/Corollary 13.21 the former — matching BRIEF.md's explicit warning to locate and preserve the book's own exact numbered conditions rather than infer a single merged notion. A trivializing formalization to rule out explicitly: stating Theorem 13.24 with only the single-subset inequality family, which would omit the two-subset facets that are half of the theorem's actual content.

This mission depends on no other chunk's Lean definitions; it restates 13a-dominants's dominant/blocker/upper-monotone vocabulary only informally (the underlying object, not any specific Lean declaration), per the series convention, since no chunk in this series can import another's draft module. Theorem 13.13 (the general dominant of a disjoint-space union) and Theorem 13.18 (the general same-space reduction) — the two results whose specializations Proposition 13.16 and Corollary 13.21 respectively are — were not drafted this pass; see HARD.md. As the last mission of the whole book, this chunk's items.yaml closes the series begun in 01-intro-duality: sixteen missions, one book, spanning from the founding disjunctive Farkas lemma to this closed-form union of two polymatroids.

Selected references

• J. Edmonds, Submodular functions, matroids, and certain polyhedra, in Combinatorial Structures and Their Applications, Gordon and Breach, 1970, 69–87 (reprinted in Combinatorial Optimization — Eureka, You Shrink!, LNCS 2570, Springer, 2003, 11–26, https://doi.org/10.1007/3-540-36478-1_2).
• E. Balas, A. Bockmayr, N. Pisaruk, and L. Wolsey, On unions and dominants of polytopes, Mathematical Programming A 99 (2004), 223–239. https://doi.org/10.1007/s10107-003-0432-4
• E. Balas, Disjunctive Programming, Springer, 2018, Chapter 13, §13.2.1–13.8 (the book's final chapter). https://doi.org/10.1007/978-3-030-00148-3

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|$ 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\}$,

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

Many polytopes that arise from combinatorial optimization problems have no small facet description in their natural variable space, yet become describable by a compact linear system once lifted to a higher-dimensional space of auxiliary variables and projected back down — Chapter 2's own extended formulation of the convex hull of a disjunctive set is one instance of this phenomenon. This chapter turns the idea around: rather than using projection to build a compact formulation, it uses projection to prove integrality of a formulation that is already compact but whose integrality is not obvious from any standard sufficient condition (total unimodularity, balancedness, etc.). The technique is illustrated on three closely related combinatorial polytopes built from perfectly matchable, assignable, and path-decomposable vertex subsets of a graph or digraph — each proved integral by lifting to an edge- or arc-variable space where total unimodularity is easy to check, then projecting.

Setting

For a finite vertex set $V$, the incidence vector of $W \subseteq V$ is $1$ on $W$, $0$ elsewhere, and $x(S) := \sum_{i \in S} x_i$. A graph $G(W)$ has a perfect matching if there is a fixed-point-free involution on $W$ respecting adjacency. The PMS (Perfectly Matchable Subgraph) polytope of $G$ is $\mathrm{conv}(X)$ where $X$ is the set of incidence vectors of such $W$; $N(S) := \{j \notin S : (i,j) \in E \text{ for some } i \in S\}$.

For a digraph $(V,A)$: $G(W)$ is assignable if it admits a cycle decomposition (a permutation of $W$ respecting arcs), giving the Assignable Subgraph Polytope. For an acyclic digraph with distinguished nodes $s,t$: $G(W \cup \{s,t\})$ admits an $s$-$t$ path decomposition if a collection of interior-node-disjoint $s$-$t$ paths covers it, giving the $s$-$t$ Path Decomposable Subgraph Polytope over $W \subseteq V \setminus \{s,t\}$. $\Gamma(S)$ and $\Gamma^*(S)$ are the corresponding out-neighborhood operators. For an arbitrary graph, $c(S)$ counts the connected components of the induced subgraph $G(S)$.

Formalization targets

Theorem 5.1 (goal) — the PMS polytope of a bipartite graph

Theorem 5.2 — the Assignable Subgraph Polytope

Theorem 5.3 — the $s$-$t$ Path Decomposable Subgraph Polytope

Theorem 5.4 — the PMS polytope of an arbitrary graph

for every $S$ all of whose components are single nodes or nonbipartite with odd order — the weakest faithful statement, since dropping the side condition would assert the inequality for subsets it does not hold for.

Significance

The results themselves. Each theorem gives an explicit, checkable linear system defining a polytope that arises naturally from a combinatorial covering/decomposition property, turning "does $G(W)$ have property $X$" into a linear-programming feasibility question. Theorem 5.1 is the one the book proves in full and the template for the other three: bipartite matching, digraph assignment, and acyclic-digraph path decomposition are structurally parallel problems (all reduce to checking a König–Hall-type combinatorial condition), and the same lift-and-project technique handles all three uniformly. Theorem 5.4 extends the idea to arbitrary (non-bipartite) graphs at the cost of a sharper right-hand side and a component-based side condition, connecting to Edmonds' classical matching-polytope theory while remaining a genuinely different object (a polytope of coverable vertex sets, not of matchings themselves).

Formalizing it. No object in this mission — the PMS, Assignable, or Path Decomposable Subgraph polytopes, or their defining neighbor operators — exists on the platform prior to this mission. The closest platform result, MetricTSP.pm_polytope_decomposition (Edmonds' perfect matching polytope theorem, in edge-variable space over a fixed vertex set requiring every vertex matched), is a genuinely different object from Theorem 5.4's PMS polytope (vertex-variable space, vertices may be left unmatched by design) and is not reused as a kind: reference item; it is noted here as related, not equivalent.

Difficulty

The natural first attempt tries to verify each polytope's integrality directly, by checking a known sufficient condition (total unimodularity, balancedness) on the displayed vertex-space system itself. This fails: the book states explicitly that (5.5)'s coefficient matrix is not totally unimodular, which is exactly why the lift-to-edge-variables step is necessary at all. The real content of each theorem is the two-part argument: (1) the lifted system in edge/arc variables is totally unimodular (checkable directly), so its polyhedron is integral; and (2) the vertex- space system is exactly the projection of the lifted one — a nontrivial fact requiring Chapter 2's projection machinery, not merely an unfolding of definitions. Theorem 5.4's extra difficulty, flagged explicitly in the text, is that its projection cone is not pointed, so the proof must work with a finite generating set rather than extreme rays, and it suffices to find a subset of generators producing every facet rather than a complete generating set — a genuinely harder argument the book itself outsources to a citation.

Formalization scope

Undirected graphs use Mathlib's SimpleGraph; digraphs use a bare relation A : V → V → Prop (not required symmetric or irreflexive, matching the book's unrestricted notion). Bipartition is recorded via part : V → Bool (decidable by construction) rather than two Set V halves, keeping the sums x(V_1), x(V_2) computable over Finsets throughout. IsAssignable uses Equiv.Perm on the vertex-set subtype, since a cycle decomposition is exactly a permutation. IsComponentOf and IsBipartiteOn (Theorem 5.4) are built directly from reachability and 2-colorability rather than Mathlib's induced-subgraph/ConnectedComponent API, matching the "maximal connected subset" reading of "component" the book's own prose intends.

IsPathDecomposable (Theorem 5.3) encodes "admits an $s$-$t$ path decomposition" via a degree-constrained arc set (every interior node has exactly one incoming and one outgoing chosen arc, none entering $s$ or leaving $t$, at least one leaving $s$) rather than an explicit list of vertex-disjoint paths — provably equivalent by the standard fact that an acyclic arc set with this degree pattern always decomposes into such a path family, and considerably lighter to state and reason about than constructing Path objects directly.

A trivializing formalization is ruled out explicitly: every theorem keeps the fractional box constraint $0 \le x_i \le 1$ rather than the integral $x_i \in \{0,1\}$ (per BRIEF.md's own warning, dropping the relaxation collapses the claim to a restatement of the combinatorial definition), and Theorem 5.1 is stated only for bipartite graphs — never generalized to subsume Theorem 5.4's genuinely different inequality system and side condition.

Selected references

• E. Balas, Disjunctive Programming, Springer, 2018. DOI: 10.1007/978-3-030-00148-3, Chapter 5, §5.2.
• M. O. Ball, U. Derigs, An analysis of alternate strategies for implementing matching algorithms, Networks 13 (1983) (cited in the text as [13], the origin of Theorems 5.2 and 5.3).
• W. R. Pulleyblank, J. Edmonds, Facets of 1-matching polyhedra, in Hypergraph Seminar, Springer Lecture Notes in Mathematics 411 (1974) — the origin of the perfectly matchable subgraph polytope literature (cited in the text as [34], the origin of Theorem 5.1).
• L. Lovász, M. D. Plummer, Matching Theory, Elsevier, 1986 (cited in the text as [35], the origin of Theorem 5.4).

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

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

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:

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