Combinatorics

Motivation

How many times can $n$ points and $t$ lines in the plane meet? The question is the prototype of incidence geometry, and the answer controls a long list of problems in discrete and computational geometry: the number of lines rich in points, the number of distinct distances or unit distances among $n$ points, the complexity of arrangements, and sum–product estimates in additive combinatorics. Erdős asked for the order of magnitude when $t = n$ and conjectured that the answer is $n^{4/3}$; Erdős and Purdy asked for the matching bound on the number of lines containing at least $k$ of the points.

Szemerédi and Trotter settled both questions in Extremal Problems in Discrete Geometry (Combinatorica 3 (1983) 381–392, doi:10.1007/BF02579194). Their principal theorem bounds the number of point–line incidences by $c_1 n^{2/3} t^{2/3}$ over the whole range $\sqrt n \le t \le \binom n2$, and the same paper derives from it the Erdős–Purdy bound on $k$-rich lines, a version of Dirac's conjecture (proved independently by Beck, Combinatorica 3 (1983)), and a bound on the number of sequences of line densities.

Timeline.

• Erdős conjectures $O(n^{4/3})$ incidences for $n$ points and $n$ lines, and shows by a grid construction that this order would be sharp.
• 1983: Szemerédi and Trotter prove the bound $c_1 n^{2/3} t^{2/3}$ for $\sqrt n \le t \le \binom n2$, with $c_1 = 10^{60}$, by a minimal-counterexample argument and a covering lemma for squares from their earlier paper.
• 1990: Clarkson, Edelsbrunner, Guibas, Sharir and Welzl give a second proof by cuttings, with a far smaller constant (Discrete Comput. Geom. 5 (1990) 99–160).
• 1997: Székely derives the bound in a few lines from the crossing lemma (Combin. Probab. Comput. 6 (1997) 353–358).

Setting

Work in the Euclidean plane $\mathbb R^2$, written Plane in the Lean development. A line is an affine subspace $l \subseteq \mathbb R^2$ whose direction space has dimension one (IsLine l). Let $\mathcal P$ be a finite set of $n$ points and $\mathcal L$ a finite family of $t$ distinct lines. The number of incidences is

$$I(\mathcal P, \mathcal L) = \#\{(p, l) \in \mathcal P \times \mathcal L : p \in l\},$$

written incidences P L. The degree $d_i$ of a point $p_i$ is the number of lines of $\mathcal L$ through it (degree L p), and the density $y_j$ of a line $l_j$ is the number of points of $\mathcal P$ on it (density P l); so $I = \sum_i d_i = \sum_j y_j$.

For the covering lemma, coordinate axes are fixed and a square is a closed axis-parallel square $Q(a,b,s) = [a, a+s] \times [b, b+s]$ with side $s > 0$ (closedSquare (a, b, s)); its interior is the open square $(a, a+s) \times (b, b+s)$ (openSquare). A square contains the points of $\mathcal P$ in the closed square, and a family of squares covers the points lying in at least one of them.

Formalization targets

Goal: Theorem 1 (p. 381, restated and proved on p. 383)

There is an absolute constant $c_1$ such that for every finite point set $\mathcal P$ with $|\mathcal P| = n$ and every finite family $\mathcal L$ of $t$ distinct lines,

$$\sqrt n \le t \le \binom n2 \quad\Longrightarrow\quad I(\mathcal P, \mathcal L) \le c_1\, n^{2/3}\, t^{2/3}.$$

The goal leaves $c_1$ unspecified. The paper's proof gives $c_1 = 10^{60}$, and later proofs give much smaller values; any improvement of the constant still proves this statement.

Milestones, in the order the proof uses them

1. Section 3, display on p. 383. Two distinct lines meet in at most one point, so the number of good intersections is at most the number of pairs of lines:

$$\sum_{i} \binom{d_i}{2} \le \binom t2, \qquad \frac{I^2}{2n} - \frac I2 \le \frac{t^2}{2}.$$

2. Section 3, inequality (1), p. 384. $0.6\,x + (1-x)^{2/3} \le 1$ for $0 < x \le 1/2$.
3. Section 3, inequality (5), p. 385. $x^{2/3} + (1-x)/100 + 2^{-1/3}(1-x)^{2/3} \le 1$ for $0 < x \le 0.1$, and the reverse strict inequality holds somewhere in $(0.1, 0.2)$.
4. Section 3, display on p. 387. With $M = 10^{10}$, $2^{i/3}(1 - 2/M)^{4i/3} \ge 200/((0.1)^{1/3} 2^{2/3})$ for every integer $i \ge 30$.
5. Section 2, Lemma (covering lemma), p. 382. For integers $1 \le r_1 \le n$ and $r_2 \ge 256 r_1$, every set of $n$ points is covered, to at least $n/16$ of its points, by a family of squares with pairwise disjoint interiors, each containing between $r_1$ and $r_2$ of the points.

Significance

The result. The bound $n^{2/3} t^{2/3}$ is sharp up to the constant throughout the range $\sqrt n \le t \le \binom n2$, as integer-grid configurations show. Outside that range the trivial bounds $n + t^2$ and $t + n^2$ take over. Theorem 1 is the source of the $O(n^2/k^3)$ bound on $k$-rich lines (the paper's Theorem 2), of Beck's theorem (Theorem 3), and, through them, of the unit-distance bound $O(n^{4/3})$, of the Elekes sum–product estimate and of many algorithmic bounds on arrangements. It is the first nontrivial case of the polynomial-partitioning incidence theory developed since 2010.

Formalizing it. The theorem has been proved, and reproved in several ways, for four decades. To the best of the mission's knowledge Mathlib has no statement of it, of the crossing lemma, or of any point–line incidence bound in the Euclidean plane. This mission produces a checked statement of the theorem with lines as genuine one-dimensional affine subspaces and an absolute constant. It also produces checked statements of the auxiliary facts the 1983 proof uses. A complete proof may follow the original argument, the cutting argument or Székely's crossing-lemma argument; any of them closes the goal.

Difficulty

Counting pairs of lines through common points (milestone 1) gives only $I \lesssim n^{1/2} t + n$, and its dual gives $I \lesssim t^{1/2} n + t$. These Cauchy–Schwarz bounds use only the fact that two lines meet at most once, a property shared by lines in finite projective planes, where the incidence count genuinely reaches order $n^{3/2}$. Any proof of the $n^{2/3} t^{2/3}$ bound must therefore use a property of the real plane that the finite geometries lack: order, continuity, or the planarity of drawings. Szemerédi and Trotter use it through a covering lemma for axis-parallel squares, whose proof is only cited in the paper ([7]). The remaining difficulty is keeping the constants of a multi-stage minimal-counterexample argument under control.

Formalization scope

The plane is EuclideanSpace ℝ (Fin 2). A line is an AffineSubspace ℝ Plane whose direction has Module.finrank equal to $1$. Every statement requires IsLine of each member of $\mathcal L$, so neither the whole plane nor a single point counts as a line. The points form a Finset Plane and the lines a Finset (AffineSubspace ℝ Plane), which makes the $t$ lines distinct. Incidences, degrees and densities are Finset.filter cardinalities under classical decidability. Powers $n^{2/3}$, $t^{2/3}$ are Real.rpow of the counts cast to $\mathbb R$, and $\binom n2$ is Nat.choose.

In the goal, the constant $c_1$ is quantified before the points and the lines. The form "for every configuration there is a $c_1$" is trivially true (take $c_1 = I + 1$) and is not this theorem. Both ends of the range $\sqrt n \le t \le \binom n2$ are kept exactly: without the lower end, a single line through $n$ collinear points has $n$ incidences, more than $c_1 n^{2/3}$ for large $n$.

The goal follows the wording of p. 381 ("at most"). The restatement on p. 383 says "less than", which fails at $n = t = 0$ and is equivalent for $n \ge 1$ after doubling $c_1$. The covering lemma is stated with the added non-degeneracy hypotheses $1 \le r_1 \le n$. As printed it fails when $0 < n < r_1$ (no square can hold $r_1$ points), and when $r_1 = r_2 = 0$ with $n > 0$.

A full development needs a real-plane incidence toolkit: a crossing lemma or a cutting lemma, or the covering lemma with its quadtree proof. That toolkit is reusable for $k$-rich lines, Beck's theorem, unit distances and sum–product bounds, and contributions of such infrastructure as separate theorems are welcome. The three numerical milestones are self-contained real-analysis exercises.

Selected references

• E. Szemerédi, W. T. Trotter, Jr., Extremal problems in discrete geometry, Combinatorica 3 (1983) 381–392. https://doi.org/10.1007/BF02579194
• E. Szemerédi, W. T. Trotter, Jr., A combinatorial distinction between the Euclidean and projective planes, European J. Combin. 4 (1983) 385–394. https://doi.org/10.1016/S0195-6698(83)80036-5
• J. Beck, On the lattice property of the plane and some problems of Dirac, Motzkin and Erdős in combinatorial geometry, Combinatorica 3 (1983) 281–297. https://doi.org/10.1007/BF02579184
• K. L. Clarkson, H. Edelsbrunner, L. J. Guibas, M. Sharir, E. Welzl, Combinatorial complexity bounds for arrangements of curves and spheres, Discrete Comput. Geom. 5 (1990) 99–160. https://doi.org/10.1007/BF02187783
• L. A. Székely, Crossing numbers and hard Erdős problems in discrete geometry, Combin. Probab. Comput. 6 (1997) 353–358. https://doi.org/10.1017/S0963548397002976

Motivation

Every physical or engineering model built from linear relations mixes two kinds of numbers. Some coefficients are exact — the $\pm 1$ entries recording Kirchhoff's current and voltage laws in an electrical network, or the incidence structure of a mechanical linkage — because they come from a topological or combinatorial fact, not a measurement. Others are physical parameters: resistances, masses, spring constants, reaction rates. These are known only approximately, and different parameters are, for modeling purposes, independent of one another. Classical linear algebra treats every entry of a coefficient matrix alike, so it cannot express this distinction, and a numerical computation on a matrix with noisy parameter entries can accidentally hit a non-generic coincidence — a determinant that would vanish only for a measure-zero set of parameter values, but that plain Gaussian elimination has no way to certify is not actually structurally forced to vanish. Murota and collaborators (see the bibliographical notes to chapter 12; the underlying theory is developed at length in Murota's Matrices and Matroids for Systems Analysis, 2000) formalized this distinction through mixed matrices, and showed that their key structural questions — is the matrix nonsingular, and what is its rank — reduce to a combinatorial optimization problem solvable by the discrete convex analysis this book develops. This mission formalizes that reduction and its capstone consequence, a generalization of the classical König–Egerváry theorem.

Setting

Fix two fields $K \subseteq F$: typically $K = \mathbb{Q}$ and $F$ a field large enough to hold every number in the problem. A family $t_1, \dots, t_m \in F$ is algebraically independent over $K$ if no nonzero polynomial with coefficients in $K$ vanishes at $(t_1, \dots, t_m)$ — informally, the $t_i$ behave as free, unconstrained parameters relative to $K$. Fix finite row and column index sets $R$ and $C$. A matrix $A = (A_{ij})_{i \in R, j \in C}$ over $F$ is a mixed matrix with respect to $(K, F)$ if it decomposes as

$$A = Q + T$$

where $Q = (Q_{ij})$ has every entry in $K$, and $T = (T_{ij})$ has entries in $F$ whose nonzero values, taken together as one family, are algebraically independent over $K$. $Q$ models the exact, structural part of the system; $T$ models the independent physical parameters. For $I \subseteq R$ and $J \subseteq C$, write $A[I,J]$ for the submatrix with rows $I$ and columns $J$. The rank of $A$ is its rank over $F$ — equivalently, the size of the largest nonvanishing-determinant square submatrix. Write $\rho(I,J) = \operatorname{rank} Q[I,J]$, $\tau(I,J) = \operatorname{rank} T[I,J]$, and $\gamma(I,J)$ for the number of rows of $I$ that contain a nonzero entry of $T$ in some column of $J$. A mixed polynomial matrix $A(s) = Q(s) + T(s)$ is the same decomposition applied entrywise to matrices whose entries are polynomials in an indeterminate $s$ (used to model the Laplace- or $z$-transform variable of a linear time-invariant system): $Q(s)$ has every coefficient of every entry in $K$, and the coefficients of $T(s)$'s entries, taken together, are algebraically independent over $K$.

Formalization targets

$$\textbf{Theorem 12.9 (goal).}\quad \text{For a mixed matrix } A=Q+T,\ \exists\, I \subseteq R,\ J \subseteq C:\quad |I|+|J|-\operatorname{rank} Q[I,J] = |R|+|C|-\operatorname{rank} A \ \ \text{and}\ \ \operatorname{rank} T[I,J] = 0.$$

This is the König–Egerváry theorem for mixed matrices: a combinatorial certificate of $A$'s rank deficiency, generalizing the classical theorem relating the maximum matching size of a bipartite graph (equivalently, the rank of a 0-1 matrix) to a minimum vertex cover. It is reached via three supporting results, each a genuine theorem in its own right: Proposition 12.6 (nonsingularity of $A$ reduces to nonsingularity of a $Q$-part and a $T$-part on complementary index splits), Theorem 12.7 (the resulting rank max-formula), and Theorem 12.8 (the three dual min-formulas Theorem 12.9 is extracted from). Theorem 12.13 extends the max-formula to the degree of the determinant of a mixed polynomial matrix.

Significance

The result itself. Theorem 12.9 gives a certificate, not just a number: a pair $(I,J)$ that simultaneously proves the exact numeric rank contribution of $Q$ and exhibits a submatrix of $T$ that vanishes identically. Because $\rho$ (via Gaussian elimination on $Q$) and $\gamma$, $\tau$ (via maximum bipartite matching on $T$'s nonzero pattern) are each individually cheap to evaluate, and the min-max structure of Theorem 12.8 is exactly the kind of problem Edmonds's matroid intersection theorem (a special case of this book's Theorem 4.18) and this book's discrete convexity machinery solve efficiently, the whole rank computation for a mixed matrix — and hence the generic solvability test for a physical system modeled by one — is polynomial-time, despite Theorem 12.7's formula naively ranging over exponentially many index-set pairs.

Formalizing it. All five results in this mission are proved in the source text (this is textbook, not open, mathematics). What formalization adds is a machine-checked confirmation that the genericity hypothesis — "the nonzero entries of $T$ are algebraically independent" — is precisely what the printed proofs use, expressed through Mathlib's own AlgebraicIndependent rather than an informal paraphrase such as "generic" or "random" values, which would be either meaningless or a different (probabilistic) condition.

Difficulty

The naive approach to testing whether $A = Q+T$ is nonsingular is to expand $\det A$ directly and check whether the resulting expression, as a polynomial in $T$'s free parameters, is the zero polynomial. This is exactly what genericity is supposed to let you avoid: Proposition 12.6's proof observes that the Laplace-type expansion $\det A = \sum_{|I|=|J|} \pm \det Q[I,J] \cdot \det T[R\setminus I, C\setminus J]$ has no cancellation between distinct terms, precisely because the nonzero entries of $T$ are algebraically independent — a coincidental cancellation would be a nontrivial polynomial relation among free parameters, which cannot happen. This turns a determinant computation with symbolic entries into a purely combinatorial search over row/column splits, each of whose two pieces is checked in the "easy" arithmetic appropriate to it (numeric determinant for $Q$, a nonzero-pattern-only matching argument for $T$). Missing this point — e.g. by treating $T$'s entries as merely "distinct" or "typically nonzero" rather than algebraically independent — reintroduces exactly the cancellation risk the theorem is built to rule out.

Formalization scope

Row and column index sets $R$, $C$ are general finite types (Fintype, with DecidableEq where needed for Finset operations), not fixed to $\mathrm{Fin}\ n$. No constant appears in any statement in this mission — every quantity (ranks, cardinalities, $\gamma$) is instance-dependent, so rule 7's explicit-constant obligation does not apply here. "Nonsingular" for a (possibly rectangular, cross-type-indexed) submatrix $M[I,J]$ is formalized as I.card = J.card together with rank M[I,J] = I.card (full rank) rather than via Matrix.det, because Mathlib's determinant requires both index sets to be the same Lean type, which I : Finset R and J : Finset C are not in general even when equinumerous; this coincides with ordinary nonsingularity whenever the ambient matrix is genuinely square. The degree of the determinant of a submatrix in Theorem 12.13 is computed the same way, via an arbitrary reindexing bijection between the row- and column-index subtypes — a choice that changes the determinant by at most a sign and hence never changes its degree. A formalization that replaced the genericity hypothesis on $T$ with mere distinctness of its nonzero entries would admit spurious cancellations in the determinant expansion and would not prove Proposition 12.6 or any of its consequences; AlgebraicIndependent K is the precise, non-trivializing condition the book's proofs use. This chapter is self-contained: no definitions from any other mission in this series are imported. Reusable beyond this mission: MatrixSubRank, IsNonsingularSub, and SubDegDet apply to any pair of matrices over any field, not only to mixed-matrix decompositions.

Selected references

• Murota, K. Discrete Convex Analysis. SIAM, 2003. DOI: 10.1137/1.9780898718508. (Chapter 12.)
• Murota, K. Matrices and Matroids for Systems Analysis. Springer, 2000.
• Murota, K. "Systems Analysis by Graphs and Matroids: Structural Solvability and Controllability." Springer, 1987.
• König, D. "Gráfok és mátrixok" (Graphs and matrices). Matematikai és Fizikai Lapok 38, 1931, 116–119.
• Egerváry, J. "Matrixok kombinatorius tulajdonságairól" (On combinatorial properties of matrices). Matematikai és Fizikai Lapok 38, 1931, 16–28.

Motivation

Chapters 6 through 8 built M-convex and L-convex functions and their conjugacy theory as abstract combinatorial objects on the integer lattice. Chapter 9 grounds that theory in a setting every reader already knows: network flows. The chapter's throughline is that the classical minimum cost flow problem — flows bounded by simple arc capacities, with a single linear cost — is a shadow of a much richer submodular flow problem, in which the constraint on a flow's boundary is not "equal a fixed supply vector" but "lie in the base polyhedron of an arbitrary submodular set function." This mission formalizes the feasibility theory for both problems and its capstone: a max-flow min-cut theorem for submodular flows that specializes to the classical max-flow min-cut theorem exactly when the submodular function degenerates to a plain capacity function.

Setting

Let $G = (V, A)$ be a finite directed graph, with $\mathrm{tail}, \mathrm{head} : A \to V$ giving each arc's start and end vertex. The boundary of a flow $\xi : A \to \mathbb R$ is $\partial\xi(v) = \sum_{a : \mathrm{tail}(a) = v} \xi(a) - \sum_{a : \mathrm{head}(a) = v} \xi(a)$. For $X \subseteq V$, $\Delta^+X$ and $\Delta^-X$ are the arcs leaving and entering $X$. Given an upper capacity $\bar c : A \to \mathbb R \cup \{+\infty\}$ and lower capacity $\underline c : A \to \mathbb R \cup \{-\infty\}$, the cut capacity function is $\kappa(X) = \bar c(\Delta^+X) - \underline c(\Delta^-X)$. A submodular set function $\rho : 2^V \to \mathbb R \cup \{+\infty\}$ with $\rho(\emptyset) = \rho(V) = 0$ plays the same structural role as $\kappa$ but is arbitrary problem data rather than a derived quantity.

Formalization targets

Goal: Theorem 9.13 (max-flow min-cut for submodular flows)

For a feasible maximum submodular flow problem on a specified arc $a_0$: $\sup\{\xi(a_0) : \xi \text{ feasible}\} = \min\big(\bar c(a_0), \min_X\{\bar c(\Delta^-X) - \underline c(\Delta^+X \setminus \{a_0\}) + \rho(X) : a_0 \in \Delta^+X\}\big)$, a common value in $\mathbb R \cup \{+\infty\}$; if the data is integer valued and the value is finite, an integer-valued maximum flow exists.

Milestones: Proposition 9.2, Theorem 9.3, Theorem 9.10

Proposition 9.2: the cut capacity function $\kappa$ is always submodular — the fact that lets the classical minimum cost flow problem's feasibility be phrased in exactly the same base- polyhedron language as the general submodular flow problem. Theorem 9.3: a flow meeting the capacity constraint with boundary $x$ exists if and only if $x(X) \le \kappa(X)$ for all $X$ and $x(V) = 0$ — the classical case, and the direct predecessor of the goal's feasibility side. Theorem 9.10: the submodular flow problem is feasible if and only if $\bar c(\Delta^-X) - \underline c(\Delta^+X) + \rho(X) \ge 0$ for all $X$ — obtained from Theorem 9.3 via Edmonds's intersection theorem in the book's own proof, and the feasibility half of the goal's own maximum-flow variant.

Significance

The result itself. Theorem 9.13 is a genuine generalization of the max-flow min-cut theorem — one of the most-cited results in combinatorial optimization — to a submodularly constrained setting where the classical single-source-single-sink cut structure is replaced by an arbitrary vertex subset $X$ scored by a submodular function $\rho$ rather than merely counted. It specializes to the classical theorem when $\rho$ is the indicator of a fixed boundary value and the graph carries a single source/sink; the book's own derivation (dividing the target arc $a_0$ and reducing to Theorem 9.10's feasibility criterion) is exactly the kind of "one shared mechanism explains two theorems" result this whole book is organized around.

Formalizing it. A prior-art search (GET /theorems?q=max-flow min-cut) found two existing platform items for the classical theorem — LinearOptimization.max_flow_min_cut (Bertsimas & Tsitsiklis, single source/sink, plain capacities) and menger_directed_max_flow (Ford-Fulkerson, integer capacities) — both at a genuinely different, simpler generality (no lower capacity bounds, no submodular vertex-cut function, a fixed source/sink rather than an arbitrary marked arc). A further search (q=network flow) found a distinct mission formalizing Bertsimas & Tsitsiklis's uncapacitated network flow LP theory (basic feasible solutions, tree solutions, basis-matrix integrality) — a different technique (linear-algebraic, not cut-based) for a different problem (no capacities at all). Neither family is reused; this mission gives the first formal statement of submodular-flow feasibility and its max-flow min-cut theorem at the book's own generality.

Difficulty

The obvious shortcut — state only the value equality of Theorem 9.13 and drop the integrality clause — would misrepresent the theorem's own content: the equality of the extremal values follows from ordinary LP duality on the polyhedron $B(\kappa) \cap B(\rho)$ (arguably already within reach of chunk 04's Edmonds's intersection theorem machinery, as the book's own proof of the feasibility predecessor Theorem 9.10 uses exactly that), whereas the integer-flow existence half is the theorem's genuine combinatorial content, unique to the integer lattice. This chunk keeps both halves in every drafted theorem (Theorem 9.3, 9.10, and the goal) rather than only the polyhedral half.

A second, more structural difficulty governed this chunk's scope: BRIEF.md recommended Theorem 9.4 (the potential-optimality criterion) and its M-convex-cost specialization Theorem 9.14 as milestones, but both need a polyhedral convexity hypothesis on real-valued (or M-convex) functions over $\mathbb R^V$ that this series has never built — the identical scope boundary chunk 10 hit with Theorem 8.4. Rather than silently drop the polyhedral-convexity hypothesis (which would make the drafted statement unsound, since the theorem's hard direction genuinely needs it), this chunk selects only results — Proposition 9.2, Theorem 9.3, Theorem 9.10, Theorem 9.13 — that need no convexity apparatus of any kind, only the submodularity of $\kappa$/$\rho$ and elementary capacity-constraint feasibility.

Formalization scope

$V$ and $A$ are Fintypes with DecidableEq V (and DecidableEq A where a Finset.erase is needed); tail, head : A → V are plain functions, not a bundled graph structure. Every capacity- and cut-related quantity is WithTop ℝ-valued (ℝ ∪ {+∞}) throughout, with no EReal: a per-term check (documented in MODERATION_NOTES.md) confirms every subtraction this chunk needs is really an addition of two terms each individually in $\mathbb R \cup \{+\infty\}$, via a small new cast NegLowerToUpper : WithBot ℝ → WithTop ℝ. The base polyhedron $B(\rho)$ is stated by its defining inequalities rather than via a named polyhedral object (chunk 04's BasePolyhedron is ℤ^V-domain and does not fit chapter 9's real-vector- space setting). Not drafted: Theorem 9.4/9.14 (needs the real-domain polyhedral-convexity layer above), Theorem 9.6 (needs a real-domain polyhedral L-convexity notion for its dual-integrality half), Theorem 9.5/9.18/9.20/9.22 (negative-cycle criteria, an alternative non-potential certificate family, checked against platform prior art and found adjacent only), Propositions 9.23–9.25 (supporting technical facts), and Theorems 9.26–9.28 (the separate network- transformation technique of §9.6). A trivializing formalization would state Theorem 9.13's value equality with the integrality clause dropped, or would silently allow $\bar c$/$\underline c$ to range over all of EReal (permitting a nonsensical $\underline c(a) = +\infty$ upper- capacity-like lower bound); neither is done — both the integrality clause and the WithTop ℝ/WithBot ℝ type-level domain restriction are kept exactly as the book states them.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.

Motivation

Chapter 16 of Keller and Trotter's Applied Combinatorics (2017 Edition, CC BY-SA 4.0) is a survey of seven topics. Two of them are self-contained results with complete proofs on the page, and this mission formalizes both.

The first is the Lovász Local Lemma. It was introduced by Erdős and Lovász in 1975 to show that certain hypergraphs are 3-colourable (Erdős–Lovász 1975), and it has become a standard tool of the probabilistic method. The classical probabilistic argument shows that a random object has a property with probability close to one. The local lemma is different: it shows that a good object exists even when it is exceedingly rare, provided that each "bad" event depends on only a few of the others. It underlies lower bounds for Ramsey numbers such as $R(3,n) \ge c\,n^2/\ln^2 n$, the subject of Section 16.8. It also underlies results on colouring, satisfiability and Latin transversals, and the algorithmic version of Moser–Tardos (2010).

The second is the Gale–Ryser Theorem, proved independently by Gale (1957) and Ryser (1957). It decides when a zero–one matrix with prescribed row and column sums exists. Equivalently, it decides when a pair of sequences is the degree sequence of a bipartite graph. Its condition is a comparison in the dominance order on integer partitions.

Setting

A finite probability space is a finite set $\Omega$ with a function $P$ defined on all subsets, finitely additive, with $P(\emptyset) = 0$ and $P(\Omega) = 1$. Let $\mathcal F = (A_i)_{i \in \iota}$ be a finite family of events. For a subfamily $G \subseteq \iota$ write

$$\prod_{j \in G} \overline{A_j} = \bigcap_{j \in G} (\Omega \setminus A_j),$$

the event that every event of $G$ fails; for $G = \emptyset$ it is $\Omega$. Fix, for each $i$, a subfamily $N(i) \subseteq \iota \setminus \{i\}$. The event $A_i$ is independent of any event not in $N(i)$ if $P(A_i \mid \prod_{j\in G}\overline{A_j}) = P(A_i)$ for every $G$ with $i \notin G$ and $G \cap N(i) = \emptyset$. In the formalization this condition is IndepOutside μ A N i, written as

$$P\Big(A_i \cap \prod_{j\in G}\overline{A_j}\Big) = P(A_i)\,P\Big(\prod_{j\in G}\overline{A_j}\Big).$$

A partition of a positive integer $t$ is a non-increasing string $V = (v_1, \dots, v_m)$ of positive integers with sum $t$; $\mathcal P(t)$ is the set of partitions of $t$. It is partially ordered by $V \ge W$ iff $V$ is no longer than $W$ and every partial sum $v_1 + \dots + v_j$ is at least $w_1 + \dots + w_j$ (Dominates). $V$ covers $W$ when $V > W$ with nothing in between (Covers). The dual partition $V^d$ has $v_1$ entries, the $j$-th being the number of $i$ with $v_i \ge j$ (dual). A zero–one matrix with row sum string $R$ and column sum string $C$ is an $m \times n$ matrix with entries in $\{0,1\}$ whose row $i$ sums to $r_i$ and column $j$ to $c_j$ (IsZeroOneMatrixWithSums).

Formalization targets

Goal: the asymmetric local lemma (Lemma 16.14)

If $0 < x(i) < 1$ and $P(A_i) \le x(i)\prod_{j \in N(i)}(1 - x(j))$ for every $i$, then for every non-empty $G \subseteq \iota$

$$P\Big(\prod_{i \in G}\overline{A_i}\Big) \ge \prod_{i\in G}\big(1 - x(i)\big), \qquad\text{and}\qquad P\Big(\prod_{i\in\iota}\overline{A_i}\Big) > 0 .$$

Milestone: the symmetric local lemma (Lemma 16.15)

If $0 < p < 1$, $d \ge 1$, $P(A_i) \le p$, $|N(i)| \le d$ and $e\,p\,(d+1) < 1$, then

$$P\Big(\prod_{i\in\iota}\overline{A_i}\Big) \ge \Big(1 - \frac1{d+1}\Big)^{|\mathcal F|} > 0 .$$

Milestones: covers in $\mathcal P(t)$ and Gale–Ryser (Proposition 16.11, Theorem 16.12)

If $V$ covers $W$ in $\mathcal P(t)$, then $W$ arises from $V$ by moving one unit from a part $v_i$ to a later part $v_j$ (possibly a new part of size one), and all parts strictly between equal $v_i - 1$. For partitions $R, C$ of $t > 0$,

$$\exists\, M \in \{0,1\}^{m\times n} \text{ with row sums } R \text{ and column sums } C \iff R^d \ge C \text{ in } \mathcal P(t).$$

The Erdős–Ko–Rado bound of Theorem 16.8 enters as the published reference FamousTheorems.erdos_ko_rado.

Significance

The local lemma is the entry point to the probabilistic method's rare-event side. A formal statement in the book's form — finite spaces and the book's conditional notion of independence — is a reusable interface for formalizing its applications: Ramsey lower bounds, hypergraph colouring and $k$-SAT with bounded occurrences. The symmetric form is the version most applications call. Mathlib has no local lemma. The platform has a conditional-probability bound from an unrelated paper mission (Erdos390.WholePaper.finiteAsymmetricLocalLemma_conditionalBound), which bounds $P(A_i \cap \prod_{j\in s}\overline{A_j})$ with $0 \le x < 1$ and does not state the product lower bound for the joint failure.

Gale–Ryser is the prototype of margin problems for $\{0,1\}$-matrices and of degree-sequence characterizations (compare Erdős–Gallai for graphs). Formalizing it produces the dominance order, conjugate partitions and covering relations on sorted lists of positive integers. Mathlib has Nat.Partition but no dominance order or conjugate. None of these results is formalized on the platform. The results themselves are classical and proved; the work is formalizing the proofs.

Difficulty

For the local lemma, the naive induction on $|G|$ fails. Conditioning on the joint failure of a subfamily requires that failure to have positive probability, and that is only known after the inductive bound has been proved for smaller subfamilies. The induction must therefore carry the lower bound and the positivity of every smaller joint failure at once. It must also split each conditioning family into the part inside $N(i)$ and the part outside. The independence hypothesis controls only the part outside, and only through intersections of complements, not through arbitrary events.

For Gale–Ryser, necessity is an exchange argument, but sufficiency needs the fine structure of covers in the dominance order (Proposition 16.11): the case analysis of where the moved unit lands, including a new last part, and the fact that a maximal chain from $R^d$ down to $C$ exists. Converting the list-level statements into matrix constructions over Fin m × Fin n is the other main cost.

Formalization scope

• Probability space. Fintype Ω with DiscreteMeasurableSpace Ω and a measure μ with IsProbabilityMeasure μ; every subset is an event and probabilities are μ.real, as in the book's finite probability spaces.
• Family and neighbourhoods. The family is A : ι → Set Ω over a Fintype ι, so repeated events are allowed. Neighbourhoods are N : ι → Finset ι with i ∉ N i.
• Weights. 0 < x i < 1 is strict on both sides, as on the page.
• Independence. The conditional-probability equation is stated multiplicatively. This agrees with the book whenever the conditioning event has positive probability, and it is automatic otherwise.
• Excluded trivialization. The independence hypothesis is not full mutual independence of the family, which would make the product formula immediate. It is not pairwise independence either, under which the lemma is false. It is exactly the book's condition on intersections of complements.
• Explicit constant (Lemma 16.15). The book's displayed conclusion is misprinted: it mentions $\mathcal G$ and $x$, which are never introduced. The statement uses the bound the book's proof yields with $x(E) = 1/(d+1)$, namely $(1 - 1/(d+1))^{|\mathcal F|}$, with $|\mathcal F|$ = Fintype.card ι, together with positivity. Here $p$ and $d$ are real and $e$ is Real.exp 1.
• Partitions. Partitions are List ℕ, non-increasing with positive entries. Entries are 1-based through entry, and partial sums are (V.take j).sum.
• Dual partition. The page's rule "at least $n+1-j$" lists the conjugate in increasing order, and its example is misprinted (it sums to 40, not 42). The definition is the conjugate partition in non-increasing order, the only reading under which Theorem 16.12 holds.
• Matrices. Matrices are Matrix (Fin m) (Fin n) ℕ with entries in $\{0,1\}$.

Not included.

• The on-line colouring and antichain-partitioning results of Section 16.1 (Theorems 16.2, 16.4, 16.5) need a formal model of adaptive Builder/Assigner games.
• Theorem 16.9 (regular Markov chains) is stated without proof.
• Theorem 16.13 (van der Waerden) is stated without proof and followed by "Material will be added here".

Welcome contributions. Reusable infrastructure: a finite-space conditional-probability API, and the dominance order as a PartialOrder on sorted partitions linked to Nat.Partition.

Selected references

• M. T. Keller, W. T. Trotter, Applied Combinatorics, 2017 Edition, Chapter 16, pp. 315–330. https://www.appliedcombinatorics.org/
• P. Erdős, L. Lovász, Problems and results on 3-chromatic hypergraphs and some related questions, Infinite and Finite Sets, 1975. https://www.renyi.hu/~p_erdos/1975-34.pdf
• D. Gale, A theorem on flows in networks, Pacific J. Math. 7 (1957). https://doi.org/10.2140/pjm.1957.7.1073
• H. J. Ryser, Combinatorial properties of matrices of zeros and ones, Canad. J. Math. 9 (1957). https://doi.org/10.4153/CJM-1957-044-3
• R. A. Moser, G. Tardos, A constructive proof of the general Lovász Local Lemma, J. ACM 57 (2010). https://doi.org/10.1145/1667053.1667060
• P. Erdős, C. Ko, R. Rado, Intersection theorems for systems of finite sets, Quart. J. Math. 12 (1961). https://doi.org/10.1093/qmath/12.1.313

Motivation

Many counting questions ask for the number of objects up to symmetry: necklaces of coloured beads that may be rotated and flipped, musical scales up to transposition, chemical isomers up to the symmetries of a molecule, graphs on $n$ vertices up to relabelling. Counting all configurations and dividing by the number of symmetries fails, because some configurations are fixed by some symmetries. The standard tool for such questions is the enumeration theorem of Redfield (1927) and Pólya (1937), which turns the symmetry group into a generating function recording not only how many inequivalent configurations there are but how many use each colour a prescribed number of times.

This mission formalizes Chapter 15 of Keller and Trotter's Applied Combinatorics (2017 Edition), which develops the theorem from Burnside's Lemma for an undergraduate audience. The chapter's footnotes record the history: the orbit-counting lemma was known to Cauchy and Frobenius before it appeared in Burnside's book, and Redfield's paper anticipating Pólya's work was rediscovered only around 1960.

Setting

Let $S$ be a finite set with $|S| = r$. A permutation group $G$ of $S$ is a set of bijections $S \to S$ containing the identity and closed under composition and inverses. Every permutation $\pi$ splits $S$ into disjoint cycles; a fixed point is a cycle of length $1$. Write $j_k(\pi)$ for the number of cycles of length $k$, so that $j_1 + 2j_2 + \cdots + r j_r = r$. The cycle index of $G$ is the polynomial with rational coefficients

$$P_G(x_1, \ldots, x_r) = \frac{1}{|G|} \sum_{\pi \in G} x_1^{j_1(\pi)} x_2^{j_2(\pi)} \cdots x_r^{j_r(\pi)}.$$

For the eight symmetries $D_8$ of a square, $P_{D_8} = \tfrac18(x_1^4 + 2x_1^2x_2 + 3x_2^2 + 2x_4)$.

A coloring of $S$ with colours $c_1, \ldots, c_m$ is a map $f : S \to \{c_1, \ldots, c_m\}$; $\mathcal C$ denotes the set of all $m^r$ of them. A permutation acts on colorings by $\pi^*(f) = f \circ \pi^{-1}$, and two colorings are equivalent when some $\pi \in G$ carries one to the other. The weight of $f$ is the monomial $\prod_{s \in S} f(s) = c_1^{a_1} \cdots c_m^{a_m}$ in commuting variables, where $a_i$ counts the points coloured $c_i$. The pattern inventory is the polynomial whose coefficient of $c_1^{a_1}\cdots c_m^{a_m}$ is the number of equivalence classes of colorings using each $c_i$ exactly $a_i$ times.

More generally, for a finite group $G$ acting on a finite set $\mathcal C$, the orbit (equivalence class) of $C$ is $\langle C\rangle$, the stabilizer of $C$ is $\operatorname{stab}_G(C) = \{\pi \in G : \pi^*(C) = C\}$, and the fixed set of $\pi$ is $\operatorname{fix}_{\mathcal C}(\pi) = \{C : \pi^*(C) = C\}$.

Formalization targets

Milestone: Proposition 15.8

For a finite group $G$ acting on a finite set $\mathcal C$ and every $C \in \mathcal C$,

$$\sum_{C' \in \langle C\rangle} |\operatorname{stab}_G(C')| = |G|.$$

Milestone: Lemma 15.9 (Burnside's Lemma)

If $N$ is the number of equivalence classes of $\mathcal C$ induced by the action, then

$$N = \frac{1}{|G|}\sum_{\pi \in G} |\operatorname{fix}_{\mathcal C}(\pi)|.$$

Goal: Theorem 15.11 (Pólya's Enumeration Theorem)

For a permutation group $G$ of $S$ with $|S| = r$ and colours $c_1, \ldots, c_m$,

$$P_G\Bigl(\sum_{i=1}^m c_i,\ \sum_{i=1}^m c_i^2,\ \ldots,\ \sum_{i=1}^m c_i^r\Bigr) = \sum_{\langle f \rangle \in \mathcal C/\sim}\ \prod_{s \in S} f(s),$$

an identity of polynomials in $c_1, \ldots, c_m$ with rational coefficients: substituting power sums of the colours into the cycle index yields the pattern inventory.

Significance

The result itself. The theorem reduces counting inequivalent configurations to a computation with the cycle structure of the symmetry group, which is usually available in closed form (cyclic, dihedral and symmetric groups, and the pair group acting on edges of a graph). Setting all $c_i = 1$ gives the number of inequivalent colorings, $P_G(m, \ldots, m)$; reading off one coefficient answers refined questions such as the number of necklaces with a prescribed number of beads of each colour. The book applies it to musical scales, isomers of hydrocarbons and nonisomorphic graphs.

Formalizing it. Burnside's Lemma is in Mathlib (MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group), and so is the orbit–stabilizer theorem, so the two milestones are short; they are kept because they are the book's route to the goal. Mathlib has Equiv.Perm.cycleType but no cycle index and no pattern inventory, and no statement of Pólya's theorem was found on the platform (searches for Pólya, cycle index, pattern inventory, necklace and orbit counting, September 2026). The mission therefore produces the first machine-checked cycle index and Pólya enumeration theorem in this environment.

Difficulty

Burnside's Lemma counts orbits by fixed points; Pólya's theorem is a weighted Burnside lemma. Two steps separate them. First, the weight-enumerator of the colorings fixed by $\pi$ must be matched with the monomial of $\pi$ evaluated at power sums. This needs the cycles of $\pi$ as subsets of $S$, including its fixed points, whereas Mathlib's cycleType records only the lengths of the nontrivial cycles. Second, the weighted orbit count needs the weight to be invariant under the action and Burnside's argument to be carried out inside a polynomial ring rather than in $\mathbb N$. Neither step is a direct instance of a Mathlib lemma. Proving the identity only after substituting integers for the $c_i$ does not suffice: it determines the number of classes, not the coefficient of each monomial.

Formalization scope

• $S$ is a Fintype with decidable equality, $r$ = Fintype.card S; a permutation group is a Subgroup (Equiv.Perm S), and $|G|$ = Nat.card G $\ge 1$.
• $j_k(\pi)$ is cycleCount π k: the number of fixed points for $k = 1$ and the multiplicity of $k$ in Equiv.Perm.cycleType for $k \ge 2$. $P_G$ is cycleIndex G : MvPolynomial (Fin r) ℚ, the variable with index $k$ standing for $x_{k+1}$.
• Colours are Fin m, colorings are S → Fin m, and $\pi^*(f) = f \circ \pi^{-1}$; the induced relation is colorSetoid G m. Composing with $\pi$ instead of $\pi^{-1}$ gives the same classes.
• The pattern inventory is patternInventory G m : MvPolynomial (Fin m) ℚ, the sum over the quotient of the weight $\prod_{s} X_{f(s)}$ of a representative (Quotient.out); that the weight is a class invariant is part of the theorem.
• The substitution is MvPolynomial.bind₁ sending $x_{k+1}$ to $\sum_i c_i^{k+1}$.
• For the milestones, a group action is a Mathlib MulAction G 𝒞 with Fintype G and Fintype 𝒞; $N$ is the number of MulAction.orbitRel classes and the identity is stated in $\mathbb Q$.
• The book's statements contain no $O(\cdot)$, approximations or unspecified constants; no constant is instantiated.
• Ruled out: the cycle index is defined from the cycle structure of each permutation alone. Defining $P_G$, or its substituted form, through colorings, fixed sets or orbit weights would make the goal a restatement of its definitions.

Reusable beyond this mission: the cycle index of a permutation group and the pattern inventory, both needed for any later count of necklaces, graphs up to isomorphism, or de Bruijn's generalization with a group acting on the colours. Contributions of cycle indices of specific groups (cyclic, dihedral, symmetric) are welcome.

Selected references

• M. T. Keller and W. T. Trotter, Applied Combinatorics, 2017 Edition, Chapter 15, pp. 291–314. https://www.appliedcombinatorics.org/
• G. Pólya, "Kombinatorische Anzahlbestimmungen für Gruppen, Graphen und chemische Verbindungen", Acta Mathematica 68 (1937), 145–254. https://doi.org/10.1007/BF02546665
• J. H. Redfield, "The Theory of Group-Reduced Distributions", American Journal of Mathematics 49 (1927), 433–455. https://doi.org/10.2307/2370675
• N. G. de Bruijn, "Pólya's theory of counting", in E. F. Beckenbach (ed.), Applied Combinatorial Mathematics, Wiley, 1964, 144–184.

Motivation

Moving as much as possible of something — freight, water, data — from an origin to a destination through connections of limited capacity is one of the basic problems of operations research. Its mathematical form, the maximum flow problem, was posed in the 1950s in work on rail networks and solved independently by Ford and Fulkerson (Maximal flow through a network, Canadian J. Math. 8 (1956)) and by Elias, Feinstein and Shannon (A note on the maximum flow through a network, IRE Trans. Inform. Theory 2 (1956)). The answer, the Max Flow–Min Cut Theorem, is a min–max duality: the largest amount that can be shipped equals the smallest total capacity whose removal disconnects the destination from the origin. It is a standard example of linear-programming duality with a combinatorial proof, and it is the source of Hall's matching theorem, Menger's theorem and Dilworth's theorem via network constructions.

This mission formalizes Chapter 13 of Keller and Trotter's Applied Combinatorics (2017 Edition), together with the two theorems of Chapter 14 that apply it, in the book's own model of a network.

Setting

A network consists of a finite vertex set $V$, a set of directed edges $(x, y)$, a source $S$ and a sink $T$ with $S \ne T$, and a capacity $c(x, y) \ge 0$ (a real number) on each edge. The underlying directed graph is an oriented graph: for any two vertices $x, y$ at most one of $(x, y)$, $(y, x)$ is an edge. Every edge at $S$ points away from $S$ and every edge at $T$ points into $T$.

A flow is a function $\phi$ on the edges with $0 \le \phi(x, y) \le c(x, y)$, extended by $\phi(x, y) = 0$ on pairs that are not edges, satisfying the conservation laws

$$\sum_x \phi(S, x) = \sum_x \phi(x, T), \qquad \sum_x \phi(x, y) = \sum_x \phi(y, x)\quad (y \ne S, T).$$

The value of $\phi$ is $\operatorname{value}(\phi) = \sum_x \phi(S, x)$.

A cut is a partition $V = L \cup U$ with $S \in L$, $T \in U$. Its capacity is

$$c(L, U) = \sum_{x \in L,\ y \in U} c(x, y),$$

summed over the edges directed from $L$ to $U$ only.

Given a flow $\phi$, an edge $(x, y)$ is used if $\phi(x, y) > 0$ and has spare capacity if $\phi(x, y) < c(x, y)$. An augmenting path is a sequence $P = (x_0, \dots, x_m)$ of distinct vertices from $x_0 = S$ to $x_m = T$ such that each step either follows an edge $(x_{i-1}, x_i)$ with spare capacity (a forward edge) or traverses a used edge $(x_i, x_{i-1})$ backwards (a backward edge). Its augmentation amount is $\delta = \min\{\delta_1, \delta_2\}$, where $\delta_1$ is the least spare capacity of a forward edge and $\delta_2$ the least flow on a backward edge ($\delta = \delta_1$ when there is no backward edge).

For Chapter 14: in a finite simple graph with bipartition $V = V_1 \cup V_2$, a matching is a set of edges no two of which share an endpoint; it saturates a vertex that is an endpoint of one of its edges; and $N(A)$ is the set of neighbors of the vertices in $A$.

Formalization targets

Goal: the Max Flow–Min Cut Theorem (Theorem 13.10)

For every network there is a real number $v_0$ with

$$v_0 = \max\{\operatorname{value}(\phi) : \phi \text{ a flow}\} = \min\{c(L, U) : V = L \cup U \text{ a cut}\},$$

that is, $v_0$ is attained by some flow and bounds every flow value from above, and $v_0$ is attained by some cut and bounds every cut capacity from below.

Milestones

• Theorem 13.4. For every flow $\phi$ and every cut, $\operatorname{value}(\phi) \le c(L, U)$.
• Proposition 13.7. If $P$ is an augmenting path for a flow $\phi$ of value $v$ and $\delta$ is its augmentation amount, the function obtained by adding $\delta$ on the forward edges of $P$ and subtracting $\delta$ on its backward edges is a flow of value $v + \delta$.
• Theorem 14.1. If every capacity is an integer, some maximum flow has $\phi(x, y) \in \mathbb Z$ on every edge.
• Theorem 14.7 (Hall). In a finite bipartite graph with bipartition $V_1 \cup V_2$ there is a matching saturating every vertex of $V_1$ if and only if $|N(A)| \ge |A|$ for every $A \subseteq V_1$.

Significance

The result. Theorem 13.10 turns every maximum-flow computation into a certified one: a flow and a cut of equal value prove each other optimal, and Theorem 13.4 shows no certificate can do better. Together with the integrality theorem 14.1 it is the engine behind the combinatorial applications of Chapter 14: maximum matchings in bipartite graphs, Hall's theorem, and the computation of the width of a poset with a minimum chain partition. Beyond the book, the same duality underlies Menger's theorem, König's theorem, the analysis of image segmentation by graph cuts, and the combinatorial theory of totally unimodular linear programs.

Formalizing it. The results are classical and proved. Mathlib has no theory of network flows. The platform has a Max-Flow Min-Cut theorem in the model of Bertsimas and Tsitsiklis (a general digraph on Fin n with capacities in $(0, \infty]$, value compared in EReal), which does not cover the book's networks with zero capacities and is stated for a different encoding. This mission produces the theory in the book's model: finite oriented networks with real non-negative capacities, flows as functions on vertex pairs, cuts as vertex subsets, and the augmenting-path step that the Ford–Fulkerson labeling algorithm iterates. Hall's theorem is in Mathlib in its indexed-family form; the graph form stated here is new to the platform.

Difficulty

Theorem 13.4 is a finite-sum rearrangement. The difficulty of the goal is the existence of a maximum flow. The textbook argument runs the labeling algorithm until it halts, then reads off a cut from the labeled vertices. With real capacities this algorithm need not halt: with badly chosen augmenting paths and irrational capacities the flow values can converge to a limit strictly below the maximum, so "repeat until no augmenting path exists" does not by itself produce a maximum flow. The existence of an optimal flow is therefore not a by-product of the algorithm's description; it has to be established in its own right before the absence of augmenting paths can be turned into a cut of equal capacity. A formalization that assumes a maximum flow exists proves a strictly weaker statement. Proposition 13.7 is elementary but bookkeeping-heavy: backward edges subtract flow, and conservation must be checked at every interior vertex of the path.

Formalization scope

The vertex set is a type V with [Fintype V] [DecidableEq V]. A network (AppliedComb.Flows.Network) bundles an edge relation adj, the source S and sink T with S ≠ T, and a real capacity function cap, together with the axioms of an oriented graph, the orientation of edges at S and T, and 0 ≤ cap x y on edges. Flows are functions ϕ : V → V → ℝ satisfying IsFlow, which includes $\phi = 0$ off the edges and keeps the first conservation law as part of the definition, as on the page. The value is $\sum_x \phi(S, x)$. A cut is its part L : Finset V with S ∈ L, T ∉ L. Augmenting paths are injective maps Fin (m + 1) → V, and $\delta_1, \delta_2, \delta$ are computed in WithTop ℝ so that an empty minimum is $\top$ and $\delta = \delta_1$ when there is no backward edge. Hall's theorem uses Mathlib's SimpleGraph with a given bipartition into two Finsets and matchings as sets of Sym2 V edges.

No explicit constants arise: the chapter has no asymptotic or approximate statements.

The book's sentence of Theorem 13.10 reads "if $v_0$ is the maximum value of a flow and $c_0$ the minimum capacity of a cut, then $v_0 = c_0$". A formalization that takes $v_0$ and $c_0$ as hypothetical extrema of possibly empty or unattained sets would be trivial or vacuous; the goal here asserts the existence of a maximum flow and a minimum cut at the same number, and the existence of a maximum flow for real capacities is part of what must be proved.

Needed infrastructure: finite-sum manipulation over Finset (reindexing, splitting over L and Lᶜ), existence of maximizers of a linear function over the set of flows, and, for Theorem 14.1, control of integrality. The definitions of networks, flows, cuts and augmenting paths are reusable for Menger's theorem, König's theorem and the chain-partition network of Section 14.3. Contributions of alternative proofs (via linear-programming duality) are welcome.

Selected references

• M. T. Keller and W. T. Trotter, Applied Combinatorics, 2017 Edition, Chapters 13–14. https://www.appliedcombinatorics.org/book/
• L. R. Ford and D. R. Fulkerson, Maximal flow through a network, Canadian Journal of Mathematics 8 (1956), 399–404. https://doi.org/10.4153/CJM-1956-045-5
• P. Elias, A. Feinstein and C. E. Shannon, A note on the maximum flow through a network, IRE Transactions on Information Theory 2 (1956), 117–119. https://doi.org/10.1109/TIT.1956.1056816
• P. Hall, On representatives of subsets, Journal of the London Mathematical Society 10 (1935), 26–30. https://doi.org/10.1112/jlms/s1-10.37.26
• U. Zwick, The smallest networks on which the Ford–Fulkerson maximum flow procedure may fail to terminate, Theoretical Computer Science 148 (1995), 165–170. https://doi.org/10.1016/0304-3975(95)00022-O

Motivation

Ramsey theory studies the principle that complete disorder is impossible: every sufficiently large structure contains a large, perfectly uniform substructure. Its most familiar instance concerns graphs. In any graph on six vertices there are three vertices that are pairwise adjacent or three that are pairwise non-adjacent, and the same phenomenon persists at every scale. The quantity that measures it, the Ramsey number $R(m, n)$, is one of the most studied and least understood functions in combinatorics. Only a handful of values are known exactly ($R(3,3) = 6$, $R(4,4) = 18$), while $R(5,5)$ is only known to lie between 43 and 49 (Radziszowski, Small Ramsey Numbers).

The subject has a short, well-documented history. F. P. Ramsey proved the general theorem in 1930 as a lemma in decidability (Ramsey 1930). Erdős and Szekeres (1935) gave the upper bound $R(m, n) \le \binom{m+n-2}{m-1}$ (Erdős–Szekeres 1935). In 1947 Erdős proved an exponential lower bound for the diagonal numbers $R(n, n)$ by counting graphs (Erdős 1947); this argument is now regarded as the origin of the probabilistic method. In 1959 Erdős used the same method to show that graphs of large girth and large chromatic number exist (Erdős 1959). For decades the exponential bases $\sqrt 2$ and $4$ stood essentially unchanged; the upper base was lowered below $4$ only in 2023 (Campos–Griffiths–Morris–Sahasrabudhe).

This mission formalizes these results as presented in Chapter 11 of Keller and Trotter, Applied Combinatorics (2017 Edition).

Setting

A graph $G$ is a finite simple graph: a finite vertex set with a symmetric, irreflexive adjacency relation (no loops, no multiple edges). A complete subgraph on $m$ vertices is a set of $m$ pairwise adjacent vertices; an independent set of size $n$ is a set of $n$ pairwise non-adjacent vertices.

A non-negative integer $N$ is a Ramsey bound for $(m, n)$ if every graph with at least $N$ vertices contains a complete subgraph on $m$ vertices or an independent set of size $n$. The Ramsey number $R(m, n)$ is the least positive Ramsey bound. In Lean these are AppliedComb.Ramsey.IsRamseyBound m n N and AppliedComb.Ramsey.ramseyNumber m n.

More generally, write $[n] = \{1, \dots, n\}$ and $C(X, s)$ for the family of $s$-element subsets of $X$. For a string $h = (h_1, \dots, h_r)$, the number $R(s : h_1, \dots, h_r)$ is the least positive $N$ such that for every $n \ge N$ and every colouring $\phi : C([n], s) \to [r]$ some colour $\alpha$ has a set $H_\alpha \subseteq [n]$ of size $h_\alpha$ all of whose $s$-subsets receive colour $\alpha$ (hypergraphRamseyNumber s r h).

The girth of a graph is the smallest number of vertices on a cycle, and infinite for a forest; the chromatic number $\chi(G)$ is the least number of colours in a proper vertex colouring.

Formalization targets

Goal: Erdős's lower bound (Theorem 11.4)

For every positive integer $n$,

$$R(n, n) \;\ge\; \frac{n}{e\sqrt 2}\, 2^{n/2}.$$

Equivalently, below this threshold there is a graph on each number of vertices with neither a complete subgraph on $n$ vertices nor an independent set of size $n$. The statement is for every $n \ge 1$, with no asymptotic slack.

Milestones

• Lemma 11.1. Every graph with at least six vertices has a complete subgraph on 3 vertices or an independent set of size 3.
• Theorem 11.2 (Ramsey's Theorem for Graphs). For positive integers $m, n$ the least positive integer $R(m, n)$ exists.
• Theorem 11.6. For positive integers $r, s$ and $h_1, \dots, h_r \ge s$, the least positive integer $R(s : h_1, \dots, h_r)$ exists.
• Theorem 11.7 (Erdős). For all integers $g \ge 3$ and $t$ there is a graph with $\chi(G) > t$ and girth greater than $g$.

A further item, not a milestone because the book does not number it, records the bound that the proof of Theorem 11.2 establishes: every graph with at least $\binom{m+n-2}{m-1}$ vertices has a complete subgraph on $m$ vertices or an independent set of size $n$.

Significance

The goal is the diagonal lower bound that every later improvement is measured against. With the upper bound from the proof of Theorem 11.2 it shows that $R(n,n)$ grows exponentially, with base between $\sqrt 2$ and $4$. No explicit construction is known to give $R(n, n) > c^n$ for any constant $c > 1$. Theorem 11.7 is the standard example of a statement whose only known proofs for decades were probabilistic, and it shows that chromatic number is not a local property.

On the formal side, Mathlib has cliques, independent sets, girth and chromatic number, but no Ramsey numbers, no Erdős lower bound and no high-girth theorem. The platform already has weaker or differently shaped relatives, all checked for this mission. Erdos1947.ramsey_lower_bound gives a graph on $2^{\lfloor k/2 \rfloor}$ vertices without monochromatic $k$-sets, a weaker bound than the goal's. BookSixth.high_girth_chromatic is a single-parameter form of Theorem 11.7 in another Lean environment. ramsey_theory_upper_bound is a diagonal $4^k$ bound. The goal statement carries the constant $1/(e\sqrt2)$ exactly, which requires an explicit, non-asymptotic lower bound for $n!$ where the book writes "Stirling's approximation".

Difficulty

The obvious route to the goal is to count graphs with a large clique or independent set and compare the result with the total number of graphs. Two steps of that route do not go through as written in the text. First, the book replaces $n!$ by its Stirling approximation, which is only asymptotic; a statement for every $n \ge 1$ needs an inequality valid for all $n$, and the constant $1/(e\sqrt2)$ leaves no room for a cruder estimate such as $n! \ge (n/e)^n$ alone. Second, the counting argument yields a graph on each $t$ below the threshold, whereas $R(n,n)$ is defined as a least threshold over all graphs with at least that many vertices; the two have to be connected.

Theorem 11.7 needs random graphs with edge probability depending on $n$, a first-moment bound on short cycles and on independent sets, and a deletion step. The book states Theorem 11.6 without proof.

Formalization scope

• Graphs are Mathlib SimpleGraph V on a finite type V : Type (Theorems 11.1, 11.2, 11.4) or on Fin N (Theorem 11.7). Cliques and independent sets are SimpleGraph.IsNClique and SimpleGraph.IsNIndepSet on a Finset.
• IsRamseyBound m n N quantifies over every graph with at least $N$ vertices, as the book does; ramseyNumber m n is the sInf of the positive Ramsey bounds. Theorem 11.2 is stated as IsLeast {N | 0 < N ∧ IsRamseyBound m n N} (ramseyNumber m n), so its content is the nonemptiness of that set. The same pattern is used for Theorem 11.6.
• The goal compares real numbers: (n : ℝ) / (Real.exp 1 * Real.sqrt 2) * (2 : ℝ) ^ ((n : ℝ) / 2) ≤ (ramseyNumber n n : ℝ), with a real power. Explicit constant: the book says "use the Stirling approximation … after some algebra"; the statement keeps the book's constant $1/(e\sqrt 2)$ and holds for every $n \ge 1$ with no threshold.
• The bound of the proof of Theorem 11.2 is stated as the Ramsey property at $\binom{m+n-2}{m-1}$, not as an inequality on ramseyNumber, so it cannot hold through an empty defining set.
• Girth is Mathlib's SimpleGraph.egirth (valued in $\mathbb N \cup \{\infty\}$, $\infty$ for forests), not SimpleGraph.girth, which is $0$ on forests. Chromatic number is SimpleGraph.chromaticNumber in $\mathbb N \cup \{\infty\}$. The parameter $t$ of Theorem 11.7 is a natural number; negative $t$ is trivial.
• Theorem 11.6 is printed with typos: $h_i \ge s$ is read for all $i = 1, \dots, r$, the undefined $n_0$ is read as $R(s : h_1, \dots, h_r)$, and $C([n], s]$ as $C([n], s)$. Colourings are functions on the subtype of $s$-element subsets of Fin n, with colours in Fin r.
• Trivializing formalizations ruled out. A Ramsey number defined as an arbitrary upper bound, or as a supremum with junk value $0$, would make the goal vacuous or false. Here the goal's right-hand side is positive, so it forces the defining set to be nonempty, and every graph is simple on exactly its vertex type, with no loops or multiple edges.
• Reusable infrastructure: IsRamseyBound/ramseyNumber, the hypergraph version, an all-$n$ lower bound for $n!$, and counting over the $2^{\binom{t}{2}}$ labelled graphs on $t$ vertices. Proofs of any milestone are welcome contributions.

Selected references

• M. T. Keller and W. T. Trotter, Applied Combinatorics, 2017 Edition, Chapter 11, pp. 229–238. https://www.appliedcombinatorics.org/
• F. P. Ramsey, On a problem of formal logic, Proc. London Math. Soc. 30 (1930), 264–286. https://doi.org/10.1112/plms/s2-30.1.264
• P. Erdős and G. Szekeres, A combinatorial problem in geometry, Compositio Math. 2 (1935), 463–470. http://www.numdam.org/item/CM_1935__2__463_0/
• P. Erdős, Some remarks on the theory of graphs, Bull. Amer. Math. Soc. 53 (1947), 292–294. https://doi.org/10.1090/S0002-9904-1947-08785-1
• P. Erdős, Graph theory and probability, Canad. J. Math. 11 (1959), 34–38. https://doi.org/10.4153/CJM-1959-003-9
• S. Radziszowski, Small Ramsey Numbers, Electron. J. Combin. Dynamic Survey DS1. https://doi.org/10.37236/21
• M. Campos, S. Griffiths, R. Morris and J. Sahasrabudhe, An exponential improvement for diagonal Ramsey, 2023. https://arxiv.org/abs/2303.09521

Motivation

Linear recurrences with constant coefficients are among the first tools of enumerative combinatorics and the analysis of algorithms: the Fibonacci numbers, the number of binary strings avoiding a pattern, the running time of a divide-and-conquer loop and the number of tilings of a strip all satisfy relations of the form $c_0 a_{n+k} + c_1 a_{n+k-1} + \cdots + c_k a_n = 0$. Chapter 9 of Keller and Trotter's Applied Combinatorics (appliedcombinatorics.org) treats such relations as linear equations in an operator, the advancement operator, in direct analogy with linear differential equations with constant coefficients. The chapter's Principal Theorem says that the solution set of such an equation is a vector space whose dimension equals the order of the recurrence; everything else in the chapter (general solutions for distinct and repeated roots, and the reduction of nonhomogeneous equations to homogeneous ones) is organised around it.

This mission formalizes that theorem, in the book's model of functions on all of $\mathbb{Z}$, together with the numbered lemmas of Section 9.5 on which its outline rests.

Setting

Let $V$ be the real vector space of all functions $f : \mathbb{Z} \to \mathbb{R}$, with pointwise addition and scalar multiplication. The advancement operator $A : V \to V$ is

$$A f(n) = f(n+1) \qquad (n \in \mathbb{Z}),$$

a linear operator with $A^p f(n) = f(n+p)$ for $p \ge 0$. For a nonnegative integer $k$ and real constants $c_0, c_1, \dots, c_k$, the advancement operator polynomial is

$$p(A) = c_0 A^k + c_1 A^{k-1} + c_2 A^{k-2} + \cdots + c_k,$$

so that $p(A) f(n) = c_0 f(n+k) + c_1 f(n+k-1) + \cdots + c_k f(n)$. The solution space of the homogeneous equation $p(A) f = 0$ is

$$W = \{ f \in V : p(A) f = 0 \},$$

the kernel of $p(A)$, a linear subspace of $V$. In Lean, $A$ is AppliedComb.Recurrence.advance : Module.End ℝ (ℤ → ℝ), $p(A)$ is opPoly k c for a coefficient vector c : Fin (k + 1) → ℝ with c i multiplying $A^{k-i}$, and $W$ is solutionSpace k c := LinearMap.ker (opPoly k c). A factor $A - r$ is advance - r • 1.

Formalization targets

Goal: Theorem 9.18 (the Principal Theorem)

For a positive integer $k$ and real constants $c_0, \dots, c_k$ with $c_0 \neq 0$ and $c_k \neq 0$,

$$\dim_{\mathbb{R}} \{ f : \mathbb{Z} \to \mathbb{R} \;:\; (c_0 A^k + c_1 A^{k-1} + \cdots + c_k) f = 0 \} = k.$$

Milestones

1. Lemma 9.19. If $r \neq 0$ and $(A - r) f = 0$, then $f(n) = f(0)\, r^n$ for every $n \in \mathbb{Z}$.
2. Lemma 9.20. If $c_0, c_k \neq 0$, $g \in V$ is arbitrary and $p(A) f_0 = g$, then every solution of $p(A) f = g$ is $f = f_0 + f_1$ with $f_1 \in W$.
3. Theorem 9.21. If $r_1, \dots, r_k$ are distinct nonzero reals, every solution of $(A - r_1)(A - r_2)\cdots(A - r_k) f = 0$ has the form

$$f(n) = c_1 r_1^n + c_2 r_2^n + \cdots + c_k r_k^n \qquad (n \in \mathbb{Z}).$$

4. Lemma 9.22. If $k \ge 1$ and $r \neq 0$, then $(A - r)^k f = 0$ holds exactly when

$$f(n) = c_1 r^n + c_2 n r^n + c_3 n^2 r^n + \cdots + c_k n^{k-1} r^n \qquad (n \in \mathbb{Z})$$

for some real constants $c_1, \dots, c_k$.

Significance

The result itself. Theorem 9.18 is what justifies the standard recipe for solving a recurrence: once $k$ linearly independent solutions are found, every solution is a linear combination of them, and $k$ initial values pin down a unique solution. Theorems 9.21 and 9.22 name those $k$ solutions when the characteristic polynomial splits over $\mathbb{R}$, and Lemma 9.20 reduces nonhomogeneous recurrences, the ones arising from counting problems with a forcing term, to one particular solution plus the homogeneous space.

Formalizing it. The book states Theorem 9.18 without a full proof ("we won't prove the full result") and leaves Lemma 9.22 as an exercise, so a formalization supplies arguments the source omits. Mathlib's LinearRecurrence develops the $\mathbb{N}$-indexed, monic version (LinearRecurrence.solSpace_rank); the bi-infinite, two-sided setting of the book, in which the constant term $c_k$ must be nonzero, is not in Mathlib or on the platform as of this mission.

Difficulty

The subspace part of Theorem 9.18 is immediate; the content is the dimension count, in both directions. On $\mathbb{Z}$ a solution must extend to negative indices as well as positive ones, so an argument that works for sequences indexed by $\mathbb{N}$ does not transfer: there the constant term plays no role and the dimension is $k$ whatever the constant term, while on $\mathbb{Z}$ a vanishing $c_k$ changes the answer. The outline in the book proceeds through factorisations of $p(A)$, which over $\mathbb{R}$ need not exist (complex roots), so the goal cannot be obtained by combining Theorems 9.21 and 9.22 alone. Lemma 9.22 requires showing that the functions $n^j r^n$ solve $(A - r)^k f = 0$ and that they exhaust its solutions, for $n$ ranging over all integers.

Formalization scope

• Functions are $\mathbb{Z} \to \mathbb{R}$ (the real space $V$ of Section 9.5, p. 199), not $\mathbb{N} \to \mathbb{R}$ and not $\mathbb{Z} \to \mathbb{C}$. Powers $r^n$ with $n$ negative are integer powers (zpow), always of a nonzero base.
• Dimension in the goal is Module.rank ℝ (solutionSpace k c) = k, a cardinal equality, so it also asserts finite-dimensionality.
• The coefficient vector is c : Fin (k + 1) → ℝ; c 0 is the leading coefficient $c_0$ and c (Fin.last k) the constant term $c_k$.
• Theorem 9.21 asserts one inclusion, as on the page ("every solution has the form"); Lemma 9.22 asserts both ("the general solution"), as an iff.
• Lemma 9.22 carries the hypothesis $r \neq 0$, the standing assumption of Section 9.5.2 (p. 200), which the lemma's own sentence does not repeat.
• No O(·), "≈" or unspecified threshold occurs in these statements, so no explicit constant is instantiated.
• Ruling out the trivial reading: $W$ is defined as the kernel of the operator polynomial $p(A)$, never as the span of $k$ chosen functions, so the goal is not a statement about the rank of a spanning family.

Needed infrastructure: linear operators on the function space ℤ → ℝ, powers and products in Module.End, Module.rank/Module.finrank, and finite sums; Mathlib's LinearRecurrence may be adapted for the forward half. The definitions advance, opPoly and solutionSpace are reusable for any later mission on recurrences or on generating functions for bi-infinite sequences. Contributions of the milestone lemmas, of a proof of the goal that avoids factorisation over $\mathbb{C}$, and of a complex-valued variant are welcome.

Selected references

• Mitchel T. Keller and William T. Trotter, Applied Combinatorics, 2017 Edition, Chapter 9 (Recurrence Equations), CC BY-SA 4.0. appliedcombinatorics.org
• Mathlib, Mathlib/Algebra/LinearRecurrence.lean (ℕ-indexed linear recurrences, LinearRecurrence.solSpace_rank). Mathlib docs
• Ronald L. Graham, Donald E. Knuth and Oren Patashnik, Concrete Mathematics, 2nd ed., Addison-Wesley, 1994, Section 7.3 (solving recurrences). ISBN 978-0-201-55802-9.