Combinatorics

Motivation

Delivering goods from one depot to many customers with a fleet of trucks is the vehicle routing problem. Dantzig and Ramser formulated it in 1959 as the "truck dispatching problem" (Management Sci. 6 (1959), doi:10.1287/mnsc.6.1.80). Five years later Clarke and Wright proposed the savings procedure (Oper. Res. 12 (1964), 568–581, doi:10.1287/opre.12.4.568): start with one truck per customer and repeatedly join two routes where joining saves the most distance, as long as the trucks can still carry the loads. On the twelve-customer example of Dantzig and Ramser it reached 290 units against their 294.

The savings procedure became the standard construction heuristic for vehicle routing. It appears in every textbook treatment of the problem, is the initial solution of many metaheuristics, and is the benchmark against which later construction methods are compared. The paper states the procedure and its bookkeeping (the half matrix, the vector $Q$, Table II) but proves nothing about it. That every run of the procedure ends, and ends in a feasible allocation, is left to the reader.

Setting

A depot $P_0$ serves customers $P_1,\dots,P_M$. The distance $d_{y,z}$ between every two points is given, and customer $P_j$ requires a load $q_j$. Trucks come in $n$ capacity classes: $x_i$ trucks of capacity $C_i$ are available, with $C_1<\dots<C_n$, and the trucks of the smallest capacity are unlimited, $x_1=\infty$ (p. 569).

A run is the ordered list of customers $P_{a_1},\dots,P_{a_k}$ served by one truck, which drives $P_0P_{a_1}\cdots P_{a_k}P_0$. Its load is $\sum_i q_{a_i}$. A state of the procedure is a list of runs; its mileage is the total length of its runs. A list of runs is an allocation if every customer lies on exactly one run, and it is feasible if each run can be given a truck of capacity at least its load without using more trucks of any class than are available.

The saving of the cell $(y:z)$ is $d_{0,y}+d_{0,z}-d_{y,z}$. The half matrix records $t_{y,z}=1$ if $P_y$ and $P_z$ are adjacent on a run, and $t_{y,0}\in\{0,1,2\}$ counts how many ends of runs lie at $P_y$. Table II counts, for each capacity level $C_i$, the runs with load above $C_i$ and the trucks with capacity above $C_i$.

The procedure starts with the runs $[P_1],\dots,[P_M]$, so $t_{y,0}=2$ for every customer. A cell $(y:z)$ is admissible if (I) $t_{y,0}>0$ and $t_{z,0}>0$; (II) $P_y$ and $P_z$ are on different runs; (III) after replacing those two runs by one run of load $Q_y+Q_z$, no column of Table II has more runs than trucks. A step links an admissible cell of maximum saving, ties broken arbitrarily, by joining the two runs end to end at $P_y$ and $P_z$. The procedure stops when no cell is admissible.

Formalization targets

Goal: correctness of the procedure

Assume symmetric distances, $C_1<\dots<C_n$, $x_1=\infty$, and that the initial one-truck-per-customer allocation passes the Table II test. Then every run of the procedure is finite whatever the tie-breaks; at every reachable state from which a link is possible a step exists; and every final state $S$ is a feasible allocation satisfying relation (A), $\sum_{z\ne y}t_{y,z}=2$ for every customer, with

$$\text{mileage}(S)=2\sum_{j=1}^M d_{0,j}-\sum_{\substack{1\le y<z\le M\\ t_{y,z}=1}}\bigl(d_{0,y}+d_{0,z}-d_{y,z}\bigr).$$

Milestones

$$\text{mileage}(\text{link}(S,y,z))=\text{mileage}(S)-(d_{0,y}+d_{0,z}-d_{y,z})\quad\text{for admissible }(y:z),$$

relation (A) at every reachable state, the permanence of links between customers, and

$$\#\{\text{runs with load}>C_i\}\le\sum_{k>i}x_k\ \ (i=1,\dots,n)\iff\text{the runs can be allocated to trucks},$$

which together give feasibility of every reachable state. Two further milestones: when $C_n\ge\sum_j q_j$ and the distances are a metric, the optimum equals the traveling salesman optimum (p. 569); and on the data of Table I every run of the procedure ends with total distance 290.

Significance

The goal is the specification the paper's procedure meets: it always terminates, never gets stuck, and outputs routes the fleet can actually drive, with the mileage the half-matrix bookkeeping predicts. The equivalence of the Table II test with truck feasibility is the reason the procedure can check capacities by counting columns instead of solving an assignment problem; it is a nested-class instance of Hall's marriage condition and is reusable for any routing or bin-assignment problem with ordered vehicle classes.

None of these statements is formalized anywhere, and the paper does not prove them. The paper makes no claim of optimality ("near-optimal", p. 568, is not quantified), and the mission does not either. A formal model of the procedure as a nondeterministic transition system is a base on which later results about savings heuristics (worst-case ratios, parallel and sequential variants) can be stated.

Difficulty

The obvious argument for termination, "each link removes a run", needs the invariant that every reachable state is a partition of the customers into runs; the procedure manipulates ordered lists and reverses runs, so the invariant must be carried through every step. Feasibility is not preserved by an arbitrary link but only by one that passes condition (III), and turning the column test into an actual assignment of runs to trucks is a matching argument that fails without both $x_1=\infty$ and the ordering of the capacities. Because ties are broken arbitrarily, every statement must hold for all runs of a nondeterministic procedure, not for one canonical execution. The worked example requires following every tie-break.

Formalization scope

Points are Fin (M+1) with depot 0, and a run's length is SupplyChainTheory.routeCost from the referenced module SupplyChainTheory_vrp. Capacity class i : Fin (n+1) is the paper's $C_{i+1}$; availabilities are in ℕ∞; loads and capacities are real. A state is a list of runs, each an ordered list of customers; the matrix $t$ and the vector $Q$ are computed from the state. The procedure is a step relation, and every invariant is stated for reachable states. Termination is Acc of the step relation at the initial state.

Choices committed to:

• distances are arbitrary real, symmetric numbers (the half matrix, p. 573); no nonnegativity or triangle inequality is assumed in the goal, and savings may be negative;
• every run: ties are free, as the paper suggests choosing randomly;
• reachable states: invariants are not claimed for arbitrary lists of runs;
• Table II is read cumulatively: column "Over $C_i$" compares runs with load $>C_i$ against all trucks of capacity $>C_i$, as the printed Tables II, IV and VI show;
• $x_1=\infty$ and $C_1<\dots<C_n$ are hypotheses; $q_j\le C_n$ is not separately assumed, since it follows from the initial Table II test;
• the initial one-truck-per-customer allocation is assumed feasible (p. 572);
• the metric hypotheses enter only the traveling-salesman milestone.

A correctness claim only about final states, without termination and progress, would hold for a procedure with no moves; a step relation with a fixed tie-break would prove less than the paper; invariants for arbitrary states are false; and a mileage identity for an arbitrary partition says nothing about the procedure's output. None of these is the target.

Not formalized: the informal $C_1\ll\sum q_j$, the shadow-cost reading of p. 571, the decomposition savings (2)–(5) of the general scheme, the load-splitting reduction of pp. 572–573, the Dantzig–Ramser methods, and the empirical comparisons and appendices.

Contributions welcome: proofs of the milestones, in particular the Table II equivalence, which needs a Hall-type argument for nested classes, and a decision procedure for the worked example.

Selected references

• G. Clarke and J. W. Wright, Scheduling of vehicles from a central depot to a number of delivery points, Operations Research 12(4) (1964), 568–581. https://doi.org/10.1287/opre.12.4.568
• G. B. Dantzig and J. H. Ramser, The truck dispatching problem, Management Science 6(1) (1959), 80–91. https://doi.org/10.1287/mnsc.6.1.80
• 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

Motivation

Online matching describes allocation when requests must be answered as they arrive. A matching decision uses only the edges revealed so far and cannot be revised when later requests appear. In the bipartite setting studied by Karp, U. Vazirani, and V. Vazirani, the arriving vertices are girls and the possible partners are boys. Even when the full graph has a perfect matching, a fixed greedy priority can leave many girls unmatched. The paper introduced RANKING, which randomly chooses the boys' priority order once and then uses that order for every arrival.

The question is quantitative: how many pairs does RANKING guarantee in expectation against a graph and an arrival order chosen before its random ranking? The paper's target is a fraction approaching $1-1/e$ of the $n$ pairs in a perfect matching. Its printed Theorem 1 concerns an auxiliary algorithm called EARLY; the RANKING statement follows the intended chain through Lemmas 3 and 5. The original EARLY analysis has a gap for general upper-triangular matrices, so this mission states the RANKING target and the earlier, unaffected lemmas separately. This distinction matters because an assertion about EARLY would be a different formalization target.

Setting

A bipartite graph has a boy side $U$ and a girl side $V$, each with $n$ vertices. An edge $(u,v)$ means that boy $u$ may be paired with girl $v$. A matching is a collection of edges in which no boy or girl occurs twice. The standing hypothesis for the performance guarantee is that the graph has a perfect matching: some bijection from boys to girls selects an edge for every boy. The graph is otherwise arbitrary.

Girls arrive in a predetermined order. When girl $v$ arrives, only her incident edges are revealed. RANKING first chooses a uniformly random permutation $\pi$ of the boys. For each arriving girl, it selects the highest-ranked adjacent boy who is still unmatched, if one exists. Write $M_{\mathrm R}(G,\pi)$ for the final matching. The expected size is the finite average over all $n!$ rankings. The guarantee must hold for every graph and every predetermined arrival order; relabeling girls lets the formal statement fix their order to $n,n-1,\ldots,1$.

The paper also uses a dual rows-arrive view. Boys arrive in an order and choose among eligible girls, whose priority order is fixed. This is the same greedy rule with the sides exchanged. For its triangular reduction, the columns are numbered $1,\ldots,n$ and column $n$ has highest priority. An upper-triangular matrix with unit diagonal is a graph with every edge $(i,i)$ and with an edge $(i,j)$ only when $i\le j$. On such a graph, the auxiliary algorithm EARLY declines to match row $i$ if column $i$ is already covered by EARLY's own matching. For any matching $M$, $D(M)$ denotes the indices for which both row $i$ and column $i$ are covered.

Formalization targets

RANKING guarantee

For every $\varepsilon>0$, one threshold $N$ must work for every size $n\ge N$ and every graph $G$ with a perfect matching:

$$\mathbb E_{\pi\sim\mathrm{Unif}(S_n)}|M_{\mathrm R}(G,\pi)| \ge (1-e^{-1}-\varepsilon)n.$$

This is the uniform lower-bound reading of the paper's $n(1-1/e)-o(n)$ target. It does not prescribe a finite-$n$ additive constant. The mission goal is the RANKING assertion drawn from the paper's Theorem 1 and Lemmas 3 and 5. The six milestones formalize the paper's Lemmas 1–5 and the corollary to Lemma 4, in their source order. They cover the side-exchange identity, arbitrary refusal algorithms, the triangular reduction, the matching-count identity, its expected form, and the pointwise comparison with EARLY.

Significance

The guarantee gives a concrete worst-case floor for a simple randomized allocation rule: as the graph size grows, RANKING matches at least an asymptotic $1-1/e$ fraction of the pairs available in a perfect matching, in expectation. The order is selected before the random permutation, matching the paper's performance measure. The lower bound remains meaningful on sparse graphs and does not rely on a density assumption. The original paper also studies the limit on what any randomized online algorithm can guarantee; that upper-bound result is treated in a separate mission.

A formal development here would provide reusable finite definitions for online greedy matching, arbitrary state-dependent refusal, fixed-order duality, and uniform expectation over permutations. The goal is a theorem statement awaiting a machine-checked proof; compiling the draft declarations verifies their Lean syntax and types, not their truth. The local mission separates the valid early structural statements from later statements whose published EARLY argument does not justify them on general upper-triangular graphs.

Difficulty

The random permutation does not make the fate of different vertices independent. Matching one girl removes a boy who might be essential to a later girl, so a per-arrival probability estimate cannot simply be added across all arrivals. The dual and triangular views capture useful structure, but turning that structure into a uniform bound for every graph is the main obstacle. In particular, reasoning about EARLY as if its matched-column set had the same monotonicity as unrestricted RANKING fails on some upper-triangular matrices. A proof of the goal must establish the RANKING guarantee without treating those later EARLY statements as available facts.

Formalization scope

Boys and girls are both Fin n; an adjacency matrix is a relation between them. A published predicate represents a perfect matching as an edge-preserving bijection. The generic greedy run processes arrival times in increasing order and interprets a smaller priority index as higher rank. It makes a new matching decision only from the current matching and the arriving vertex. RANKING's returned edges are consistently ordered as (boy, girl), even though girls arrive. The dual run has rows arriving in an arbitrary permutation and takes column $n-1$ as highest priority in Lean's zero-based numbering. EARLY's refusal test consults the matching constructed by EARLY itself.

All expectations are finite averages over Equiv.Perm (Fin n), scaled by $1/n!$. The formal $o(n)$ claim is $\forall\varepsilon>0,\ \exists N,\ \forall n\ge N,\ \forall G$ with a perfect matching, the displayed lower bound. Placing $N$ before $G$ preserves the worst-case meaning. The perfect-matching condition is essential: the empty graph cannot satisfy a positive linear guarantee. The triangular matrix in Lemma 3 retains every diagonal edge, so a zero matrix cannot witness the reduction. These conventions rule out vacuous versions of the goal and reduction.

The definitions of partial matching, covered vertices, greedy run, RANKING, EARLY, and uniform average are part of the mission. A complete proof may build further finite counting and permutation machinery; such lemmas can be shared beyond this paper. Contributions toward the six milestone statements, the goal, and faithful supporting results are in scope. Lemmas 6–12 and the printed EARLY Theorem 1 are outside this mission because their analysis depends on claims that fail for some matrices allowed by their surrounding assumptions.

Selected references

• Richard M. Karp, Umesh V. Vazirani, and Vijay V. Vazirani, An Optimal Algorithm for On-line Bipartite Matching, Proceedings of the 22nd Annual ACM Symposium on Theory of Computing, 1990, pp. 352–358. DOI: 10.1145/100216.100262.

Motivation

Many counting problems in probability, combinatorics and statistics ask for the law of the number of occurrences of rare, weakly dependent events: long head runs in coin tossing, matching segments between two DNA sequences, isolated vertices or small subgraphs in a random graph, clusters of points in a scan statistic. Chen's 1975 adaptation of Stein's method gives an explicit error bound for approximating such a count by a Poisson law. Arratia, Goldstein and Gordon (Ann. Probab. 17 (1989) 9–25) recast it in terms of a neighbourhood of dependence for each event. In this form the error bound needs only the first two moments of the indicators whenever each event is independent of the events outside its neighbourhood. The paper's examples (head runs, DNA sequence matching, birthday-type problems) made this form standard in applied probability.

The paper has two main results. Theorem 1 bounds the distance between the law of the total count and a Poisson law; it is essentially contained in Chen (1975). Theorem 2, which the authors describe as new, is a process version. It compares the joint law of all the indicators, that is, where the events occur, with a Poisson process. Theorem 3, a corollary, compares a dependent family of events with an independent family having the same marginal probabilities. This mission formalizes Theorem 2, the finite-dimensional bound it is derived from, the steps of its proof in §6, and Theorem 3.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space and $I$ an index set. For $\alpha\in I$ let $X_\alpha$ be a Bernoulli random variable, $X_\alpha\in\{0,1\}$, with

$$p_\alpha=P(X_\alpha=1)>0,\qquad \lambda=\sum_{\alpha\in I}p_\alpha\in(0,\infty).$$

For each $\alpha$ fix a set $B_\alpha\subseteq I$ with $\alpha\in B_\alpha$, the neighbourhood of dependence of $\alpha$. Put $p_{\alpha\beta}=E(X_\alpha X_\beta)$ and

$$b_1=\sum_{\alpha\in I}\sum_{\beta\in B_\alpha}p_\alpha p_\beta,\qquad b_2=\sum_{\alpha\in I}\sum_{\alpha\neq\beta\in B_\alpha}p_{\alpha\beta},\qquad b_3=\sum_{\alpha\in I}E\bigl|E\{X_\alpha-p_\alpha\mid\sigma(X_\beta:\beta\in I-B_\alpha)\}\bigr|.$$

Roughly, $b_1$ measures the size of the neighbourhoods, $b_2$ the expected number of neighbours of an occurrence, and $b_3$ the dependence between an event and the events outside its neighbourhood. In many applications $X_\alpha$ is independent of $\sigma(X_\beta:\beta\notin B_\alpha)$, so $b_3=0$.

The dependent Bernoulli process is $\mathbf X=(X_\alpha)_{\alpha\in I}$, a random element of $\mathbb Z_+^I$. The Poisson process on $I$ with intensity $p_{(\cdot)}$ is $\mathbf Y=(Y_\alpha)_{\alpha\in I}$ with the $Y_\alpha$ mutually independent and $Y_\alpha$ Poisson with mean $p_\alpha$.

Distances are measured in the paper's total variation norm,

$$\|\mathcal L(U)-\mathcal L(V)\|=\sup_{\|h\|=1}|Eh(U)-Eh(V)|=2\sup_A|P(U\in A)-P(V\in A)|,$$

which is twice the usual total variation distance.

Formalization targets

Goal: Theorem 2

$$\|\mathcal L(\mathbf X)-\mathcal L(\mathbf Y)\|\le2(2b_1+2b_2+b_3).$$

The bound has no dependence on $\lambda$ and no assumption on $I$ beyond countability (which the setting forces).

Milestones, in attack order

1. $T_iS_ih=h$ (§6, p. 22). For functions on $\mathbb Z_+^d$, the coordinatewise Stein operators $(T_if)(j)=j_if(j)-\lambda_if(j+e_i)$ and $(S_ih)(j+e_i)=-(\lambda_iP(Z_i=j_i))^{-1}E\{h(j_1,\dots,Z_i,\dots,j_d)1(Z_i\le j_i)\}$ satisfy $T_iS_ih=h$.
2. Bounds on $f_i=S_i(h-P_ih)$ (§6, p. 22), where $P_ih$ averages $h$ over a Poisson($\lambda_i$) $i$-th coordinate. For $\|h\|\le1$, $\|f_i\|<2(1\wedge1.4\lambda_i^{-1/2})$ and $\|\Delta_kf_i\|<4(1\wedge1.4\lambda_i^{-1/2})$.
3. Display (15) (p. 24). $E\{(X_\alpha-p_\alpha)(f(U+X_\beta e_k)-f(U))\}\le2\|f\|(p_{\alpha\beta}+p_\alpha p_\beta)$ for any random $U$.
4. Displays (13)–(14), the step $i=1$ (p. 23). With $W_j=\sum_{\alpha\in I(j)}X_\alpha$ the block sums of a partition and $Z_1$ an independent Poisson($\lambda_1$),

$$|Eh(W_1,\dots,W_d)-Eh(Z_1,W_2,\dots,W_d)|\le2\|f_1\|\sum_{I(1)}p_\alpha^2+2\|f_1\|\sum_{I(1)}\sum_{\alpha\ne\beta\in B_\alpha}(p_{\alpha\beta}+p_\alpha p_\beta)+\|f_1\|\sum_{I(1)}s_\alpha.$$

5. The finite-dimensional bound (Theorem 2, p. 11). For a partition of $I$ into nonempty blocks $I(1),\dots,I(d)$ with $W_j=\sum_{I(j)}X_\alpha$, $Z_j=\sum_{I(j)}Y_\alpha$ and $\lambda_j=EW_j$:

$$\|\mathcal L((W_1,\dots,W_d))-\mathcal L((Z_1,\dots,Z_d))\|\le2\bigl(1\wedge1.4(\min_i\lambda_i)^{-1/2}\bigr)(2b_1+2b_2+b_3).$$

Companion results

• Theorem 3 (p. 12). For an independent Bernoulli process $\mathbf X'$ with the same marginals as $\mathbf X$, $\|\mathcal L(\mathbf X)-\mathcal L(\mathbf X')\|\le2(2b_1+2b_2+b_3)+4\sum p_\alpha^2$.
• The remark after Theorem 3. $\|\mathcal L(\mathbf X')-\mathcal L(\mathbf Y)\|\le2\sum p_\alpha^2$, so $4\sum p_\alpha^2$ in Theorem 3 can be replaced by $2\sum p_\alpha^2$.

Significance

The result. Theorem 2 says that when $b_1$, $b_2$, $b_3$ are small, the set of indices at which the dependent events occur is close in law to a Poisson process with the same intensity. The bound covers every event about the locations, not just the total count. It is in the strong total variation norm and needs only moment information when $b_3=0$. Theorem 3 turns this into a decoupling statement: a dependent family of rare events is almost indistinguishable from an independent family with the same marginals. The process bound is the form used when the positions of rare events matter, for example in the distribution of the location of the longest match in sequence comparison and in scan statistics.

Formalizing it. The results are proved in the paper; none is machine-checked. A formal development would give a Lean statement and proof of a Chen–Stein bound with explicit constants, for countable index sets and arbitrary dependence. It would also include the coordinatewise Stein operators on $\mathbb Z_+^d$ and the bounds on their solutions, which are reusable for other multivariate Poisson approximations. A companion mission formalizes Theorem 1, including Lemma 1 (the bounds on the one-variable Stein solution) on which milestone 2 rests.

Difficulty

The total variation distance between two laws on $\mathbb Z_+^I$ cannot be bounded coordinate by coordinate, because the $X_\alpha$ are dependent. The one-variable Stein equation controls only the law of a single integer-valued statistic. The paper passes through finite-dimensional block sums and replaces the coordinates one at a time. At each replacement the error has to be charged to the terms of $b_1,b_2,b_3$ indexed by the current block, so that the total over all blocks reproduces $2b_1+2b_2+b_3$ without a factor $d$. Two further points need care. First, the bound $\|\Delta_kf_1\|\le2\|f_1\|$ is the only one available for differences in a coordinate other than the one being replaced; this is why the constants are larger than in Theorem 1. Second, the infinite index set requires a limiting argument from finitely many blocks to the full process.

Formalization scope

• The index set is a countable type. The page says "arbitrary index set", but $p_\alpha>0$ and $\sum p_\alpha<\infty$ force countability; the assumption also makes $\mathbf X$ measurable as a map into $\mathbb N^I$ with the product σ-algebra.
• The $X_\alpha$ are measurable, $\mathbb N$-valued and bounded by $1$. $p_\alpha$ is $P(X_\alpha=1)$. The standing hypotheses $p_\alpha>0$, $\sum p_\alpha=\lambda$ and $\lambda>0$ are explicit.
• $b_1,b_2,b_3$ and $s_\alpha$ are $[0,\infty]$-valued, and every bound is an inequality in $[0,\infty]$, so a divergent series is never read as $0$. The conditional expectation in $s_\alpha$ is taken with respect to a σ-algebra generated by measurable maps, hence a genuine sub-σ-algebra.
• The norm $\|\mathcal L(U)-\mathcal L(V)\|$ is twice the published definition MarkovChainCLT.tvDist (supremum over measurable sets of $|\mu(A)-\nu(A)|$). Dropping the factor $2$ would make the goal twice as strong and false in general.
• $\mathbf Y$ (and $\mathbf X'$ in Theorem 3) lives on its own probability space. Mutual independence of the $Y_\alpha$ and of the $X'_\alpha$ is a hypothesis. Without it the law of the process is not determined by the marginals and the statements are false.
• Block sums $W_j$ are $\mathbb N$-valued tsums, equal to the true sums almost surely. A partition is a surjection $I\to\{1,\dots,d\}$ (Fin d), so Lean's coordinate 0 is the paper's coordinate $1$.
• $(S_ih)(j)$ is set to $0$ when $j_i=0$, as for $S$ in §4. The strict inequalities in milestone 2 use the actual sup norms over $\mathbb Z_+^d$.

Needed infrastructure: product measures and independence on $\mathbb N^I$, Poisson laws (Mathlib's poissonMeasure), conditional expectation, and a one-variable Stein bound (Lemma 1). Contributions of proofs of any milestone, of the general step $i$ of §6, and of the one-dimensional Lemma 1 are welcome.

Selected references

• R. Arratia, L. Goldstein, L. Gordon, Two moments suffice for Poisson approximations: the Chen-Stein method, Ann. Probab. 17(1) (1989) 9–25. https://doi.org/10.1214/aop/1176991491
• L. H. Y. Chen, Poisson approximation for dependent trials, Ann. Probab. 3(3) (1975) 534–545. https://doi.org/10.1214/aop/1176996359
• A. D. Barbour, G. K. Eagleson, Poisson approximation for some statistics based on exchangeable trials, Adv. Appl. Probab. 15(3) (1983) 585–600. https://doi.org/10.2307/1426620
• A. D. Barbour, L. Holst, S. Janson, Poisson Approximation, Oxford University Press, 1992. https://global.oup.com/academic/product/poisson-approximation-9780198522355

Motivation

Counts of rare events often look Poisson even when the events are dependent. For example, a local pattern in a random graph can overlap another copy of the pattern, so the corresponding occurrence indicators are not independent. The useful question is quantitative: how far is the distribution of the total count from a Poisson distribution with the same mean? Arratia, Goldstein and Gordon give a bound in terms of three quantities that can be estimated from neighbourhoods of dependence. Their 1989 paper applies the Chen–Stein method to the count and then to the full point process. This mission concerns the count bound, Theorem 1.

The authors explain that the result is essentially contained in Chen’s earlier work, while their one-variable proof prepares the process result in Theorem 2. The bound remains useful as a precise statement of the dependence conditions under which the Poisson approximation works. The process theorem belongs to the companion mission.

Setting

Let $I$ index Bernoulli indicators $X_\alpha$, each taking values in $\{0,1\}$ on a probability space with law $P$. Write $p_\alpha=P(X_\alpha=1)>0$, and let

$$W=\sum_{\alpha\in I}X_\alpha,\qquad \lambda=E W=\sum_{\alpha\in I}p_\alpha\in(0,\infty).$$

For each $\alpha$, choose a dependence neighbourhood $B_\alpha\subseteq I$ containing $\alpha$. The neighbourhoods need not be symmetric, and the theorem imposes no independence condition: dependence on indicators outside $B_\alpha$ is measured directly. Define $p_{\alpha\beta}=E(X_\alpha X_\beta)$ and

$$\begin{aligned} b_1&=\sum_\alpha\sum_{\beta\in B_\alpha}p_\alpha p_\beta,\\ b_2&=\sum_\alpha\sum_{\substack{\beta\in B_\alpha\\\beta\ne\alpha}}p_{\alpha\beta}. \end{aligned}$$

The remaining quantities use conditional expectation. Let $V_\alpha=\sum_{\beta\notin B_\alpha}X_\beta$, and let $\mathcal F_\alpha$ be the sigma algebra generated by all $X_\beta$ outside $B_\alpha$. Put

$$\begin{aligned} s'_\alpha&=E\left|E[X_\alpha-p_\alpha\mid V_\alpha]\right|, & b'_3&=\sum_\alpha s'_\alpha,\\ s_\alpha&=E\left|E[X_\alpha-p_\alpha\mid\mathcal F_\alpha]\right|, & b_3&=\sum_\alpha s_\alpha. \end{aligned}$$

Conditioning on the count $V_\alpha$ retains less information than conditioning on all far indicators, so $s'_\alpha\le s_\alpha$. Let $Z$ have the Poisson law with mean $\lambda$. The paper defines $\|\mathcal L(W)-\mathcal L(Z)\|$ as twice the usual supremum over events: $2\sup_A|P(W\in A)-P(Z\in A)|$.

Formalization targets

Theorem 1: total variation and the zero-count event

The goal is the complete four-clause statement of Theorem 1, including its strict final inequality:

$$\begin{aligned} \|\mathcal L(W)-\mathcal L(Z)\| &\le 2\left[(b_1+b_2)\frac{1-e^{-\lambda}}{\lambda} +b'_3\min\{1,1.4\lambda^{-1/2}\}\right]\\ &\le 2(b_1+b_2+b_3),\\ |P(W=0)-e^{-\lambda}| &\le (b_1+b_2+b'_3)\frac{1-e^{-\lambda}}{\lambda} <\min\{1,\lambda^{-1}\}(b_1+b_2+b_3). \end{aligned}$$

The intermediate targets are the Stein-operator inverse identity, the bound on a telescoping term, display (11) relating the approximation error to $b_1,b_2,b'_3$, and the two clauses of Lemma 1. The goal keeps the coefficients and both forms of $b_3$ fixed, as the paper states them.

Significance

The result reduces a distributional approximation question to local sums of probabilities and conditional-dependence errors. When $b_1$, $b_2$ and $b_3$ are small, the entire law of the count is close to its Poisson comparison law, and the probability of no occurrence has its own sharper bound. The latter is useful whenever a model asks whether at least one rare event occurs. The result applies without demanding exact independence outside the chosen neighbourhoods; the residual dependence appears in $b_3$.

The paper proves these results. The formalization task is to give the known estimates machine-checked statements and proofs with the constants and probability conventions exposed. Mathlib supplies the Poisson measure and conditional expectation, while the mission adds the paper-specific neighbourhood sums and Stein operators. The formalized theorem can be reused for count approximations in other dependent-indicator models once those models supply bounds on the three error quantities. No machine-checked proof is claimed here: the theorem items are proposed targets with sorry bodies.

Difficulty

A first approximation based only on $E W$ misses overlapping event pairs. Bounding pair dependence through $b_2$ alone also misses dependence between one indicator and the aggregate of far indicators. The authors' third term measures that remaining effect by conditional expectation. The proof must control the Stein solution uniformly while preserving its precise constants; replacing that control with a qualitative bound would not recover Theorem 1. In the countably infinite setting, the sums and conditional expectations also require careful handling of convergence and measurability. The proof of Lemma 1 is attributed in the paper to Barbour and Eagleson; it is a substantive target here rather than an assumed bound.

Formalization scope

The Lean index type is countable. Under the paper's assumptions $p_\alpha>0$ and $\sum_\alpha p_\alpha<\infty$, only countably many indices can exist, so this representation retains the stated probabilistic setting. Indicators are measurable natural-number-valued functions with values at most one. The parameter $\lambda$ is a positive real equipped with the exact HasSum statement for the probabilities. The Poisson law is Mathlib's poissonMeasure at $\lambda$ converted to a nonnegative real parameter.

The sums defining $b_1,b_2,b_3,b'_3$ use extended nonnegative reals, so divergence becomes $+\infty$ rather than the real tsum default zero. The random counts $W$ and $V_\alpha$ use natural-number tsum; their divergent-input default can occur only on a null set under the finite-mean hypotheses and therefore does not change their laws. Measurability of these counts follows from countability and measurability of each indicator. The far-field sigma algebra is generated by the measurable indicators, and the formalization checks that it lies below the ambient sigma algebra, avoiding a default-zero conditional expectation. The paper's total variation norm is exactly 2 * MarkovChainCLT.tvDist, with the factor two retained.

The source writes a strict final inequality without discussing infinite error sums. The Lean statement conditions that single strict clause on $b_1+b_2+b_3<\infty$; otherwise both sides can be infinite and strict comparison is false. The other three clauses allow infinite bounds, as the source does. Lemma 1 fixes the Stein inverse at zero exactly as the paper chooses and uses explicit pointwise sup-norm bounds over all nonnegative integers. Display (11) allows $|h(k)|\le1$, a strengthening of the displayed $\|h\|=1$ case. These choices rule out loss of the norm's factor two, disappearing divergent sums, default-zero mapped measures or conditional expectations, and an unannounced independence assumption.

Selected references

• Richard Arratia, Larry Goldstein and Louis Gordon, Two moments suffice for Poisson approximations: the Chen-Stein method, Annals of Probability 17(1), 9–25, 1989. DOI 10.1214/aop/1176991491.

Motivation

The question behind this mission was posed by T. E. Harris to L. R. Ford, Jr. and D. R. Fulkerson at RAND, in the setting of rail transport: given a rail network linking two cities, with a capacity on every link, find the largest steady flow from one city to the other. Ford and Fulkerson's answer, the minimal cut theorem, published in the Canadian Journal of Mathematics in 1956 (DOI 10.4153/CJM-1956-045-5), says that the obvious upper bound, the total capacity of a set of links whose removal separates the two cities, is always achieved by some flow.

The theorem became the starting point of network flow theory, and through it of a large part of combinatorial optimization and operations research: transportation, assignment, scheduling and network reliability problems are routinely reduced to it.

Timeline.

• 1927: K. Menger proves that the minimum number of vertices separating two vertex sets of a graph equals the maximum number of disjoint paths joining them (Fund. Math. 10), the unit-capacity ancestor of the theorem.
• 1955: Harris and Ross study the Soviet rail network as a capacity problem in a RAND report; Harris formulates the maximal flow problem (Schrijver's historical account: Math. Program. 91, 2002).
• 1956: Ford and Fulkerson publish the minimal cut theorem for undirected networks, with a non-constructive proof based on maximal flows (this paper). Independently, Elias, Feinstein and Shannon state and prove the max-flow min-cut theorem for directed networks (IRE Trans. Inf. Theory 2, 1956), and Dantzig and Fulkerson obtain it from linear programming duality.
• 1956–1962: Ford and Fulkerson's labelling (augmenting path) algorithm, collected in Flows in Networks (Princeton, 1962).
• 1972: Edmonds and Karp give polynomial bounds for augmenting-path methods (J. ACM 19).

Setting

A network $N$ consists of a finite set of vertices $V$, a finite set of arcs $E$, two distinct vertices, the source $a$ and the sink $b$, and a positive capacity $c(e)>0$ on every arc. Each arc $e$ has two distinct end vertices; arcs are undirected, and several arcs may join the same pair of vertices.

A chain joining $u$ and $w$ is a set of distinct arcs that can be arranged as $\alpha_1(v_0v_1),\alpha_2(v_1v_2),\dots,\alpha_m(v_{m-1}v_m)$ with $v_0=u$, $v_m=w$ and the vertices $v_0,\dots,v_m$ pairwise distinct; each arc may be traversed in either direction. The null chain ($m=0$) joins $u$ to itself.

A flow $f$ assigns a number $f(C)\ge 0$ to each chain $C$ joining $a$ and $b$ (and $0$ to every other set of arcs) such that the load $\ell_f(e)=\sum_{C\ni e}f(C)$ satisfies $\ell_f(e)\le c(e)$ for every arc. Its value is $\mathrm{val}(f)=\sum_C f(C)$. An arc is saturated by $f$ if $\ell_f(e)=c(e)$. A maximal flow is a flow of largest value.

A set $D$ of arcs is a disconnecting set if every chain joining $a$ and $b$ contains an arc of $D$; its value is $v(D)=\sum_{e\in D}c(e)$. A cut is a disconnecting set no proper subset of which is disconnecting.

The proof introduces two further objects: the set $S$ of arcs saturated by every maximal flow, and the set $L\subseteq S$ of left arcs, those arcs of $S$ whose left vertex (the end vertex met first by a positive chain flow of a maximal flow, travelling from $a$) can be reached from $a$ by a chain with no arc saturated by some maximal flow.

Formalization targets

Goal: Theorem 1 (Minimal cut theorem), p. 400

$$\exists\, m\in\mathbb R:\quad m=\max_{f\ \text{flow}}\mathrm{val}(f)=\min_{D\ \text{disconnecting}}v(D),$$

with both the maximum and the minimum attained. The statement mentions only flows and disconnecting sets, not the proof objects $S$ and $L$.

Milestones, in the order of the paper's proof

1. A maximal flow exists, and the set of maximal flows is convex (p. 400).
2. Lemma 1: $S$ is a disconnecting set (p. 400).
3. Every arc of $S$ receives the same orientation from all positive chain flows of all maximal flows: its left vertex is unique (pp. 400–401).
4. Lemma 2: $L$ is a disconnecting set (p. 401).
5. Lemma 3: no positive chain flow of a maximal flow contains more than one arc of $L$ (p. 401).
6. $\mathrm{val}(f)\le v(D)$ for every flow $f$ and every disconnecting set $D$ (p. 402).
7. $L$ is a cut of minimal value, and every maximal flow has value $v(L)$ (p. 402).

Two further statements of the paper are included as items without being milestones: the remark that a disconnecting set of minimal value is a cut (p. 400), and the Corollary (p. 402): if a set $A$ of arcs meets every cut in exactly one arc, adding $k$ to the capacity of each arc of $A$ raises the maximal flow value by $k$.

Significance

The minimal cut theorem turns a maximization over flows into a minimization over finite sets of arcs, so an optimal flow comes with a short certificate of optimality. It implies Menger's theorem (unit capacities), and through it König's theorem on bipartite matchings and Hall's marriage theorem. The Corollary is the tool behind the paper's own computing procedure for source–sink planar networks (§2, formalized in a companion mission).

The theorem is classical and proved. What this mission adds is a machine-checked proof of the paper's own formulation: undirected arcs, parallel arcs, flows decomposed along chains (path flows, with no circulations), and the minimum taken over arc sets meeting every chain, together with the proof's intermediate claims. Max-flow min-cut theorems already on the platform (Applied Combinatorics VIII, AppliedComb.Flows.max_flow_min_cut; Introduction to Linear Optimization X, LinearOptimization.max_flow_min_cut) concern directed networks with edge flows obeying conservation and cuts given by vertex sets. They are related results, not this statement, and connecting the two models is itself welcome work.

Difficulty

Weak duality (milestone 6) is immediate; the content is the reverse inequality. The obvious first step, taking a maximal flow and observing that its saturated arcs separate $a$ from $b$, does not finish the proof: a positive chain flow may pass through several saturated arcs, so the total capacity of the saturated arcs can exceed the flow value. One has to single out a disconnecting subset that every positive chain flow crosses exactly once, and there is no canonical choice from a single flow. The paper's sets $S$ and $L$ are defined from all maximal flows at once, and the work consists in showing that these sets are well behaved. The orientation claim in particular needs an exchange argument on two chains that cross at an arc, where the recombined arc sequences may revisit vertices and must be reduced to chains. In a formal development this "a walk contains a chain" step and the averaging of maximal flows over finitely many chains are the main bookkeeping costs.

Formalization scope

• A network is a structure on a vertex type V and an arc type E, both Fintype with decidable equality, with end-vertex maps tail, head (labels only, no direction), tail e ≠ head e, a source and a sink with source ≠ sink, and capacities cap : E → ℝ with 0 < cap e. These are the paper's standing assumptions; there are no others in §1. In particular, no planarity is assumed and an arc may join $a$ and $b$ directly.
• A chain is a Finset E that is the arc set of some arrangement (list of arcs, list of pairwise distinct vertices, each arc joining consecutive vertices in either order).
• A flow is a function f : Finset E → ℝ, non-negative, zero off the chains joining source and sink, with every arc load at most the capacity. A collection of chain flows that lists a chain twice merges into this form without changing the value or any load.
• "Maximal" means of maximum value. The goal is stated with IsGreatest and IsLeast on the sets of flow values and of values of disconnecting sets, so no supremum of a real set appears and both extrema must be attained.
• A trivializing formalization is ruled out: chains must be self-avoiding and must join the source and the sink, the disconnecting condition quantifies over exactly these chains, and the minimum ranges over all disconnecting sets rather than over a family chosen to match a given flow.
• Needed infrastructure: finite sums over Finset (Finset E), convexity in Finset E → ℝ, compactness of the flow polytope (for existence), and lemmas on lists (extracting a chain from a walk). The walk-to-chain lemma and weak duality are reusable for the companion mission and for any path-flow model.

Selected references

• L. R. Ford, Jr. 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
• K. Menger, Zur allgemeinen Kurventheorie, Fundamenta Mathematicae 10 (1927), 96–115. https://doi.org/10.4064/fm-10-1-96-115
• L. R. Ford, Jr. and D. R. Fulkerson, Flows in Networks, Princeton University Press, 1962.
• J. Edmonds and R. M. Karp, Theoretical improvements in algorithmic efficiency for network flow problems, Journal of the ACM 19 (1972), 248–264. https://doi.org/10.1145/321694.321699
• A. Schrijver, On the history of the transportation and maximum flow problems, Mathematical Programming 91 (2002), 437–445. https://doi.org/10.1007/s101070100259

Motivation

A matching in a graph is a set of edges no two of which share a node. Given a real weight on every edge, the maximum-weight matching problem asks for a matching of largest total weight. It is one of the basic problems of combinatorial optimization: assignment, pairing and scheduling problems reduce to it, and it is the standard example of a combinatorial problem that is solvable in polynomial time although it is not obviously a linear program.

For bipartite graphs the problem is a linear program in disguise: the polytope cut out by nonnegativity and the node-degree inequalities has only 0–1 vertices (the Birkhoff–von Neumann theorem in the square case; Mathlib has it as extremePoints_doublyStochastic). For general graphs this fails already on a triangle, where the vector with every coordinate $1/2$ satisfies all degree inequalities but is not a combination of matchings. Edmonds' 1965 paper (DOI 10.6028/jres.069b.013) adds one family of inequalities, one for each odd set of nodes, and proves that the resulting polyhedron has exactly the matching vectors as its vertices. The companion paper Paths, trees, and flowers gives the cardinality algorithm on which the weighted algorithm of §7 is built.

Timeline:

• 1931: König and Egerváry prove the min–max theorems for bipartite matching; 1946: Birkhoff shows that the doubly stochastic matrices are the convex hull of the permutation matrices (the bipartite perfect-matching polytope).
• 1947: Tutte characterizes graphs with a perfect matching.
• 1965: Edmonds, Paths, trees, and flowers: the blossom algorithm for maximum-cardinality matching.
• 1965: Edmonds, this paper: Theorem (P) (the matching polyhedron) and Theorem (M) (blossom-shrinking optimality certificates), with a weighted matching algorithm.

Setting

Let $G$ be a finite graph with node set $V$ and edge set $E$; each edge meets two different nodes, its ends. Real variables $x_e$ correspond to the edges $e\in E$. The polyhedron $C\subseteq\mathbb R^E$ is the set of vectors $x$ satisfying

1. $x_e\ge 0$ for every edge $e$;
2. $\sum_{e \text{ meets } v} x_e\le 1$ for every node $v$;
3. $\sum_{e \text{ has both ends in } S} x_e\le r$ for every set $S$ of $2r+1$ nodes, $r$ a strictly positive integer.

The matching vectors $P$ are the vectors with every component $0$ or $1$ that satisfy (2); they are the incidence vectors of matchings. For edge weights $c\in\mathbb R^E$, the linear form (4) is $W(c,x)=\sum_e c_e x_e$.

The dual program has a variable $y_v$ for each node and $z_S$ for each odd set $S$ ($|S|=2r_S+1$, $r_S\ge1$). Its objective is (5) $U(y,z)=\sum_v y_v+\sum_S r_S z_S$, subject to (6) $y,z\ge0$ and (7) $y_{v_1}+y_{v_2}+\sum_{S\ni v_1,v_2}z_S\ge c_e$ for every edge $e$ with ends $v_1,v_2$. For a matching $M$, conditions (8)–(10) are the complementary slackness conditions: $y_v=0$ at nodes not covered by $M$, equality in (7) on $M$, and every odd set with $z_S>0$ contains exactly $r_S$ edges of $M$.

A blossom sequence $\{G_i\}_{i=0}^n$ (Theorem (M)) starts from $G_0=G$ with matching $M_0=M$ and repeatedly shrinks an odd circuit $B_i$ (a blossom, $2a_i+1$ edges of which $a_i$ are matched) to a single node, carrying node weights $w(v^i)$ and edge weights $w(e^i)$ that obey conditions (a)–(k) of p. 127.

In the Lean development these are Graph, IsMatching, incidence, matchingPolyhedron ($C$), matchingVectors ($P$), W, U, DualFeasible ((6)–(7)), CompSlack ((8)–(10)) and BlossomSequence, all in the namespace EdmondsMatching65.Polyhedron.

Formalization targets

Goal: Theorem (P)

$$\operatorname{ext}(C)=P.$$

The vertices (extreme points) of $C$ are exactly the matching vectors of $G$. Hence the maximum weight of a matching equals $\max\{W(c,x):x\in C\}$ for every $c$.

Milestones

1. $P\subseteq\operatorname{ext}(C)$ (§2, p. 126).
2. If for every $c$ some 0–1 point of $C$ maximizes $W(c,\cdot)$ over $C$, then $\operatorname{ext}(C)=P$ (§2, p. 126).
3. Weak duality: $W(c,x)\le U(y,z)$ for $x\in C$ and $\langle y,z\rangle$ satisfying (6)–(7) (§3, p. 126).
4. If $M$ is a matching and $\langle y,z\rangle$ satisfies (6)–(10), then $W(c,\chi^M)=U(y,z)$ (§3, p. 127).
5. A blossom sequence for $M$ yields $\langle y,z\rangle$ satisfying (6)–(10) (§5, pp. 127–128).
6. For every $c$ some maximum matching has a blossom sequence (§6, p. 128).
7. Theorem (M): a matching is maximum if and only if a blossom sequence for it exists (§4, p. 127).
8. For every $c$ there are a matching $M$ and $\langle y,z\rangle$ satisfying (6)–(10) (§3, p. 127).

Significance

The result. Theorem (P) turns maximum-weight matching in general graphs into a linear program over an explicitly described polyhedron, and Theorem (M) with the §5 translation gives a short certificate of optimality for every maximum matching. Together they established the template of polyhedral combinatorics: describe the convex hull of the combinatorial objects by inequalities, and prove the description through linear programming duality and an algorithm. The matching polytope underlies the analysis of the weighted blossom algorithm, separation over odd-set inequalities (Padberg–Rao), and many later integrality results; Edmonds' own §8 states the extension to degree-constrained subgraphs.

Formalizing it. The theorem has been proved since 1965 and appears in every text on combinatorial optimization; this mission asks for a machine-checked proof of the polytope statement for general finite graphs, including parallel edges, together with the duality certificate and the blossom-sequence characterization. The prove2me platform has a proved form of Edmonds' perfect matching polytope theorem on complete graphs in convex-decomposition form (MetricTSP.pm_polytope_decomposition), a different polytope with a different conclusion; nothing states Theorem (P) or Theorem (M).

Difficulty

The inclusion $P\subseteq\operatorname{ext}(C)$ and weak duality are routine. The difficulty is the reverse inclusion: showing that no fractional point of $C$ is a vertex. The bipartite argument (a fractional point has a cycle of fractional edges along which it can be perturbed both ways) breaks on odd cycles: perturbing along an odd circuit violates a degree inequality, and the odd-set inequalities that cut off the half-integral points are exponentially many and overlap. The paper's route needs, for every weight vector, an optimal matching together with a dual solution satisfying (6)–(10), and the existence of that certificate is the substance of the weighted matching algorithm: the blossom sequence of Theorem (M) must be constructed, and the translation (11)–(16) from node and edge weights of the contracted graphs to $\langle y,z\rangle$ must be verified through the whole shrinking history.

Formalization scope

• The graph is a finite node type V, a finite edge type E and an end map ends : E → Sym2 V with no loops. Parallel edges are allowed: the contracted graphs of Theorem (M) have them, and Theorem (P) holds for multigraphs; simple graphs are the case of an injective end map.
• Vectors are E → ℝ, one coordinate per edge. Vertices are Mathlib's Set.extremePoints ℝ. Odd sets carry an explicit r : ℕ with 1 ≤ r and |S| = 2r + 1; even sets and singletons carry no inequality.
• Edge weights are arbitrary reals; matchings need not be perfect and may be empty. No connectivity, no parity of |V|.
• The dual variable z is a function on all node sets of which only odd sets are read.
• A contracted graph Gᵢ is a partition of V into blocks; an edge of G is an edge of Gᵢ when its ends lie in different blocks. Each Mᵢ must be a matching of Gᵢ, and all of (a)–(k) appear as fields of BlossomSequence; a sequence missing any of them would make milestone 6 trivial or milestone 5 false.
• A trivializing formalization is ruled out: coordinates indexed by node pairs (Sym2 V → ℝ) leave non-edge coordinates free and give a polyhedron with no extreme points, and the goal is stated as equality of extreme points, not as a convex-hull identity or as the existence of a dual certificate.
• Needed infrastructure: extreme points of polyhedra as unique maximizers of linear forms, finite LP weak duality over these index sets, and the weighted blossom algorithm (or another proof of milestone 8). The polyhedral lemmas are reusable for other integrality results; contributions on any milestone are welcome.

Selected references

• J. Edmonds, Maximum Matching and a Polyhedron With 0,1-Vertices, J. Res. Nat. Bur. Standards Sect. B 69B (1965), 125–130. https://doi.org/10.6028/jres.069b.013
• J. Edmonds, Paths, Trees, and Flowers, Canad. J. Math. 17 (1965), 449–467. https://doi.org/10.4153/CJM-1965-045-4
• W. T. Tutte, The Factorization of Linear Graphs, J. London Math. Soc. 22 (1947), 107–111. https://doi.org/10.1112/jlms/s1-22.2.107
• M. W. Padberg, M. R. Rao, Odd Minimum Cut-Sets and b-Matchings, Math. Oper. Res. 7 (1982), 67–80. https://doi.org/10.1287/moor.7.1.67
• A. Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Springer, 2003, Chapter 25.

Motivation

The solution concept of von Neumann and Morgenstern's Theory of Games and Economic Behavior (1944) is defined from two ingredients: a set of imputations and a domination relation between them. A solution is a set of imputations that is internally stable (no member dominates another) and externally stable (every non-member is dominated by some member). In §65 of the book the authors observe that this definition never uses what imputations and domination actually are. They abstract it to an arbitrary set $D$ and an arbitrary relation $\mathcal S$ on $D$, and ask which properties of $\mathcal S$ guarantee that exactly one solution exists.

The abstract notion is what graph theory now calls a kernel of a directed graph: draw an arc $x \to y$ whenever $x\mathcal S y$; a solution is a set of vertices that is independent and absorbs every vertex outside it. Kernels appear in combinatorial game theory (the losing positions of a finite impartial game form a kernel of its move graph) and in the theory of preference and choice.

Timeline.

• 1944 (1st ed.; 3rd ed. 1953, reprinted 2007): von Neumann and Morgenstern define solutions for an arbitrary relation (§65), show that a finite set with an acyclic relation has exactly one solution (65:X), and that acyclicity is necessary for every subset to have a unique solution (65:Z).
• 1953: M. Richardson, Solutions of irreflexive relations, extends existence (not uniqueness) to finite relations without cycles of odd length.

Setting

Let $D$ be an arbitrary set and $\mathcal S$ an arbitrary relation on $D$; $x\mathcal S y$ is read "$x$ dominates $y$". A solution (in $D$ for $\mathcal S$) is a set $V \subseteq D$ with

$$\text{(65:1)}\qquad V = \{\, y \in D : x\mathcal S y \text{ holds for no } x \in V \,\}.$$

For $E \subseteq D$, an element $x$ is a maximum of $E$ if $x \in E$ and no $y \in E$ has $y\mathcal S x$; the set of maxima is $E^m$.

For $m \ge 1$, condition $(A_m)$ says: never $x_1\mathcal S x_0, x_2\mathcal S x_1, \dots, x_m\mathcal S x_{m-1}$ with $x_0 = x_m$ and all $x_i \in D$. The relation is acyclic if it satisfies every $(A_m)$, $m = 1, 2, \dots$; in particular never $x\mathcal S x$. It is strictly acyclic if there is no infinite sequence $x_0, x_1, x_2, \dots$ in $D$ with $x_{i+1}\mathcal S x_i$ for every $i$. Property (65:K) says that every non-empty $E \subseteq D$ has $E^m \ne \ominus$. A partial ordering (65:B) is a transitive relation for which at most one of $x = y$, $x\mathcal S y$, $y\mathcal S x$ holds.

For the main theorem the book constructs a candidate solution by induction (65.7.1): $A_1 = D$; $B_i = A_i^m$; $C_i$ is the set of elements of $A_i$ dominated by some element of $B_i$; $A_{i+1} = A_i - B_i - C_i$. With $i_0$ the first index for which $A_{i_0} = \ominus$,

$$\text{(65:2)}\qquad V_0 = B_1 \cup \cdots \cup B_{i_0 - 1}.$$

In Lean the elements live in a type α, D V : Set α, and S : α → α → Prop with S x y meaning $x\mathcal S y$; the predicates are IsSolution D S V, maxima E S, IsAcyclic, IsStrictlyAcyclic, HasMaximaProperty, IsPartialOrdering, ConditionG, and the construction stageA, stageB, stageC, V0.

Formalization targets

Goal: (65:X)

If $D$ is finite and $\mathcal S$ is acyclic on $D$, then

$$\exists!\, V:\ V \text{ is a solution in } D \text{ for } \mathcal S, \qquad\text{and}\qquad V \text{ is a solution} \iff V = V_0 .$$

Milestones, in attack order

1. (65:I) For a partial ordering, a finite $D$ satisfies (65:G): every non-maximal $y$ is dominated by some maximum.
2. (65:H) For a partial ordering of an arbitrary $D$: $V$ is a solution $\iff$ (65:G) holds and $V = D^m$.
3. (65:O:c) Strict acyclicity implies acyclicity; for finite $D$ the two are equivalent.
4. (65:P) (65:K) $\iff$ strict acyclicity, for arbitrary $D$.
5. (65:S) For finite $D$ and acyclic $\mathcal S$, some $A_i$ is empty.
6. (65:V) For finite $D$ and acyclic $\mathcal S$, every solution equals $V_0$.
7. (65:W) For finite $D$ and acyclic $\mathcal S$, $V_0$ is a solution.
8. (65:Z) If every $E \subseteq D$ has a unique solution in $E$ for $\mathcal S$, then $\mathcal S$ is acyclic on $D$.

Significance

The result itself. (65:X) is the most general of the book's three existence-and-uniqueness theorems for solutions (complete ordering, partial ordering, acyclic relation; 65.8.1). For games proper it has no direct application: the set of imputations of an essential game has no maxima, so (65:K) fails (65.9.1). Its role is to isolate a sufficient condition for a unique solution. With (65:Z), and applied to every subset of $D$, it characterizes the finite relations for which every subset has exactly one solution: exactly the acyclic ones (65.8.2). In graph language it is the statement that a finite directed acyclic graph has exactly one kernel. In combinatorial game theory this is the partition of the positions of a finite impartial game into P- and N-positions. The complete- and partial-ordering results (65:E)–(65:I) are the special cases the book treats first.

Formalizing it. The results are classical and fully proved in the book; to the best of our knowledge none of them is on the Prove2Me platform, and Mathlib has well-foundedness (WellFounded, RelEmbedding of ℕ) but no kernel or von Neumann–Morgenstern solution notion for an abstract relation. The mission produces machine-checked proofs of the book's §65 chain: the equivalence of (65:K) with strict acyclicity for arbitrary sets, the finite equivalence of acyclicity and strict acyclicity, the explicit construction of $V_0$, and the characterization of 65.8.2.

Difficulty

Most of the individual steps are short. The work is in making the book's finite induction precise. The sets $A_i$ are defined recursively and $V_0$ refers to the first empty stage $i_0$. The uniqueness proof (65:V) is a minimal-counterexample argument over the stage index, which moves between "smallest $k$ with $y \notin A_k$" and the disjoint decomposition (65:U) of $D$ into the $B_i$ and $C_i$. A tempting shortcut, taking an arbitrary well-founded rank function instead of the book's construction, proves existence and uniqueness but not that the solution is the $V_0$ of (65:2), which is part of the goal. For (65:P) and (65:O:c) the difficulty is the passage between finite cycles and infinite chains. Going from a chain in a finite set to a repetition needs a pigeonhole argument, and going from a set without maxima to a chain needs dependent choice.

Formalization scope

• Representation. An ambient type α; D, E, V are Set α; the relation is S : α → α → Prop and is only ever consulted on elements of the set under consideration, so it is the book's relation on $D$ (or its restriction to $E$). Finite and infinite sequences are functions ℕ → α.
• Solutions. IsSolution D S V is the set equation (65:1) literally; it forces $V \subseteq D$. Uniqueness in the goal is ∃! over all V : Set α, not over a subtype; there is no degenerate reading in which the solution is fixed by construction.
• Acyclicity. IsAcyclic D S requires $(A_m)$ for every $m \ge 1$, all cycle elements in $D$. The case $m = 0$ is excluded, as in the book (it would be unsatisfiable). This is equivalent to the absence of a Relation.TransGen loop inside $D$, but the book's form is stated.
• Construction. Stages are indexed from $0$: stageA D S k is the book's $A_{k+1}$. V0 D S is the union of all $B_i$, which equals $B_1 \cup \cdots \cup B_{i_0 - 1}$ because every later $B_i$ is empty.
• Standing hypotheses instantiated. (65:S), (65:V), (65:W) and the goal (65:X) carry the hypotheses of 65.7.1, "$D$ finite and $\mathcal S$ acyclic" (for finite $D$ equivalently strictly acyclic, i.e. (65:K)), as D.Finite and IsAcyclic D S. (65:H) and (65:I) carry the partial-ordering hypothesis (65:B:a), (65:B:b) of 65.5.1, and (65:I) also finiteness of $D$. (65:O:c), (65:P) and (65:Z) are for arbitrary $D$ and $\mathcal S$, as 65.6.2 and 65.8.2 state. The empty $D$ is allowed everywhere; there the unique solution is $\ominus$.
• Not stated. The infinite case of (65:X) and of (65:Y), which the book leaves open (65.7.1, 65.8.3, question (65:9)); the complete-ordering results (65:E), (65:F), which silently assume $D \neq \ominus$; the counting statement (65:8).
• Needed infrastructure. Finite-set induction and pigeonhole on Set.Finite, dependent choice for (65:P). The definitions are reusable for any later work on kernels of digraphs and on abstract stable sets. Proofs of any milestone, and alternative proofs of the goal, are welcome.

Selected references

• J. von Neumann and O. Morgenstern, Theory of Games and Economic Behavior, 60th-anniversary edition, Princeton University Press, 2007 (reprint of the 3rd ed., 1953), §65, pp. 587–602. https://doi.org/10.1515/9781400829460
• M. Richardson, Solutions of irreflexive relations, Annals of Mathematics 58 (1953), 573–590. https://doi.org/10.2307/1969755

Motivation

Many collective decisions are taken by coalitions that either carry the vote or do not: committees, legislatures, shareholder meetings, councils with weighted votes. In such a situation the only aim of a participant is to be part of a coalition that wins, and nothing is left to bargain about except the division of the prize inside the winning coalition. Chapter X of von Neumann and Morgenstern's Theory of Games and Economic Behavior (1944; 3rd ed. 1953) isolates exactly this class of zero-sum $n$-person games, the simple games, and studies their numerical description by weighted majorities and their finite main simple solutions.

The chapter is the origin of a large later literature: simple games and weighted voting games are the standard model of voting bodies in political science and social choice (for instance the Shapley–Shubik power index, 1954). The characterization of which simple games admit homogeneous weights, and the solutions they carry, starts here.

Setting

A zero-sum $n$-person game with players $I = \{1, \dots, n\}$ is represented by its characteristic function $v$, a real function on the subsets of $I$ with $v(\ominus) = 0$, $v(-S) = -v(S)$ ($-S$ the complement) and $v(S \cup T) \geqq v(S) + v(T)$ for disjoint $S, T$. An imputation is a vector $\vec\alpha$ with $\alpha_i \geqq v((i))$ and $\sum_i \alpha_i = 0$; $\vec\alpha$ dominates $\vec\beta$ if some nonempty $S$ has $\sum_{i\in S}\alpha_i \leqq v(S)$ and $\alpha_i > \beta_i$ for $i \in S$; a solution is a set $V$ of imputations none of which dominates another and which dominates every imputation outside it (30.1.1). The game is inessential when its reduced form vanishes identically, essential otherwise.

A coalition $S$ is flat if $v(S) = \sum_{k\in S} v((k))$. The losing coalitions $L_\Gamma$ are the flat sets, and the winning coalitions $W_\Gamma$ are the sets whose complement is flat. The game is simple if it is essential and every coalition is winning or losing. $W^m$ denotes the minimal winning coalitions, those of which no proper subset wins.

Weights $w_1, \dots, w_n$ define the winning system $W = \{S : \sum_{i\in S} w_i > \tfrac12 \sum_i w_i\}$, and under the conditions (50:B) (non-negative weights, no player with half the total weight, no ties) this is the weighted majority game $[w_1,\dots,w_n]$. The weights are homogeneous if the advantage $a_S = \sum_{i\in S} w_i - \sum_{i\in -S} w_i$ is the same for all $S$ in $W^m$.

In §50 the game is taken in reduced form with $\gamma = 1$, so $v((i)) = -1$. For numbers $x_i \geqq 0$ and a coalition $S$ let $\vec\alpha^S$ give $-1$ to the players outside $S$ and $-1 + x_i$ to player $i$ in $S$. When the $x_i$ satisfy $\sum_{i \in S} x_i = n$ for every $S \in W^m$, the set $V$ of all $\vec\alpha^S$, $S \in W^m$, is a main simple solution.

Formalization targets

Goal: (50:K), p. 444

$$\text{Every homogeneous weighted majority game possesses a main simple solution,}$$

namely the set of $\vec\alpha^S$, $S \in W^m$, with $x_i = \frac{n}{b} w_i$, $b = \frac12(\sum_i w_i + a)$, $a$ the common advantage. Conversely, if $x_i \geqq 0$ solve $\sum_{i\in S} x_i = n$ on $W^m$, then $w_i = x_i$ are homogeneous weights for the game if and only if

$$\sum_{i=1}^n x_i < 2n .$$

Milestones

1. (49:C) $L_\Gamma$ contains the empty set and all one-element sets.
2. (49:A) $W_\Gamma, L_\Gamma$ are mapped onto each other by complementation, $W_\Gamma$ is closed under supersets, and $L_\Gamma$ is closed under subsets.
3. (49:B) $W_\Gamma \cap L_\Gamma = \ominus$ if and only if the game is essential. If the game is inessential, every set is both winning and losing.
4. (49:F) The pairs $W, L$ of simple games are exactly those satisfying (48:A:a)–(48:A:d) and (49:C).
5. (50:A) The essential three-person game is simple: it is the direct majority game.
6. (50:B) Non-negative weights define a winning system with (49:W*) if and only if (50:B:a), (50:B:b) hold.
7. (50:D) $a_S > 0$ on $W$, $a_S < 0$ on $L$, and $a_S = 0$ never occurs.
8. (50:G) An imputation $\vec\beta$ is undominated by $V = \{\vec\alpha^S : S \in U\}$ if and only if $R(\vec\beta) \in U^+$.
9. (50:J) The exact criterion (50:8*), (50:9*) for $V$ to be a solution.

Significance

The result links two descriptions of a simple game. One is numerical: a vector of weights, normalized by homogeneity. The other is game-theoretic: a finite solution in which each minimal winning coalition forms and divides a fixed total among its members. When the weights are homogeneous they are, up to scale, the shares in the main simple solution. When a main simple solution exists, its shares are homogeneous weights exactly under the inequality (50:20). The criterion (50:J) behind it is the chapter's general tool for deciding which systems of "profitable" minimal winning coalitions yield a finite solution. It is used again in the enumeration of simple games in §§51–55.

All of the results are proved in the book. As far as a search of the Prove2Me library shows (queries on simple game, weighted majority, winning coalition and stable set, 2026-09-28), none of them has been machine-checked. The only stable-set statements on the platform concern feasible payoff vectors of convex games, which is a different domain. The mission therefore asks for a formal proof of the known results, including the case analysis of §50.5–50.6, and in doing so it produces a reusable Lean theory of simple games and their winning systems.

Difficulty

The characterizations of §49 are set-theoretic, but they depend on superadditivity to show that subsets of flat sets are flat, and on the strategic-equivalence description of essentiality. The substantial part is (50:J). Deciding whether $V$ is a solution means classifying every imputation $\vec\beta$ by the set $R(\vec\beta)$ where it meets the shares $-1 + x_i$.

The natural first attempt is to check only the minimal winning coalitions. It fails, because domination can be exercised through any winning coalition. The book's argument has to exclude sets of $U^+$ with $\sum_{i\in T} x_i < n$ by producing infinitely many undominated imputations against a finite $V$. It also has to handle indifferent players with $x_i = 0$, whose presence makes $R(\vec\beta)$ larger than the coalition that generated $\vec\beta$. For the converse half of the goal, the obstacle is the strict inequality $a > 0$: the equations (50:17) are linear and say nothing about it.

Formalization scope

Players are Fin n (the book's player $i$ is index $i - 1$), coalitions are Finset (Fin n), and characteristic functions are Finset (Fin n) → ℝ. Imputations are vectors Fin n → ℝ, and systems of coalitions are Set (Finset (Fin n)). A game is identified with its characteristic function (by 26.1 every $v$ satisfying (25:3:a)–(25:3:c) arises from a game). The theory is the "old" one of 30.1.1 (49.1.1), with no excess. The definitions of imputation, domination and solution are the same as in mission V of this series and are restated here, because a draft cannot import another draft.

The standing hypotheses, stated in each theorem where the book has them in force:

• (25:3:a)–(25:3:c) on $v$ in every theorem;
• simplicity (essential + (49:1:b)) in (50:G), (50:J), (50:K);
• the reduced form with $\gamma = 1$, as $v((i)) = -1$ for all $i$ (50.4.1), in (50:G), (50:J), (50:K);
• $U \subseteq W^m$, (50:7) $x_i \geqq 0$ and (50:8) $\sum_{i\in S} x_i = n$ for $S \in U$ (50.5.1) in (50:G), (50:J);
• (50:B) on the weights in (50:D) and in the first half of (50:K);
• non-negative weights in (50:B). The book states (50:B) for arbitrary real weights, but its "only if" direction is false without $w_i \geqq 0$: $[10, 10, 10, -\tfrac1{10}]$ is a counterexample. The corrected statement is recorded in the item.

The numbers $x_i$ are given for every player. Players in no minimal winning coalition, for whom the book defines no $x_i$, do not affect any $\vec\alpha^S$. In the converse of (50:K) the derived weights are $w_i = x_i$ for every player.

The goal is not the bare solvability of (50:17). A statement that only asserted "$x$ exists with (50:7), (50:17)" would reduce to linear algebra. The goal asserts that the set of $\vec\alpha^S$ is a solution in the sense of 30.1.1, with domination requiring a nonempty effective set, and it adds the converse equivalence with (50:20). The set $V$ is built from $W^m$ only, never from all of $W$.

Welcome contributions: proofs of the §49 milestones, which form a small reusable library on winning and losing systems; a proof of (50:G) and (50:J); and lemmas connecting $W_\Gamma$ of a simple reduced game with the explicit formula (49:2), $v(S) = n - |S|$ on $W$ and $-|S|$ on $L$.

Selected references

• J. von Neumann, O. Morgenstern, Theory of Games and Economic Behavior, 60th-anniversary ed., Princeton University Press, 2007 (reprint of the 3rd ed., 1953), Chapter X, §§48–50, pp. 420–444. https://doi.org/10.1515/9781400829460
• L. S. Shapley, M. Shubik, "A method for evaluating the distribution of power in a committee system", American Political Science Review 48 (1954) 787–792. https://doi.org/10.2307/1951053