Motivation

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

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

Setting

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

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

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

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

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

Formalization targets

Goal: Corollary 4.3 (p. 144)

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

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

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

Milestones

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

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

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

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

is a facet of $P(G)$.

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

• V. Chvátal, On certain polytopes associated with graphs, J. Combin. Theory Ser. B 18 (1975) 138–154. https://doi.org/10.1016/0095-8956(75)90041-6
• C. Berge, Graphes et hypergraphes, Dunod, Paris, 1970 (English translation: Graphs and Hypergraphs, North-Holland, 1973), Chapter 13, §3.
• J. Edmonds, Maximum matching and a polyhedron with 0,1-vertices, J. Res. Nat. Bur. Standards 69B (1965) 125–130. https://doi.org/10.6028/jres.069B.013
• M. W. Padberg, On the facial structure of set packing polyhedra, Math. Programming 5 (1973) 199–215. https://doi.org/10.1007/BF01580121
• L. Lovász, Normal hypergraphs and the perfect graph conjecture, Discrete Math. 2 (1972) 253–267. https://doi.org/10.1016/0012-365X(72)90006-4

Motivation

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

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

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: Theorem 3.1 (p. 140)

For every graph $G$, the system

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

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

Milestones

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

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

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

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

Explicit conventions and added hypotheses:

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

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

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

Selected references

• V. Chvátal, On certain polytopes associated with graphs, J. Combin. Theory Ser. B 18 (1975) 138–154. https://doi.org/10.1016/0095-8956(75)90041-6
• L. Lovász, Normal hypergraphs and the perfect graph conjecture, Discrete Math. 2 (1972) 253–267. https://doi.org/10.1016/0012-365X(72)90006-4
• L. Lovász, A characterization of perfect graphs, J. Combin. Theory Ser. B 13 (1972) 95–98. https://doi.org/10.1016/0095-8956(72)90045-7
• D. R. Fulkerson, Anti-blocking polyhedra, J. Combin. Theory Ser. B 12 (1972) 50–71. https://doi.org/10.1016/0095-8956(72)90032-9
• M. Grötschel, L. Lovász, A. Schrijver, Geometric Algorithms and Combinatorial Optimization, Springer, 1988. https://doi.org/10.1007/978-3-642-97881-4

Motivation

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

What this mission does NOT prove.

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

Two corrections to C1 §3 built into this mission.

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

Setting

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

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

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

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

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

Formalization targets

Goal: the role postulates force exactly seven points

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

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

Milestones

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

Corollaries

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

Significance

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

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

Numerical cross-check

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

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

Setting

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

Formalization targets

Goal: Theorem 30.2

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

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

Milestones

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

Significance

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

Difficulty

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

Formalization scope

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

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

Selected references

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

Motivation

Chapter 17 introduced multiclass prediction; Chapter 29 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), asks the two questions the fundamental theorem answered for binary classes: which classes of multiclass predictors are PAC learnable with respect to the 0–1 loss, and with what sample complexity. Natarajan's dimension generalizes the VC dimension by shattering with two disagreeing label functions, and the multiclass fundamental theorem (Theorem 29.3) bounds the uniform-convergence, agnostic and realizable sample complexities in terms of it, up to logarithmic factors in the number of labels $k$; the only new ingredient in its proof is Natarajan's lemma, the multiclass substitute for Sauer's lemma. The chapter then computes or bounds the Natarajan dimension of the classes that matter, One-versus-All and general reductions to binary classifiers, and linear multiclass predictors (Theorem 29.7). Its last section is a warning: unlike the binary case, not all ERMs are equal, and with infinitely many labels a class can be learnable by one ERM and not by another, so learnability and uniform convergence come apart (Claim 29.9).

Setting

$H$ is a class of functions from $X$ to a finite label set $Y$ with $|Y| = k$. $C \subseteq X$ is shattered by $H$ if there are $f_0, f_1 : C \to Y$ with $f_0(x) \ne f_1(x)$ everywhere on $C$ such that every $B \subseteq C$ is realized by some $h \in H$ agreeing with $f_0$ on $B$ and with $f_1$ on $C \setminus B$ (Definition 29.1); $\operatorname{Ndim}(H)$ is the largest size of a shattered set (Definition 29.2). One-versus-All builds $T(\bar h)(x) = \operatorname{argmax}_i h_i(x)$ from $k$ binary classifiers, the smaller label on ties; a general reduction applies a rule $r : \{0,1\}^l \to [k]$ to $l$ binary classifiers; the linear class $H_\Psi$ predicts $\operatorname{argmax}_i\langle w, \Psi(x, i)\rangle$ for a class-sensitive feature map $\Psi : X \times [k] \to \mathbb{R}^d$ (29.1). The class of §29.4 has labels $P_f(X) \cup \{\ast\}$, the finite and cofinite subsets of $X$ plus a special label, and hypotheses $h_A(x) = A$ if $x \in A$ and $\ast$ otherwise; $A_{good}$ returns $h_\emptyset$ on an all-$\ast$ sample and $A_{bad}$ returns $h_{\{x_1, \dots, x_m\}^c}$.

Formalization targets

Goal: Theorem 29.3

There are absolute constants $C_1, C_2 > 0$ such that every class $H \subseteq Y^X$ with $\operatorname{Ndim}(H) = d$ satisfies

$$C_1\frac{d + \log(1/\delta)}{\epsilon^2} \le m^{UC}_H(\epsilon,\delta),\ m_H(\epsilon,\delta) \le C_2\frac{d\log k + \log(1/\delta)}{\epsilon^2}, \qquad C_1\frac{d + \log(1/\delta)}{\epsilon} \le m^{\mathrm{real}}_H(\epsilon,\delta) \le C_2\frac{d\log(kd/\epsilon) + \log(1/\delta)}{\epsilon},$$

the upper bounds by every ERM learner and the lower bounds for small $\epsilon, \delta$ and $d \ge 2$, in the format of Mission IV's Theorem 6.8.

Milestones

Lemma 29.4 (Natarajan: $|H| \le |X|^{\operatorname{Ndim}(H)}k^{2\operatorname{Ndim}(H)}$); Lemma 29.5 (the Natarajan dimension of One-versus-All is $O(kd\log(kd))$); Theorem 29.7 ($\operatorname{Ndim}(H_\Psi) \le d$); Claim 29.9(1) ($A_{good}$ needs $\frac1\epsilon\log\frac1\delta$ examples); Claim 29.9(2) ($A_{bad}$ fails with constant probability on $(|X|-1)/(6\epsilon)$ examples). Further items: the equality $\operatorname{Ndim} = \operatorname{VCdim}$ for two classes, and Lemma 29.6 for general reductions.

Significance

Theorem 29.3 is the multiclass fundamental theorem of Natarajan (1989) and Ben-David, Cesa-Bianchi, Haussler and Long (1995): finite Natarajan dimension characterizes multiclass learnability, and the sample complexity is linear in it, with the dependence on $k$ confined to logarithms. Natarajan's lemma is the combinatorial core, and the dimension bounds of §29.3 are what make the theorem usable: a One-versus-All scheme over a class of VC dimension $d$ costs $\tilde O(kd)$, and a linear multiclass predictor costs at most its number of parameters, so the multivector construction of Chapter 17 is learnable with $\tilde O(nk/\epsilon^2)$ examples. Claim 29.9 is a genuine phenomenon of Daniely, Sabato, Ben-David and Shalev-Shwartz (2011): in multiclass classification the choice of ERM matters, and the equivalence "learnable iff uniform convergence" of the binary theory is false, which is why Conjecture 29.10 about good ERMs is open in the form the chapter states it.

Difficulty

The equality with the VC dimension for two labels is a direct comparison of the two shattering definitions. Natarajan's lemma is a Sauer-type induction on $|X|$, in which a shattered set must be produced from two hypotheses that differ at a point; the exercise-level proof of the book becomes a careful double induction formally. Theorem 29.3's upper bounds follow the binary proof of Chapter 28 with Natarajan's lemma in place of Sauer's, hence Massart's lemma and Theorem 26.5 for the agnostic case and the double-sample argument for the realizable case; the lower bounds reduce to the binary ones by embedding a binary class into a multiclass one on a shattered set. These are long formal developments, and the theorem is stated with unspecified constants for that reason. Lemmas 29.5 and 29.6 are counting: a shattered $C$ has $2^{|C|} \le |H_C| \le |(H_{bin})_C|^k$, Sauer's lemma bounds the right side by $\big(\sum_{i \le d}\binom{|C|}{i}\big)^{k}$, and the resulting inequality is solved. For Lemma 29.5's printed $3kd\log(kd)$ this fails only at $(k, d) = (2, 1), (3, 1)$. There a shattered set splits by the label pair $\{f_0(x), f_1(x)\}$ into parts shattered by $\{B \setminus A : A, B \in H_{bin}\}$ (pairs $\{0, b\}$) or by $H_{bin}$ (other pairs). The first class has at most $31$ traces on $5$ points. Theorem 29.7 maps a shattered set into $\mathbb{R}^d$ by $\rho(x) = \Psi(x, f_0(x)) - \Psi(x, f_1(x))$, up to sign, and shows the image is shattered by homogeneous halfspaces; the tie-breaking rule decides which sign and which halfspace convention to use. Claim 29.9(1) is the bound $(1-\epsilon)^m \le \delta$; Claim 29.9(2) needs only that at most $(d-1)/2$ of the $d-1$ light points appear in the sample, an event of probability at least $1/3$ by Markov's inequality when $m \le (d-1)/(6\epsilon)$, which exceeds the claimed $e^{-1}/6$.

Formalization scope

Labels are an arbitrary finite type, shattering and the Natarajan dimension are stated with witnesses $f_0, f_1$ defined on all of $X$, and the dimension is a supremum in $\mathbb{N} \cup \{\infty\}$. The multiclass 0–1 loss, the ERM property, agnostic PAC learnability and uniform convergence are Mission I's generic notions; the realizable multiclass PAC property is defined here in the shape of Definition 3.1 with $D(\{h \ne f\})$ as the error, since Mission I's binary version is $\{0,1\}$-specific. Theorem 29.3 is stated exactly as Mission IV states Theorem 6.8, with existential constants, upper bounds for every ERM learner of a nonempty measurable class with the countable-approximation property (the measurability device of Remark 3.1), and lower bounds for $\epsilon < \epsilon_0$, $\delta < \delta_0$, $d \ge 2$. Argmax predictors, both One-versus-All and $H_\Psi$, break ties towards the smallest label; the book states this rule for One-versus-All, and some fixed rule is necessary for Theorem 29.7, since with arbitrary tie-breaking every function is an argmax predictor of the zero mapping. Lemmas 29.5 and 29.6 are stated per shattered set. Lemma 29.5 keeps the printed $3kd\log(kd)$, which is true although the book's step $|(H_{bin})_C| \le |C|^d$ fails for small $|C|$. Lemma 29.6 uses $2ld\log_2(2ld)$, which the counting supports, because the printed $3ld\log(ld)$ is false at $l = d = 1$. Theorem 29.3's uniform-convergence upper bound is stated for $d \ge 1$. At $d = 0$ the confidence term $\log(1/\delta)$ vanishes as $\delta \to 1$, the bound reaches $m = 1$, and a single example is not representative. The class of §29.4 has labels Option of the subtype of finite-or-cofinite sets, with the discrete σ-algebra, and the two ERMs are predicates fixing the output on all-$\ast$ samples; Claim 29.9(1) is stated for countable $X$ with measurable singletons and Claim 29.9(2) for finite $X$ of size at least $2$, with the proof's own distribution, $h_\emptyset$ as target, and every $\epsilon \in (0, 1/2)$ in place of the book's unspecified constant $a$.

Not stated: Corollary 29.8 (its lower bound $(k-1)(n-1)$ is cited, not proved), Conjecture 29.10, the exercises.

Selected references

• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 29. doi:10.1017/CBO9781107298019
• B. K. Natarajan, On learning sets and functions, Machine Learning 4, 1989. doi:10.1007/BF00114804
• S. Ben-David, N. Cesa-Bianchi, D. Haussler, P. M. Long, Characterizations of learnability for classes of {0, …, n}-valued functions, Journal of Computer and System Sciences 50(1), 1995. doi:10.1006/jcss.1995.1008
• D. Haussler, P. M. Long, A generalization of Sauer's lemma, Journal of Combinatorial Theory A 71(2), 1995. doi:10.1016/0097-3165(95)90001-2
• A. Daniely, S. Sabato, S. Ben-David, S. Shalev-Shwartz, Multiclass learnability and the ERM principle, COLT 2011; Journal of Machine Learning Research 16, 2015.
• A. Daniely, S. Sabato, S. Shalev-Shwartz, Multiclass learning approaches: a theoretical comparison with implications, NIPS 2012.

Motivation

Chapter 6 stated the fundamental theorem of statistical learning: a binary class is learnable if and only if its VC dimension is finite, with sample complexity $\Theta((d + \ln(1/\delta))/\epsilon^2)$ in the agnostic case and $\Theta((d\ln(1/\epsilon) + \ln(1/\delta))/\epsilon)$ in the realizable case. Chapter 28 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), proves it. The agnostic upper bound is obtained from the Rademacher machinery of Chapter 26 with Sauer's lemma and Massart's lemma, up to a $\log(d/\epsilon)$ factor that only chaining removes (28.1). The agnostic lower bound comes in two parts: a two-point construction giving $m \ge 0.5\log(1/(4\delta))/\epsilon^2$, and a $d$-point construction giving $m \ge d/(512\epsilon^2)$ at confidence $1/8$, whose heart is Lemma 28.1, the optimality of the Maximum-Likelihood rule against the family of noisy distributions $D_b$. The realizable upper bound is proved through $\epsilon$-nets: with $m \ge \frac8\epsilon(2d\log(16e/\epsilon) + \log(2/\delta))$ examples a random sample hits every set of measure at least $\epsilon$ in the class (Theorem 28.3), so any hypothesis consistent with the sample has error below $\epsilon$. Mission IV states these bounds with unnamed constants; this mission gives the chapter's explicit ones.

Setting

$H$ is a class of functions $X \to \{0,1\}$ with the 0–1 loss and $\operatorname{VCdim}(H) = d$. For the upper bound, $A = \{(\mathbb{1}[h(x_i) \ne y_i])_i : h \in H\}$ is the loss set of a sample and $R(A)$ its Rademacher complexity. For the lower bounds, $C = \{c_1, \dots, c_d\}$ is a set shattered by $H$ and, for $b \in \{\pm1\}^d$ and $\rho \in (0,1)$, $D_b$ draws $c_i$ uniformly and labels it $b_i$ with probability $(1+\rho)/2$; for $d = 1$ these are the distributions $D_\pm$ of §28.2.1. The Maximum-Likelihood rule $A_{ML}$ predicts at each $c_i$ the majority of the labels seen at $c_i$. An $\epsilon$-net for $H$ with respect to $D$ is a sample meeting every $h \in H$ with $D(h) \ge \epsilon$ (Definition 28.2).

Formalization targets

Goal: Theorem 28.3

Let $\operatorname{VCdim}(H) = d$, $\epsilon \in (0,1)$, $\delta \in (0, 1/4)$ and $m \ge \frac8\epsilon\big(2d\log\frac{16e}{\epsilon} + \log\frac2\delta\big)$. Then with probability at least $1 - \delta$ over $S \sim D^m$, $S$ is an $\epsilon$-net for $H$.

Milestones

The two-sided deviation bound of §28.1 ($|L_D(h) - L_S(h)| \le 2\sqrt{(8d\log(em/d) + 2\log(4/\delta))/m}$ uniformly over $H$); the lower bound $m(\epsilon,\delta) \ge 0.5\log(1/(4\delta))/\epsilon^2$ of §28.2.1; Lemma 28.1; the lower bound $m(\epsilon, 1/8) \ge d/(512\epsilon^2)$ of §28.2.2; the realizable upper bound of §28.3 (ERM has error at most $\epsilon$ with probability $1 - \delta$ for the sample size of Theorem 28.3). Further items: the Rademacher bound $R(A) \le \sqrt{2d\log(em/d)/m}$, the explicit uniform-convergence sample complexity of §28.1, and the expectation lower bound $\rho/4$ of §28.2.2.

Significance

These are the theorems that make the VC dimension the right measure of learnability, with constants. The upper bounds show what the abstract machinery of Missions II, IV, XX buys when instantiated: Sauer plus Massart plus Theorem 26.5 gives the agnostic rate, and the double-sample symmetrization plus Sauer gives the realizable rate, sharper by a factor $1/\epsilon$ because $\epsilon$-nets need only one-sided control. The lower bounds are the No-Free-Lunch argument refined to quantify $\epsilon$ and $\delta$: the two-point distribution shows that confidence costs $\log(1/\delta)/\epsilon^2$, and the $d$-point family with Lemma 28.1 shows that the dimension costs $d/\epsilon^2$, through the exact optimality of majority voting and a binomial anti-concentration bound. Theorem 28.3 is also the basic $\epsilon$-net theorem of Haussler and Welzl, a result of independent importance in computational geometry.

Difficulty

The Rademacher bound is Sauer's lemma (Mission IV) plus Massart's lemma (Mission XX) with $\|a - \bar a\| \le \sqrt m$; the deviation bound is Theorem 26.5 applied to $\ell$ and $-\ell$ with a union bound; the explicit sample complexity is Lemma A.2, $x \ge 4a\log(2a) + 2b \Rightarrow x \ge a\log x + b$, which a formal proof must establish (the tangent inequality for $\log$ at $2a$). The two-point lower bound requires the binomial lower-tail estimate of Lemma B.11 and the algebra $\frac12(1 - \sqrt{1 - \sqrt{4\delta}}) \ge \delta$, valid for $\delta < 1/4$, the only nonvacuous range. Lemma 28.1 is a conditioning argument: fixing the instance indices and the labels off $c_i$, the contribution of $c_i$ is minimized by predicting the more likely $b_i$ given the labels at $c_i$, which is the majority; the formal proof must decompose the product measure $D_b^m$ over the positions $r$ with $x_r = c_i$. The expectation bound $\rho/4$ then needs Lemma B.11 again, $1 - e^{-a} \le a$, Jensen for $\sqrt{\cdot}$ and $\mathbb{E}[n_i] = m/d$, and the probability bound $1/8$ follows by Mission III's reverse Markov inequality with $\rho = 8\epsilon$. Theorem 28.3 is the double-sample argument: Claim 1 ($P[S \in B] \le 2P[(S,T) \in B']$, via a Chernoff bound that only needs $m\epsilon \ge 2\log 2$), Claim 2 (symmetrization by a random half, $P[(S,T) \in B'] \le e^{-\epsilon m/4}\tau_H(2m)$), Sauer's lemma, and Lemma A.2 once more. The realizable upper bound applies Theorem 28.3 to the error sets $\{x : h(x) \ne f(x)\}$, a class of the same VC dimension.

Formalization scope

All objects are those of the earlier missions: risks, samples and learners from Mission I, vcDim and the countable-approximation property PointwiseSeparable from Mission IV (the measurability device for suprema over $H$, used wherever a symmetrization or Rademacher argument is invoked), condLaw from Mission XIV for the distributions $D_b$, and rademacher, evalSet, lossClass from Mission XX. Probability statements bound the outer measure of the failure event under iidLaw. The Rademacher and deviation items require $m > d + 1$, the range in which Mission IV states Sauer's lemma in the form $(em/d)^d$; the explicit sample complexity of §28.1 implies this range, since its first term $432d\log(64d/\epsilon^2)/\epsilon^2$ dominates the possibly negative $8d\log(e/d)$, and Lemma A.2 holds for any real $b$, so the book's constants are used verbatim. The lower bounds take a shattered set as an injective $c : \mathrm{Fin}\ d \to X$ with the shattering property written out, use $D_b$ as condLaw of the uniform law on $C$, and state the excess risk against $\min_{h \in H}L_{D_b}(h)$ as $\exists h \in H$ with $L(h) + \epsilon \le L(A(S))$, or as a real infimum over $H$ in the expectation item; no measurability of the learner is needed because $D_b^m$ is atomic. Lemma 28.1 compares the sums over $b$ of the expected risks, the common term $\min_h L_{D_b}$ cancelling, for every majority rule with arbitrary tie-breaking. Theorem 28.3 and the realizable bound are stated for $\delta \in (0, 1/4)$, the theorem's own range; the realizable bound is the inner clause of Mission I's IsPACWith on that range rather than a sample-complexity function, since the theorem does not cover $\delta \ge 1/4$ with its formula.

Not stated: the realizable lower bound (an exercise), the remark that chaining removes the logarithm in (28.1), and the intermediate claims of the proof of Theorem 28.3 as separate items.

Selected references

• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 28. doi:10.1017/CBO9781107298019
• V. N. Vapnik, A. Ya. Chervonenkis, On the uniform convergence of relative frequencies of events to their probabilities, Theory of Probability and its Applications 16(2), 1971. doi:10.1137/1116025
• A. Blumer, A. Ehrenfeucht, D. Haussler, M. K. Warmuth, Learnability and the Vapnik-Chervonenkis dimension, Journal of the ACM 36(4), 1989. doi:10.1145/76359.76371
• D. Haussler, E. Welzl, ε-nets and simplex range queries, Discrete and Computational Geometry 2, 1987. doi:10.1007/BF02187876
• M. Anthony, P. L. Bartlett, Neural Network Learning: Theoretical Foundations, Cambridge University Press, 1999. doi:10.1017/CBO9780511624216