Combinatorics

Motivation

Generating functions are the standard device of enumerative combinatorics for turning a counting sequence into a single algebraic or analytic object: a sequence $\{a_n : n \ge 0\}$ is recorded as the power series $\sum_{n\ge0} a_n x^n$, and operations on series (products, powers, derivatives) become operations on the counts. Chapter 8 of Keller and Trotter's Applied Combinatorics (appliedcombinatorics.org), an open textbook used in undergraduate combinatorics courses, develops the method up to one of its classical applications: extending the binomial theorem to real exponents, as Newton did, and reading off an identity about central binomial coefficients that is awkward to prove by direct counting.

The identity in question,

$$2^{2n} = \sum_{k=0}^{n} \binom{2k}{k}\binom{2n-2k}{n-k},$$

appears in standard collections of binomial identities such as Graham, Knuth and Patashnik's Concrete Mathematics (1994).

Setting

For a real number $p$ and a nonnegative integer $k$, the book defines a number $P(p, k)$ by the recursion

$$P(p, 0) = 1, \qquad P(p, k) = p\,P(p-1, k-1) \quad (k > 0),$$

so that $P(p, k) = p(p-1)\cdots(p-k+1)$ with no requirement $p \ge k$. The generalized binomial coefficient is

$$\binom{p}{k} = \frac{P(p,k)}{k!}.$$

For integers $p \ge k \ge 0$ this is the usual binomial coefficient; for integers $0 \le p < k$ it is $0$; for other real $p$ it is in general nonzero for every $k$. In the Lean development $P(p,k)$ is AppliedComb.GenFun.fallingP p k and $\binom pk$ is AppliedComb.GenFun.binomReal p k.

The generating function of a real sequence $a = (a_n)_{n\ge0}$ is the formal power series $A(x) = \sum_{n\ge0} a_n x^n$, in Lean PowerSeries.mk a : PowerSeries ℝ. When a closed-form function such as $(1+x)^p$ or $(1-4x)^{-1/2}$ is called the generating function of a sequence, the statements below read this as convergence of $\sum_n a_n x^n$ to the function's value on an explicit real interval around $0$.

The central binomial coefficients are $\binom{2n}{n}$: $1, 2, 6, 20, 70, \dots$

Formalization targets

Goal: Corollary 8.14

For every integer $n \ge 0$,

$$2^{2n} = \sum_{k=0}^{n} \binom{2k}{k}\binom{2n-2k}{n-k},$$

stated as an identity of natural numbers.

Milestones

• Lemma 8.11. For every real $p$ and integer $k \ge 0$, $P(p, k+1) = P(p, k)\,(p - k)$.
• Lemma 8.12. For every integer $k \ge 0$, $\binom{-1/2}{k} = (-1)^k \binom{2k}{k} / 2^{2k}$.
• Theorem 8.10 (Newton's Binomial Theorem). For real $p \ne 0$ and real $|x| < 1$,

$$(1+x)^p = \sum_{n=0}^{\infty} \binom{p}{n} x^n .$$

• Theorem 8.13. For real $|x| < 1/4$,

$$(1-4x)^{-1/2} = \sum_{n=0}^{\infty} \binom{2n}{n} x^n .$$

• Proposition 8.3. For real sequences $a$, $b$, the product of their generating functions is the generating function of $\bigl(\sum_{k=0}^n a_k b_{n-k}\bigr)_{n\ge0}$.
• Theorem 8.16 (already on the platform). For each $n \ge 1$, the number of partitions of $n$ into distinct parts equals the number of partitions of $n$ into odd parts.

The first five follow the chapter's own chain toward the goal; Theorem 8.16 is the chapter's other main result and is included as a reference.

Significance

Corollary 8.14 says that the sequence of central binomial coefficients convolved with itself is the sequence $4^n$; equivalently, the generating function of $\binom{2n}{n}$ is a square root of $1/(1-4x)$. Central binomial coefficients count lattice paths with $n$ up-steps and $n$ down-steps, and the identity says that the pairs consisting of a balanced path of length $2k$ and one of length $2n-2k$, summed over $k$, are equinumerous with all $4^n$ strings over a four-letter alphabet. The same generating function reappears in the book's Section 9.7, and Newton's theorem with exponent $-1/2$ or $1/2$ is the standard route to closed forms for Catalan-type sequences.

On the formalization side, Mathlib has the central binomial coefficient (Nat.centralBinom), formal power series, and Newton's series in the complex-analytic form Complex.one_add_cpow_hasFPowerSeriesOnBall_zero, which is also published on the platform as FamousTheorems.newton_binomial_series_6b and included in this mission as a reference. It does not contain the convolution identity of Corollary 8.14, and it does not contain the book's recursive $P(p,k)$ or the closed form of $\binom{-1/2}{k}$. The mission produces a machine-checked version of the chapter's chain from the book's own definitions to the identity.

Difficulty

The identity is not a special case of the Vandermonde convolution $\sum_k \binom{a}{k}\binom{b}{n-k} = \binom{a+b}{n}$: both factors depend on the summation index in their upper argument as well as their lower one. Induction on $n$ does not close directly, since the sum for $n+1$ is not a simple combination of the sum for $n$. A counting proof is possible but not obvious, which is why the chapter's route goes through a generating function with a non-integer exponent. That route passes from formal power series to real analysis: $(1-4x)^{-1/2}$ is a real function, and the passage from an identity of functions on an interval to an identity of coefficients requires the uniqueness of power series coefficients on an open interval and the product of two convergent series. The book asserts Newton's theorem without proof.

Formalization scope

• Numbers. $P(p,k)$ and $\binom pk$ are real-valued, defined by the book's recursion (Definition 8.8) and quotient (Definition 8.9) in the definition item AppliedComb.GenFun.binomReal. Mathlib's descPochhammer and Ring.choose compute the same values; they are not used in the statements so that Lemma 8.11 is a statement about the book's recursion rather than a definitional unfolding.
• Pinned readings. The book treats generating functions as formal power series and states Theorems 8.10 and 8.13 without a domain for $x$. Here both are stated analytically: Theorem 8.10 for real $p \ne 0$ and real $x$ with $|x| < 1$, Theorem 8.13 for real $x$ with $|x| < 1/4$, with the real power Real.rpow of a positive base on the left and HasSum (unconditional convergence of the series) on the right. The book's hypothesis $p \ne 0$ is kept. No other explicit constants replace informal ones: the chapter's statements contain no $O(\cdot)$, "$\approx$" or "sufficiently large".
• Proposition 8.3 is stated for formal power series PowerSeries ℝ with the sum written as $\sum_{k=0}^{n} a_k b_{n-k}$ over Finset.range (n + 1).
• Goal. Corollary 8.14 is an identity in ℕ with Nat.choose; the subtractions $2n-2k$ and $n-k$ occur only for $k \le n$ and are exact. A statement asserting only that the square of the formal power series $\sum_n \binom{2n}{n}X^n$ equals $\sum_n 4^n X^n$, or a purely formal version of Theorem 8.13, would hide the identity in a coefficient comparison and is not the book's statement; the goal is the explicit sum identity.
• Theorem 8.16 is referenced as FamousTheorems.card_odds_eq_card_distincts, stated for all $n$ with Mathlib's Nat.Partition, whose partitions are multisets of positive integers, as in the book (p. 168); the case $n = 0$ it adds is immediate.

A complete development needs real power series on an interval (Cauchy products, identity theorem for coefficients), the real power function, and elementary manipulation of binomial coefficients; the identification of binomReal with Ring.choose is reusable for any later statement using the generalized binomial coefficient. Proofs of any milestone are welcome independently, and so is a direct proof of Corollary 8.14 that bypasses the analytic chain.

Selected references

• M. T. Keller and W. T. Trotter, Applied Combinatorics, 2017 Edition, CC BY-SA 4.0. Chapter 8. https://www.appliedcombinatorics.org/
• R. L. Graham, D. E. Knuth and O. Patashnik, Concrete Mathematics, 2nd ed., Addison-Wesley, 1994. ISBN 978-0-201-55802-9.
• Mathlib, Complex.one_add_cpow_hasFPowerSeriesOnBall_zero (Newton's binomial series). https://github.com/leanprover-community/mathlib4

Motivation

Partially ordered sets model precedence: tasks that must wait for other tasks, versions that supersede others, files nested in directories, alternatives ranked by several criteria at once. Two questions about such a structure recur in scheduling and in the design of algorithms. How many sequential "threads" are needed so that every item lies on a thread in which all items are mutually comparable? How many "rounds" are needed so that no round contains two comparable items? Dilworth's theorem answers the first and its dual, due to Mirsky, answers the second: in both cases the obvious lower bound, given by one large set of mutually incomparable (resp. comparable) items, is attained.

This mission formalizes Chapter 6 of Keller and Trotter's open textbook Applied Combinatorics (2017 Edition, appliedcombinatorics.org), whose capstone is Dilworth's theorem, together with the chapter's other three proved theorems on the same objects.

Timeline. Sperner (1928, doi:10.1007/BF01171114) showed that the largest family of subsets of a $t$-set in which no member contains another has $\binom{t}{\lfloor t/2\rfloor}$ members. Dilworth (1950, doi:10.2307/1969503) proved that a finite poset whose largest antichain has $w$ elements can be partitioned into $w$ chains. Mirsky (1971, doi:10.2307/2316481) recorded the dual statement for antichain partitions. Fishburn (1970, doi:10.1016/0022-2496(70)90062-3) characterized the posets that arise from comparing real intervals as those with no subposet $\mathbf 2 + \mathbf 2$.

Setting

A poset $\mathbf P = (X, P)$ is a set $X$ with a reflexive, antisymmetric and transitive relation $\le$. Here $X$ is finite and is represented by a finite type $\alpha$ with a partial order. A subset $C \subseteq X$ is a chain if every two distinct points of $C$ are comparable; a subset $A \subseteq X$ is an antichain if every two distinct points of $A$ are incomparable. The empty set is both.

The width of $\mathbf P$ is the largest size of an antichain, and the height the largest size of a chain:

$$\operatorname{width}(\mathbf P) = \max_{A \text{ antichain}} |A|, \qquad \operatorname{height}(\mathbf P) = \max_{C \text{ chain}} |C|.$$

A chain partition of $X$ into $k$ parts is a family $C_1, \dots, C_k$ of pairwise disjoint chains with union $X$; an antichain partition is defined the same way with antichains.

The subset lattice $\mathbf 2^t$ is the family of all subsets of a $t$-element set, ordered by inclusion.

A poset is an interval order if each point $x$ can be assigned a closed real interval $[a_x, b_x]$, degenerate intervals allowed, such that $x < y$ exactly when $b_x < a_y$. The poset $\mathbf 2 + \mathbf 2$ consists of two disjoint two-element chains with no comparabilities between them, and $\mathbf P$ excludes $\mathbf 2 + \mathbf 2$ if no four points of $X$ induce a copy of it.

Formalization targets

Goal: Dilworth's theorem (Theorem 6.17)

For every finite poset $\mathbf P$ with $w = \operatorname{width}(\mathbf P)$,

$$\exists\, C_1, \dots, C_w \text{ chains partitioning } X, \quad\text{and}\quad X = C_1 \cup \dots \cup C_k \text{ a chain partition} \implies w \le k.$$

Milestones

• Theorem 6.18 (dual of Dilworth). With $h = \operatorname{height}(\mathbf P)$, $X$ has a partition into $h$ antichains, and every antichain partition has at least $h$ parts.
• Theorem 6.27 (Sperner). For $t \ge 1$,

$$\operatorname{width}(\mathbf 2^t) = \binom{t}{\lfloor t/2 \rfloor}.$$

• Theorem 6.29 (Fishburn). A finite poset is an interval order if and only if it excludes $\mathbf 2 + \mathbf 2$.

The milestones stand on the same definitions as the goal (width, height, chain and antichain partitions, subposets) and are ordered from the one closest to the goal's statement to the one furthest from it.

Significance

The result itself. Dilworth's theorem is a min–max theorem: a minimum over covers equals a maximum over obstructions. It is equivalent to König's theorem on bipartite matchings and to Hall's marriage theorem, and it underlies the computation of minimum chain covers by bipartite matching and network flows (Chapter 14 of the same book). The dual theorem gives the layer decomposition used in scheduling with precedence constraints. Sperner's theorem is the first result of extremal set theory, and Fishburn's theorem is the basic structure theorem for interval orders, which model preferences with thresholds of indifference.

Formalizing it. All four results are classical and proved. In Mathlib at the environment revision of this mission there is no Dilworth or Mirsky theorem; Sperner's inequality (the upper bound on antichains in a Boolean lattice) is available through the LYM inequality, and there is no theory of interval orders. The Prove2Me library holds the easy half of Dilworth (an antichain is no larger than any chain partition) in a different Mathlib environment and over a different chain-partition structure. The mission asks for complete machine-checked statements of the book's four theorems over one common set of definitions.

Difficulty

For Dilworth's theorem the lower bound is a pigeonhole argument; the content is the existence of a partition into exactly $w$ chains. Greedy constructions fail: removing a longest chain, or a maximal chain through a chosen point, can leave a poset whose width has not decreased, so a partition built by repeatedly peeling chains may use more than $w$ of them. No local rule visible from a single chain decides whether its removal keeps the count at $w$.

For Sperner's theorem the lower bound (the middle rank is an antichain) is immediate and the upper bound needs a counting argument over maximal chains; both halves are required, since the target is an equality. For Fishburn's theorem one direction is a four-line contradiction; the other requires constructing real intervals from nothing but the absence of $\mathbf 2 + \mathbf 2$.

Formalization scope

The ground set is a type α with [PartialOrder α] [Fintype α]. Chains and antichains are Mathlib's IsChain (· ≤ ·) and IsAntichain (· ≤ ·). width α and height α are maxima of Finset.card over all antichains (resp. chains) of α; the family is never empty, since the empty set qualifies, so both are well defined and equal $0$ for the empty poset. Width is defined from antichains, not as the least number of chains in a partition; a definition of the latter kind would make the goal true by definition and is ruled out. Chain and antichain partitions are families indexed by Fin k of pairwise disjoint Finsets whose union is all of α; empty parts are not excluded, which does not change either theorem. The "no fewer" clauses quantify over every k and every such family. The subset lattice $\mathbf 2^t$ is Finset (Fin t) ordered by inclusion, $\lfloor t/2 \rfloor$ is t / 2 in ℕ, and Sperner's theorem keeps the book's hypothesis $t \ge 1$. An interval representation is a pair of maps a b : α → ℝ with a x ≤ b x; $\mathbf 2 + \mathbf 2$ is Fin 2 ⊕ Fin 2 with the disjoint-sum order, and "excludes" means there is no order embedding of it into α. Fishburn's theorem is stated for finite posets: the book's construction of a representation is finite, and the equivalence fails for some uncountable posets.

No statement contains an asymptotic bound, so no explicit constant is instantiated.

A complete development needs finite-poset combinatorics (induction on the ground set, subposets as subtypes, maximal and minimal elements), which is reusable across order theory; results proving the definitions agree with Mathlib's notions of chains in Finset lattices are welcome, as is an alternative proof of Dilworth via Hall's theorem, which Mathlib has.

Selected references

• M. T. Keller and W. T. Trotter, Applied Combinatorics, 2017 Edition, Chapter 6, pp. 113–140. https://www.appliedcombinatorics.org
• R. P. Dilworth, A decomposition theorem for partially ordered sets, Annals of Mathematics 51 (1950), 161–166. https://doi.org/10.2307/1969503
• L. Mirsky, A dual of Dilworth's decomposition theorem, American Mathematical Monthly 78 (1971), 876–877. https://doi.org/10.2307/2316481
• E. Sperner, Ein Satz über Untermengen einer endlichen Menge, Mathematische Zeitschrift 27 (1928), 544–548. https://doi.org/10.1007/BF01171114
• P. C. Fishburn, Intransitive indifference with unequal indifference intervals, Journal of Mathematical Psychology 7 (1970), 144–149. https://doi.org/10.1016/0022-2496(70)90062-3

Motivation

Shortest-path distances and network potentials are among the oldest objects in combinatorial optimization: a directed graph with arc lengths, its shortest-path distances, and the "feasible potentials" (vertex labels consistent with those lengths) underlie duality in min-cost flow, scheduling, and difference-constraint systems. Murota's Discrete Convex Analysis (SIAM, 2003) isolates the abstract structure behind these objects — distance functions satisfying the triangle inequality, and their associated sets of admissible potentials — and shows it is governed by exactly the same discrete-convexity machinery as submodular set functions: a one-to-one correspondence with a second family of well-behaved integer point sets, the L-convex sets. Where an M-convex set (chapter 4) is defined by an exchange axiom generalizing matroid base exchange, an L-convex set is defined by closure under coordinatewise lattice operations (∨, ∧) and translation by the all-ones vector — a genuinely different axiom system that nonetheless produces a parallel structural theory: hole-freeness, a polyhedral description via an induced distance function, and integral convexity.

Companion mission 05-lconvex-sets (Discrete Convex Analysis IV) covers this chapter's other half: the hole-free property (Theorem 5.2), the one-to-one correspondence between L-convex sets and integer-valued triangle-inequality distance functions (Theorem 5.5), the intersection properties (Theorem 5.7), and the chapter's discrete separation theorem (Theorem 5.9, its goal). This mission builds the vocabulary those results also need (redeclared here, since sibling drafts cannot yet import one another) and proves the results the chapter leaves for its second half: the fundamental facts connecting a distance function to its admissible potentials (Proposition 5.1), the two-way polyhedral correspondence's supporting propositions (5.3-5.4), Minkowski-sum convexity (Theorem 5.8), and — this mission's goal — the explicit description of an L-convex set's convex hull that establishes its integral convexity (Theorem 5.10).

Setting

Fix a finite ground set $V$. A distance function is a map $\gamma : V \times V \to \mathbb R \cup \{+\infty\}$ with $\gamma(v,v) = 0$; it may take negative finite values and need not be symmetric. It defines a directed graph $G_\gamma = (V, A_\gamma)$ with $A_\gamma = \{(u,v) : \gamma(u,v) < +\infty\}$, arc $(u,v)$ having length $\gamma(u,v)$. Write $\bar\gamma(u,v)$ for the shortest-path length from $u$ to $v$ in $G_\gamma$ ($+\infty$ if none exists); $\gamma$ is well defined ($\bar\gamma$ finite-valued wherever a path exists) exactly when $G_\gamma$ has no negative cycle. The triangle inequality $\gamma(v_1,v_2) + \gamma(v_2,v_3) \ge \gamma(v_1,v_3)$ defines the class $T[\mathbb R]$ (or $T[\mathbb Z]$ when integer-valued). A vector $p \in \mathbb R^V$ is an admissible potential of $\gamma$ if $p(v) - p(u) \le \gamma(u,v)$ for all $u \ne v$; write $D(\gamma)$ for the set of all such potentials.

A nonempty set $D \subseteq \mathbb Z^V$ is L-convex if it satisfies (SBS[Z]): $p, q \in D \implies p \vee q,\ p \wedge q \in D$ (coordinatewise max/min), and (TRS[Z]): $p \in D \implies p \pm \mathbf 1 \in D$. A set $S \subseteq \mathbb Z^V$ is integrally convex if every point of its convex hull $\overline S$ lies in the convex hull of $S$ restricted to that point's integral neighborhood $N(p) = \{y \in \mathbb Z^V : \lfloor p \rfloor \le y \le \lceil p \rceil\text{ coordinatewise}\}$ — a strong, local form of "no holes" saying every real point of the hull is explained by nearby integer points alone.

Formalization targets

Goal: integral convexity of L-convex sets

For an L-convex set $D \subseteq \mathbb Z^V$, writing $a = p - \lfloor p \rfloor$ for the fractional part of $p \in \mathbb R^V$, $\alpha_1 > \cdots > \alpha_m$ for the distinct nonzero values of $a$, and $U_i(p) = \{v : a(v) \ge \alpha_i\}$ (with $U_0 = \emptyset$):

$$\overline D = \{p \in \mathbb R^V : \lfloor p \rfloor + \chi_{U_i(p)} \in D\ \ (i = 0, 1, \ldots, m)\}, \qquad \text{hence } D \text{ is integrally convex}.$$

This is the weakest stable form available: it exhibits an explicit, finite set of at most $|V|+1$ integer witnesses for every point of the hull, which is what "integrally convex" asserts abstractly, rather than a numerical bound that a sharper construction could later shrink.

Supporting structural targets

Four further results build the correspondence this goal uses: the basic duality between a distance function's admissible potentials, its shortest-path closure, and negative-cycle freedom (Prop. 5.1); the induced-distance-function construction recovering a triangle-inequality distance function from any integer point set, and the convex hull of an L-convex set as its associated polyhedron (Prop. 5.3); the converse construction recovering an L-convex set from an integer-valued distance function (Prop. 5.4); and convexity in Minkowski sum (Thm. 5.8).

Significance

Theorem 5.10 is what makes "L-convex" a genuinely convex-analytic notion rather than a combinatorial curiosity: it shows the convex hull of an L-convex set is not merely a polyhedron (already known from the chapter's polyhedral-description results) but one with the strongest local integrality property discrete convex analysis considers, integral convexity — every real point's hull membership is certified by a small, explicitly constructed set of nearby lattice points, uniformly across the whole set. This is the L-convex counterpart of the corresponding M-convex fact (chapter 4's Theorem 4.24) and is used later in the book wherever L-convex functions (chapter 7) need their epigraphs' local structure. Proposition 5.1 is the combinatorial engine underneath: it is exactly the LP-duality statement between shortest paths and feasible potentials that appears, in various guises, throughout network flow theory, made precise here as the base case the L-convex correspondence rests on.

None of these results are open — Murota presents them as, in his own words, "fundamental facts well known in network flow theory" (Proposition 5.1) systematized into the discrete convex analysis framework. What this mission contributes is a faithful, machine-checked formal statement of each, in the shared Lean vocabulary (LConvexSet, AdmissiblePotentials, ShortestDist) the rest of the Discrete Convex Analysis series can build on; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The shortest-path closure $\bar\gamma$ is not a bookkeeping convenience but genuinely graph-theoretic content: proving Proposition 5.1 requires constructing an admissible potential from a shortest-path labeling and, conversely, deriving the negative-cycle-freeness of $G_\gamma$ from the mere existence of one admissible potential — a min-cost-flow-style LP duality argument, not a direct combinatorial check. Theorem 5.10's difficulty sits in a different place: the naive approach to "$D$ is integrally convex" would attempt an inductive argument peeling off one coordinate at a time, but the actual proof constructs a single, uniform family of $m+1$ witness points from the sorted fractional values of $p$ — a Carathéodory-style representation (Eq. (5.11)) that must simultaneously stay inside the integral neighborhood $N(p)$ and land in $D$ itself via the triangle inequality of $D$'s induced distance function, a construction with no one-coordinate-at-a-time shortcut.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; L-convex sets are Set (V → ℤ); distance functions are V → V → WithTop ℝ; admissible-potential sets are Set (V → ℝ). The shortest-path closure is formalized directly from finite walks (Fin (k+1) → V) rather than via a graph-library shortest-path predicate, matching the book's own construction. The Eq. (5.11) witnesses are built exactly as the book describes them — sorted distinct nonzero fractional values and their level sets — mirroring the Lovász-extension construction of the companion mission 20-ch04b-mconvexsets. No numeric constants are hard-coded anywhere in this mission (rule 7 is vacuous). The goal's explicit witness set (at most $|V|+1$ points) is not a trivializing special case: it holds for every L-convex set and every point of its hull, with no extra hypothesis narrowing the class. This mission's definitions (LConvexSet, AdmissiblePotentials, DistanceFunction, IsIntegrallyConvex) are redeclared from chunk 05-lconvex-sets (and, for IsIntegrallyConvex/IntegralNeighborhood, from chapter 3's own definitions) rather than imported, since sibling drafts in this series cannot yet reference one another; a later, published version of this book's namespace should consolidate them. Contributions completing any of the five sorrys are welcome; Proposition 5.1's LP-duality argument and the goal's Carathéodory-style construction are the two with the most independent proof content.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• A. J. Hoffman, "On abstract dual linear programs," Naval Research Logistics Quarterly, 10 (1963), pp. 369-373 (feasible-potential duality in network flow theory).

Motivation

Maximizing a nonnegative submodular set function without constraints contains Max Cut, Max Directed Cut and facility-location problems as special cases. In the value-oracle model an algorithm knows nothing about the function except the values $f(S)$ of the sets $S$ it queries, and it is judged by the number of queries it makes. Feige, Mirrokni and Vondrák (SIAM J. Comput. 40(4), 2011) gave constant-factor algorithms in this model and matching limits on what any algorithm can do. For symmetric functions, such as cut functions of undirected graphs, a uniformly random set already achieves $\tfrac12$ of the optimum in expectation (Theorem 2.1 of the paper). The question this mission formalizes is whether any algorithm can do better, and the answer given by Theorem 4.5 is: not without exponentially many value queries. The same factor $\tfrac12$ was later shown to be achievable for general (non-symmetric) nonnegative submodular functions by Buchbinder, Feldman, Naor and Schwartz (FOCS 2012 / SIAM J. Comput. 2015), so the bound of Theorem 4.5 is the tight limit of the whole problem in the value-oracle model.

Timeline:

• 2007 (FOCS) / 2011 (SIAM J. Comput.): Feige, Mirrokni and Vondrák prove that no algorithm with subexponentially many value queries achieves $(\tfrac12 + \epsilon)$ of the optimum on symmetric nonnegative submodular functions, and give $\tfrac25$ for general functions.
• 2011: Vondrák's symmetry-gap framework (SIAM J. Comput. 42(1), 2013) generalizes the construction to constrained problems.
• 2012: Buchbinder, Feldman, Naor and Schwartz give a randomized $\tfrac12$-approximation for general nonnegative submodular functions, matching the bound.

Setting

Let $[n] = \{0, \dots, n-1\}$ be the ground set, with $n$ even. A set function $f : 2^{[n]} \to \mathbb{R}$ is submodular if $f(S \cup T) + f(S \cap T) \le f(S) + f(T)$ for all $S, T$, symmetric if $f([n]\setminus S) = f(S)$ for all $S$, and $\mathrm{OPT}(f) = \max_{S} f(S)$.

Fix an integer $m$ with $1 \le m \le n/2$ and write $\epsilon = m/n$, so that $\epsilon n$ is an integer. For integers $k, \ell$ put

$$f(k,\ell) = \begin{cases} (k+\ell)(n-k-\ell) & |k-\ell| \le m,\\ k(n-2\ell) + (n-2k)\ell + m^2 - 2m|k-\ell| & |k-\ell| > m. \end{cases}$$

For a set $C \subseteq [n]$ with $|C| = n/2$ and $D = [n] \setminus C$, the hard instance is $f_C(S) = f(|S\cap C|, |S\cap D|)$. The cut function of the complete graph is $g(S) = |S|(n-|S|)$, with maximum $\tfrac14 n^2$. A set $Q$ is balanced for $C$ if $\bigl||Q\cap C| - |Q\cap D|\bigr| \le m$; on balanced sets $f_C = g$.

A deterministic adaptive $q$-query algorithm $A$ chooses each query from the answers received so far, and after $q$ answers outputs a set $A(h)$ when run against an oracle $h$. A randomized algorithm is a distribution $\mu$ over deterministic ones, with expected value $\mathbb{E}_{A\sim\mu}[h(A(h))]$.

Formalization targets

Goal: Theorem 4.5 with the constants of its proof

For every such $n, m$:

1. every $f_C$ with $|C| = n/2$ is nonnegative, symmetric and submodular, with

$$\mathrm{OPT}(f_C) = \tfrac12 n^2 (1 - 2\epsilon + 2\epsilon^2);$$

2. for every $q < e^{\epsilon^2 n/8}$ and every randomized $q$-query algorithm $\mu$ there is a $C$ with $|C| = n/2$ and

$$\mathbb{E}_{A\sim\mu}\bigl[f_C(A(f_C))\bigr] \le \tfrac14 n^2 + \bigl(2e^{-\epsilon^2 n/8} + 2e^{-\epsilon^2 n/4}\bigr)\,\mathrm{OPT}(f_C).$$

Hence the ratio attained is at most $\frac{1}{2(1-2\epsilon+2\epsilon^2)} + 4e^{-\epsilon^2 n/8} = \tfrac12 + \epsilon + O(\epsilon^2) + 4e^{-\epsilon^2 n/8}$.

Milestones

• Theorem 1.2, the Chernoff bound for independent variables in $[-1,1]$.
• Submodularity of $f_C$.
• The value $\mathrm{OPT}(f_C) = \tfrac12 n^2(1 - 2\epsilon + 2\epsilon^2)$, attained at $S = C$.
• A fixed query is unbalanced for at most a $2e^{-\epsilon^2 n/4}$ fraction of the half-size sets $C$.
• If all queries are balanced, the algorithm cannot distinguish $f_C$ from $g$.
• The deterministic case of the bound, averaged over $C$.

Significance

The theorem shows that the factor $\tfrac12$ for symmetric submodular maximization, and hence for unconstrained submodular maximization in general, cannot be improved by any algorithm that uses a subexponential number of value queries, whatever its running time. It is an information-theoretic bound and needs no complexity assumption. Along with the later matching $\tfrac12$-approximation, it settles the value-oracle approximability of the problem. The construction, a function equal to a symmetric function on "balanced" sets and larger elsewhere, is the prototype of the symmetry-gap technique used for many later oracle lower bounds.

The result is proved in the paper. No machine-checked version is known to exist: the platform has no value-oracle or query-lower-bound statement. Formalizing it requires a precise model of adaptive randomized query algorithms, a concentration bound for the hypergeometric distribution, and a finite verification of submodularity of an explicit two-regime function, and it fixes the constants that the printed statement leaves as $O(\cdot)$ terms.

Difficulty

Two steps of the printed argument do not go through as written. First, the proof bounds the probability that a fixed query is unbalanced by citing the Chernoff bound for independent variables, but for a uniformly random half-size set $C$ the count $|Q\cap C|$ is hypergeometric, and the summands are not independent. A bound for sampling without replacement is needed instead. Replacing the balanced partition by independent coin flips is not an option: then $|C| \ne n/2$ in general, and the function is no longer the paper's instance.

Second, the argument counts only the queries, but the value an algorithm receives is $f_C$ of its output, which equals $g$ of the output only if the output is balanced as well. That event has to be controlled too.

Finally, submodularity of $f_C$ must be checked across the boundary $|k-\ell| = \epsilon n$ between the two regimes, where the formula changes.

Formalization scope

• The ground set is Fin n with $n$ even; $\epsilon n$ is an integer $m$ with $1 \le m$ and $2m \le n$, following the paper's "assume that $\epsilon n$ is an integer". Sets are Finset (Fin n), and all values are real.
• $\mathrm{OPT}$ is Finset.sup' over all subsets. There is no junk value.
• The partition $(C, D)$ is uniform over half-size sets; probabilities over it are counts of n/2-subsets divided by $\binom{n}{n/2}$, written multiplied out.
• A deterministic algorithm is a pair of decision rules query, output : List ℝ → Finset (Fin n) making exactly $q$ adaptive queries with arbitrary real answers. A randomized algorithm is a PMF over deterministic algorithms, which covers every randomization with countable support. The algorithm sees $f$ only through query answers; it never receives $C$.
• Pinned-down constants. The printed theorem, "fewer than $e^{\epsilon^2 n/8}$ queries" and "expected value at least $(\tfrac12+\epsilon)\mathrm{OPT}$", is not what the proof gives for one and the same $\epsilon$. On the proof's instances $\mathrm{OPT} = \tfrac12 n^2(1-2\epsilon+2\epsilon^2)$, and the ratio held is $\frac{1}{2(1-2\epsilon+2\epsilon^2)} > \tfrac12 + \epsilon$. The formal goal states the explicit bound the proof establishes. The literal printed pair, stated for the proof's family with the same $\epsilon$, is false: the zero-query algorithm that outputs a fixed half-size set gets at least $\tfrac14 n^2 > (\tfrac12+\epsilon)\mathrm{OPT}$.
• Added term. The error term $2e^{-\epsilon^2 n/4}$ for the output set is added to the paper's $2e^{-\epsilon^2 n/8}$.
• Ruled-out trivializations. A restricted algorithm class (non-adaptive, deterministic, or one that must return a queried set) would give a different, weaker theorem. So would a bound that lets the algorithm read $C$, which would make the statement false. Both the instance's properties (nonnegativity, symmetry, submodularity, the value of OPT) and the bound are part of the goal, so an empty or degenerate family cannot satisfy it. The quantifier order is: for every algorithm there is an instance.
• Needed infrastructure: a value-oracle algorithm model; tail bounds for the hypergeometric distribution (Hoeffding's inequality for sampling without replacement), which Mathlib lacks; averaging over a PMF of algorithms. The algorithm model and the hypergeometric bound are reusable for other oracle lower bounds. Proofs of any milestone, and alternative derivations of the balance bound, are welcome.

Selected references

• U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing Non-Monotone Submodular Functions, SIAM J. Comput. 40(4):1133–1153, 2011. https://doi.org/10.1137/090779346
• N. Alon, J. H. Spencer, The Probabilistic Method, Wiley (source of Theorem 1.2).
• W. Hoeffding, Probability Inequalities for Sums of Bounded Random Variables, J. Amer. Statist. Assoc. 58(301):13–30, 1963. https://doi.org/10.1080/01621459.1963.10500830
• J. Vondrák, Symmetry and Approximability of Submodular Maximization Problems, SIAM J. Comput. 42(1):265–304, 2013. https://doi.org/10.1137/110832318
• N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, SIAM J. Comput. 44(5):1384–1402, 2015. https://doi.org/10.1137/130929205

Motivation

Many optimization problems ask for a subset of a finite ground set that maximizes a submodular function, a set function with diminishing marginal returns. Max Cut and Max Directed Cut in graphs, facility location with fixed costs, and the maximization of mutual information or entropy of a subset of random variables are all of this form. Unlike the monotone case, where a greedy algorithm achieves $1 - 1/e$, a general nonnegative submodular function may decrease when elements are added, and the empty set and the full set can both be poor. The question is how large a constant fraction of the optimum a polynomial-time algorithm can guarantee when the function is given only through an oracle that returns $f(S)$ for a queried set $S$.

Feige, Mirrokni and Vondrák (SIAM J. Comput. 40(4), 2011) gave the first constant-factor algorithms for this problem. A uniformly random set achieves $1/4$ of the optimum, a deterministic local search achieves $1/3 - \epsilon/n$, and a randomized smooth local search achieves $2/5 - o(1)$. The last result is the paper's best approximation for general nonnegative submodular functions (Table 1, p. 1136), and it is the subject of this mission.

Timeline. Feige, Mirrokni and Vondrák: $1/4$, $1/3$ and $2/5$ (FOCS 2007; journal version 2011). Gharan and Vondrák (SODA 2011): about $0.41$ by simulated annealing. Buchbinder, Feldman, Naor and Schwartz (FOCS 2012; SIAM J. Comput. 2015): a randomized double greedy algorithm achieving $1/2$, which matches the $1/2$ hardness in the value oracle model proved in the same paper by Feige, Mirrokni and Vondrák.

Setting

Let $X$ be a finite ground set with $n = |X| \ge 1$ elements and $f : 2^X \to \mathbb{R}$ a function with $f(S) \ge 0$ for all $S$ and

$$f(S \cup T) + f(S \cap T) \le f(S) + f(T) \quad (S, T \subseteq X).$$

Write $OPT = \max_{S \subseteq X} f(S)$. The multilinear extension of $f$ is

$$F(x) = \sum_{S \subseteq X} f(S) \prod_{i \in S} x_i \prod_{j \notin S} (1 - x_j),$$

the expected value of $f$ on a random set containing each $i$ independently with probability $x_i$.

For $A \subseteq X$ and $\delta \in [-1,1]$, the random set $\mathcal{R}(A,\delta)$ is sampled with bias $\delta$ based on $A$: each element of $A$ is included independently with probability $p = (1+\delta)/2$, each element of $B = X \setminus A$ with probability $q = (1-\delta)/2$. The potential is $\Phi(A) = \mathbf{E}[f(\mathcal{R}(A,\delta))]$ and the smoothed marginal value of $x$ is

$$\omega_{A,\delta}(x) = \mathbf{E}[f(\mathcal{R}(A,\delta) \cup \{x\})] - \mathbf{E}[f(\mathcal{R}(A,\delta) \setminus \{x\})].$$

Algorithm SLS starts from $A = \emptyset$. At each iteration it obtains estimates $\tilde\omega_{A,\delta}(x)$ within $\pm\frac{1}{n^2}OPT$ of $\omega_{A,\delta}(x)$. If some $x \notin A$ has $\tilde\omega_{A,\delta}(x) > \frac{2}{n^2}OPT$ it adds $x$; otherwise, if some $x \in A$ has $\tilde\omega_{A,\delta}(x) < -\frac{2}{n^2}OPT$ it removes $x$; otherwise it stops and returns a random set $\mathcal{R}(A, \delta')$.

Formalization targets

Goal: Theorem 3.6 in the explicit form of its proof

With $\delta = 1/3$, and $\delta' = 1/3$ with probability $0.9$ or $\delta' = -1$ with probability $0.1$: for every run from $\emptyset$ whose estimates are all accurate and which has terminated at $A$,

$$\tfrac{9}{10}\,\mathbf{E}[f(\mathcal{R}(A,\tfrac13))] + \tfrac{1}{10}\,f(X \setminus A) \ge \Big(\frac{2}{5} - \frac{9}{5n}\Big) OPT,$$

and, for every $\delta \in (0,1]$, every run of $k$ iterations with accurate estimates has $k < n^2/\delta$ (fewer than $3n^2$ for $\delta = 1/3$).

Milestones, in attack order

• Lemma 2.2: $\mathbf{E}[g(A(p))] \ge (1-p)g(\emptyset) + p\,g(A)$.
• Display (∗): for three independently sampled sets, $\mathbf{E}[f(A_1(p_1) \cup A_2(p_2) \cup A_3(p_3))] \ge \sum_{I \subseteq \{1,2,3\}} \prod_{i\in I} p_i \prod_{i \notin I}(1-p_i) f(\bigcup_{i \in I} A_i)$.
• The increment identity $\Phi(A \cup \{x\}) - \Phi(A) = \delta\,\omega_{A,\delta}(x)$ for $x \notin A$, and its removal counterpart.
• $0 \le \Phi(A) \le OPT$.
• The terminal upper estimates $\mathbf{E}[f(R \cup (B\cap C))],\ \mathbf{E}[f(R \cap (B \cup C))] \le \mathbf{E}[f(R)] + \frac{2}{n}OPT$.
• The two lower bounds in $27$ths on the same two expectations.
• The final chain $\mathbf{E}[f(R)] + \frac19 f(B) + \frac2n OPT \ge \frac49 OPT$.

Significance

The $2/5$ bound showed that local search on a smoothed objective, the multilinear extension restricted to points with two coordinate values, beats both uniform sampling and plain local search for non-monotone submodular maximization. The multilinear extension later became the standard tool for submodular maximization under constraints, through continuous greedy methods, contention resolution schemes and the analysis of randomized rounding. Display (∗) and Lemma 2.2 are the basic sampling inequalities for submodular functions and are reused throughout that literature.

The result is proved in the paper; it has been superseded in ratio by later algorithms reaching $1/2$. To our knowledge none of it is machine-checked: Mathlib has no multilinear extension and no submodular maximization results. This mission produces a checked form of the analysis with every constant explicit: the $o(1)$ as $\frac{9}{5n}$, "polynomial time" as $n^2/\delta$ iterations, and the dependence on the accuracy of the sampled estimates as an explicit hypothesis.

Difficulty

The iteration bound and the increment identity are routine once the multilinear extension is set up. The substance lies in the lower bounds. The returned set $R$ is random, so the comparison with the optimal set $C$ cannot be made through a single local-optimality inequality as in deterministic local search; and approximate local optimality holds only for the smoothed marginals $\omega_{A,\delta}$, which are averages over the random set, not for $f$ at any fixed set. Sampling inequalities such as (∗) are stated for independent samples of arbitrary, possibly overlapping sets, and their expectations are sums over products of subsets; the bookkeeping of such sums is the main formalization burden. The constants must also balance exactly: with $\delta = 1/3$ the $27$ths add up so that the $\frac{9}{10}/\frac{1}{10}$ mixture yields $2/5$. A different split or a different $\delta$ gives a different constant.

Formalization scope

The ground set is a Fintype X with decidable equality; sets are Finset X; $f$ is real valued, with nonnegativity and submodularity as hypotheses. The standing assumptions of the paper are made explicit: $f \ge 0$ (§3), value-oracle access (modelled by $f$ itself), $n = |X|$, and $n \ge 1$ (Nonempty X), so that $\frac{1}{n^2}$ and $\frac{9}{5n}$ are not Lean's junk value of division by zero. $OPT$ is Finset.sup' over all subsets, which has no junk value. Every expectation over independently sampled sets is an exact finite sum: the multilinear extension for $\mathcal{R}(A,\delta)$, and iterated sums over subsets for the several independent samples in Lemma 2.2 and (∗). Sampling probabilities carry $0 \le p \le 1$.

The algorithm is a relation, not a choice: any element meeting the step-3 condition may be added, and removal is allowed only when no addition applies. The goal quantifies over every run from $\emptyset$, every choice of accurate estimates, recomputed at every iteration, and every termination point. Accuracy is non-strict ("within $\pm$"); the thresholds are strict. The thresholds and accuracy use $OPT$ itself, as the proof does, although step 1 of the algorithm says an estimate of $OPT$ is used. The sampling that produces the estimates and its "with high probability" are not modelled, and the goal is conditional on accurate estimates. The value of the $\delta' = -1$ branch is written as $\mathbf{E}[f(\mathcal{R}(A,-1))]$, which equals $f(X \setminus A)$.

A statement "every $A$ satisfying the terminal conditions gives $2/5 - 9/(5n)$" would be the final milestone plus arithmetic and is not the goal. The goal fixes the start at $\emptyset$, the thresholds, the step order, the accuracy of every estimate, termination and the $0.9/0.1$ mixture.

A complete development needs basic calculus of the multilinear extension: affinity in one coordinate, translation $f(\cdot \cup D)$ and restriction $f(\cdot \cap D)$, and splitting a sample into disjoint pieces. These lemmas are reusable for any work on submodular maximization, and contributions of them as separate theorems are welcome. The golden-ratio variant $\delta = \delta'$ (proof omitted in the paper), the tight example and the hardness results of §4 are out of scope.

Selected references

• U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing Non-Monotone Submodular Functions, SIAM J. Comput. 40(4):1133–1153, 2011. https://doi.org/10.1137/090779346
• S. O. Gharan, J. Vondrák, Submodular Maximization by Simulated Annealing, SODA 2011. https://doi.org/10.1137/1.9781611973082.83
• N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, SIAM J. Comput. 44(5):1384–1402, 2015. https://doi.org/10.1137/130929205
• G. Calinescu, C. Chekuri, M. Pál, J. Vondrák, Maximizing a Monotone Submodular Function Subject to a Matroid Constraint, SIAM J. Comput. 40(6):1740–1766, 2011. https://doi.org/10.1137/080733991

Motivation

Sorting a collection of strings in lexicographic order is a basic subroutine in compilers, string indexing, suffix sorting and the construction of tries. The classical method, due to Aho, Hopcroft and Ullman (The Design and Analysis of Computer Algorithms, 1974), is a multipass radix sort that processes the strings from the last position to the first and runs in time proportional to the total length $m$ of the input plus the alphabet size $k$. Mehlhorn showed that a straightforward first-to-last scan of equal-length strings needs $\Omega(km)$ time.

Paige and Tarjan (Three Partition Refinement Algorithms, SIAM J. Comput. 16(6):973–989, 1987, doi:10.1137/0216062) observed that most of the input is usually irrelevant to the sorted order: only the shortest prefix of each string that tells it apart from the others matters. Their algorithm separates the problem into two steps: (1) find this distinguishing prefix of every string, and (2) sort the distinguishing prefixes. The first step is carried out by partition refinement, the same technique that the paper then applies to the relational coarsest partition problem (the second mission of this series) and to double lexical ordering. This mission formalizes the correctness and the termination bound of the first step.

Setting

Fix $k \ge 1$ and the alphabet $\Sigma = \{1, 2, \dots, k\}$, together with an end marker $0$ that is smaller than every symbol. A string is a finite sequence over $\Sigma \cup \{0\}$; $\lambda$ is the empty string, $|x|$ is the length of $x$, and $x(i)$ is its $i$-th symbol (positions start at $1$). A string $\alpha$ is a prefix of $y$ if $y = \alpha z$ for some string $z$; every string is a prefix of itself. $\Sigma^*0$ is the set of strings over $\Sigma$ followed by one $0$.

The input is a multiset $U = \{x_1, \dots, x_n\} \subseteq \Sigma^*0$ with $n \ge 1$; repeated strings are allowed. The distinguishing prefix $x'_i$ of $x_i$ in $U$ is

1. the shortest prefix of $x_i$ that is not a prefix of any other string of $U$, if $x_i$ occurs only once in $U$;
2. $x_i$ itself, if $x_i$ occurs more than once.

Write $m' = \sum_{i=1}^n |x'_i|$.

For a string $\alpha$, the labeled block $B_\alpha$ is the multiset of strings of $U$ having $\alpha$ as a prefix, and $\alpha$ is its associated prefix. The block is finished if $\alpha = x'_i$ for some $i$, and unfinished otherwise. A state $P$ is a set of labeled blocks. For an unfinished block $B_\alpha \in P$,

$$\mathrm{split}(B_\alpha, P) = \bigl(P \setminus \{B_\alpha\}\bigr) \cup \{\, B_{\alpha u} : u \in \Sigma \cup \{0\},\ \exists x \in B_\alpha,\ x(|\alpha| + 1) = u \,\}.$$

The refinement algorithm starts from $P_0 = \{B_\lambda\}$ and repeatedly applies the step Refine: pick any unfinished block $B_\alpha \in P$ and replace $P$ by $\mathrm{split}(B_\alpha, P)$. A run with $K$ steps is a sequence $P_0, P_1, \dots, P_K$ produced this way; any choice of unfinished block is allowed at every step.

Formalization targets

Goal: Theorem 1 with its explicit bound

For every run $P_0, \dots, P_K$ of the refinement algorithm,

$$K \le m' \qquad\text{and}\qquad \bigl(\text{no block of } P_K \text{ is unfinished}\bigr) \implies P_K = \{B_{x'_1}, \dots, B_{x'_n}\}.$$

The paper states Theorem 1 as "The algorithm terminates and is correct"; the bound $K \le m'$ is the explicit count proved in the last sentence of its proof (p. 975). The goal leaves the choice of unfinished block free, so it holds for every refinement order.

Milestones

1. End markers (§2, p. 974). No string of $U$ is a proper prefix of another string of $U$.
2. Lemma 1 (p. 975). Along every run, every finished block $B_\beta$ is contained in a block of the current state, and there is $B_\alpha \in P_j$ with $\alpha$ a prefix of $\beta$.
3. Proof of Theorem 1, second sentence. For every state of every run, $\sum_{B_\alpha \in P_j} |\alpha| \le m'$.
4. Proof of Theorem 1, third sentence. Every Refine step strictly increases $\sum_{B_\alpha \in P} |\alpha|$.

A supplementary item states the fact on p. 974 that motivates the two-step design: distinct strings have distinct distinguishing prefixes, and $x_i \le x_j$ iff $x'_i \le x'_j$ in lexicographic order.

Significance

Theorem 1 is the correctness half of the lexicographic sorting algorithm: once the distinguishing prefixes are known, sorting $U$ reduces to sorting strings of total length $m'$, which is how the paper obtains its $O(m' + k)$ time bound in place of $O(m + k)$. The paper notes that under a natural probability model $m'$ is of order $n \log_k n$, so the gain is large whenever the strings are long. The invariant of Lemma 1 is also the pattern on which the later partition refinement algorithms of the paper are built: a target partition is shown to refine every intermediate partition, and a potential function bounds the number of refinement steps.

The result has been proved since 1987. What this mission adds is a machine-checked account of the algorithm at the level of its abstract refinement steps, with the explicit bound $m'$ rather than an asymptotic statement, and with the standing assumptions of §2 (non-empty input, end markers) made explicit. No formal proof of this algorithm is present in Mathlib or on the platform.

Difficulty

The obvious argument, "each step makes the labels longer, and labels never grow past the distinguishing prefixes", needs two facts that are not immediate from the definitions. First, the labels of a reached state must form a partition of $U$ into non-empty blocks whose labels are pairwise incomparable under the prefix order; this is an invariant of the algorithm, not part of the definition of a state, and it fails for arbitrary sets of labels. Second, the label of an unfinished block must be a proper prefix of every finished label below it, which rests on the end marker: without end markers a string can be a proper prefix of another, a block can be unfinished yet have no strictly longer children, and the algorithm can stall. Bounding the sum of label lengths by $m'$ is not a label-by-label comparison: a state can have fewer labels than strings, and the distinguishing prefixes of different strings can share a label as a common prefix.

Formalization scope

Strings are List (Fin (k + 1)), with 0 : Fin (k + 1) the end marker and prefix the Mathlib relation <+:. The multiset $U$ is a family x : Fin n → List (Fin (k + 1)), so repetitions are distinct indices. The hypotheses 0 < n and EndMarked x ($U \subseteq \Sigma^*0$) are the paper's standing assumptions. A block is identified by its label, not by its set of members: two different labels can carry the same strings (for instance $B_\lambda = B_1$ when every string begins with $1$), and they are different blocks. A state is a Finset of labels; a run is a map Fin (K + 1) → Finset (List (Fin (k + 1))) starting at {[]}. Positions are 1-based in the paper and 0-based in Lean, so $x(|\alpha|+1)$ is (x i)[α.length]?. The distinguishing prefix follows the literal definition; for $n = 1$ it is the empty string.

The running times $O(m' + k)$ and $O(n + k)$ space, the implementation with a queue and a global index, and step two (sorting the prefixes via the refinement tree) are RAM-model statements and are not formalized. Only the explicit step count $m'$ is. A formalization in which split added all $k + 1$ children, added none, or allowed refining a finished block would change the theorem (the bound fails or the goal becomes vacuous); the definitions add exactly the children realized by some string of the block and refine only unfinished blocks.

Contributions welcome: proofs of the milestones, a general API for prefix-closed partition refinement on List, and a proof of the order-preservation item via Mathlib's List.Lex.

Selected references

• R. Paige, R. E. Tarjan, Three Partition Refinement Algorithms, SIAM Journal on Computing 16(6):973–989, 1987. https://doi.org/10.1137/0216062
• A. V. Aho, J. E. Hopcroft, J. D. Ullman, The Design and Analysis of Computer Algorithms, Addison-Wesley, 1974.
• K. Mehlhorn, Data Structures and Algorithms 1: Sorting and Searching, Springer, 1984. https://doi.org/10.1007/978-3-642-69672-5