Why the assignment dual matters

The subgradient method maximizes a concave, piecewise-linear function $w(\pi)=\min_k\{c_k+\pi\cdot v_k\}$ by moving along a subgradient $v_k$ of an active piece with a prescribed step. Held, Wolfe and Crowder's 1974 paper Validation of subgradient optimization tested the method on three families of Lagrangean duals from combinatorial optimization — the assignment problem, a relaxation of the travelling salesman problem in the style of Held and Karp, and multicommodity flows — and gave the first systematic account of when the method works in practice.

On randomly generated assignment problems of order $n\le 30$ the authors observed that the method usually did not merely converge: it stopped, after finitely many steps, at an iterate whose subgradient was exactly zero. Their explanation is a structural fact about the assignment dual, Theorem 3.1 of the paper: when the optimal assignment is unique — the typical case for random integer costs — the set of optimal dual prices has full dimension $n$, so a sequence of steps of decreasing length can land inside it. This mission formalizes that theorem and the steps of its proof.

Setting

There are $n$ men and $n$ jobs, and a real $n\times n$ cost matrix $A=(a_{ir})$: $a_{ir}$ is the cost for which man $i$ does job $r$. A one-to-one assignment is a permutation $\sigma$ of $\{1,\dots,n\}$, where $\sigma(r)$ is the man doing job $r$; its cost is $\sum_r a_{\sigma(r)\,r}$. The assignment problem (3.1) asks for a permutation of minimal cost; the assignment is unique if exactly one permutation attains that minimum.

The linear relaxation of (3.1), over doubly stochastic matrices $x=(x_{ir})$, has the dual linear program (3.2), $\max\{\sum_i\pi_i+\sum_r\rho_r : \pi_i+\rho_r\le a_{ir}\}$. For fixed prices $\pi\in\mathbb R^n$ on the men the best $\rho$ is $\rho_r=\min_s[a_{sr}-\pi_s]$, which leaves the dual function (3.3)

$$w(\pi)=\sum_{i=1}^n\pi_i+\sum_{r=1}^n\min_s\,[a_{sr}-\pi_s],$$

the inner minimum being over the men $s$ for each job $r$. The optimal set is $\Omega=\{\pi : w(\pi')\le w(\pi)\ \text{for all }\pi'\}$.

To put $w$ in the form $\min_k\{c_k+\pi\cdot v_k\}$ the paper uses assignments in a weaker sense: arbitrary functions $A:\{1,\dots,n\}\to\{1,\dots,n\}$, $n^n$ of them, with cost $c_A=\sum_r a_{A(r)\,r}$ and vector $(v_A)_i=1-\#\{r:A(r)=i\}$ (3.4). The subgradient step raises the price of a man assigned no job and lowers the price of a man assigned several; $v_A=0$ exactly when $A$ is a permutation.

In the Lean development these are assignCost, assignVec, IsOptimalAssignment, w and optSet in the namespace HeldWolfeCrowder.Assignment.

Formalization targets

Goal: Theorem 3.1 (p. 70)

If the assignment problem has a unique optimal permutation, then

$$\dim\operatorname{aff}\,\Omega=n .$$

The hypothesis is uniqueness among permutations; the conclusion is the dimension of the affine hull of the optimal set.

Milestones, in the order the proof uses them

1. Eq. (3.4): $w(\pi)=\min_A\{c_A+\sum_i\pi_i(v_A)_i\}$ over all $n^n$ assignments $A$.
2. §3, Eqs. (3.1)–(3.3): $w$ attains its maximum, and $\max w$ equals the cost of an optimal permutation.
3. Eq. (3.5): if $\sigma$ is the unique optimal permutation, some maximizer $\bar\pi$ of $w$ has, for every job $r$, the minimum $\min_s[a_{sr}-\bar\pi_s]$ attained only at $s=\sigma(r)$.
4. Eq. (3.6): for an optimal permutation $\sigma$, the set $\Pi=\{\pi : a_{ir}-\pi_i>a_{\sigma(r)\,r}-\pi_{\sigma(r)}\ \text{for all } r,\ i\ne\sigma(r)\}$ is convex and open, $v=0$ on it, and $\Pi\subseteq\Omega$.

Significance

The theorem turns an empirical observation into a statement about the problem: finite termination of the subgradient method on assignment problems is a property of the dual, not luck. Since $w$ is unchanged by adding the same constant to every price, $\Omega$ always contains a line; Theorem 3.1 says that, under uniqueness, it is as large as it can be. The paper (p. 70) cites the argument of its Section 2 that, with a full-dimensional optimal set, termination of the method is "nearly certain".

The result is proved in the paper; none of it is known to be machine-checked. What the formalization adds is a checked link between three classical ingredients: the integrality of the assignment polytope (Birkhoff–von Neumann, which Mathlib has as doublyStochastic_eq_convexHull_permMatrix), linear-programming duality, and strict complementary slackness, which neither Mathlib nor the platform has in the form needed. The piecewise-linear representation (3.4) is reusable wherever the assignment dual appears as a Lagrangean subproblem.

Difficulty

The inclusion $\Pi\subseteq\Omega$ is elementary; the substance is that $\Pi$ is nonempty. The obvious candidate — any optimal dual solution — fails: an optimal $\pi$ may leave ties $a_{sr}-\pi_s=a_{\sigma(r)\,r}-\pi_{\sigma(r)}$ for some $s\ne\sigma(r)$, so it sits on the boundary of $\Omega$ and shows nothing about dimension. What is needed is an optimal price vector with all these inequalities strict at once, and uniqueness of the optimal permutation is a statement about the primal side only; transferring it to the dual side goes through the linear relaxation (3.1), whose uniqueness is not the hypothesis, and through a strict complementarity property that is not available in Mathlib or on the platform.

Formalization scope

Men and jobs are both Fin n; the costs are a : Matrix (Fin n) (Fin n) ℝ with a i r the cost of man i on job r; prices are π : Fin n → ℝ (no inner product or norm is needed, so no EuclideanSpace). The inner minimum of (3.3) is Finset.univ.inf' over the men, well defined for every n. One-to-one assignments are Equiv.Perm (Fin n) with σ r the man doing job r, so the orientation of the matrix matches (3.3); arbitrary assignments are functions Fin n → Fin n. "Of dimension $n$" is Module.finrank ℝ (vectorSpan ℝ (optSet a)) = n. The page prints the index condition of (3.6) as "$i\ne r$"; the formalization uses $i\ne\sigma(r)$, which is what the argument requires. The case $n=0$ is allowed and trivial.

A statement asserting only that $\Omega$ is nonempty, or that it has dimension at least one, is not this theorem: both hold for every cost matrix, the second because $\Omega$ is invariant under adding a constant to all prices. The goal requires the full value $n$, and its hypothesis is uniqueness of the optimal permutation, not of the optimal linear-programming solution.

A complete development needs: the assignment linear program and its integrality (Mathlib's Birkhoff–von Neumann theorem), weak and strong duality between (3.1) and (3.2) or directly $\max w=\min_\sigma c_\sigma$, and a strict complementarity statement for this primal–dual pair; the last two are reusable beyond this mission. Contributions of any of these, and of alternative arguments for (3.5) that avoid strict complementary slackness, are welcome.

Selected references

• M. Held, P. Wolfe, H. P. Crowder, Validation of subgradient optimization, Mathematical Programming 6 (1974) 62–88. https://doi.org/10.1007/BF01580223
• M. Held, R. M. Karp, The traveling-salesman problem and minimum spanning trees: Part II, Mathematical Programming 1 (1971) 6–25. https://doi.org/10.1007/BF01584070
• H. W. Kuhn, The Hungarian method for the assignment problem, Naval Research Logistics Quarterly 2 (1955) 83–97. https://doi.org/10.1002/nav.3800020109
• A. J. Goldman, A. W. Tucker, Theory of linear programming, in H. W. Kuhn, A. W. Tucker (eds.), Linear Inequalities and Related Systems, Annals of Mathematics Studies 38, Princeton University Press, 1956, 53–97.
• Mathlib, Mathlib/Analysis/Convex/Birkhoff.lean (Birkhoff–von Neumann theorem, doublyStochastic_eq_convexHull_permMatrix). https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Analysis/Convex/Birkhoff.lean

Motivation

Integer programs are routinely solved by first solving their linear programming (LP) relaxation and then searching for an integer optimum near the fractional one. How near an integer optimum must be is the subject of proximity theorems. They bound the search region of branch-and-bound and of dynamic programming, and they turn a fractional optimum into a starting point for exact algorithms.

The classical bound is due to Cook, Gerards, Schrijver and Tardos (Math. Programming 34, 1986): for an integer program in inequality form $\max\{c^Tx : Ax\le b,\ x\in\mathbb Z^n\}$ that is feasible and bounded, every optimal LP solution $x^*$ has an optimal integer solution $z^*$ with $\|x^*-z^*\|_\infty\le n\cdot\delta$, where $\delta$ is the largest absolute value of a subdeterminant of $A$. For programs in standard form $Ax=b$ with $m$ rows this gives, via the Hadamard bound, $\|z^*-x^*\|_1\le n^2\cdot m^{m/2}\Delta^m$, which grows with the number of variables $n$.

Eisenbrand and Weismantel (ACM Trans. Algorithms 16(1), Article 5, 2019; conference version SODA 2018) removed the dependence on $n$ altogether, using the Steinitz lemma on rearranging vectors so that all partial sums stay short. Their bound depends only on $m$ and on the largest absolute value $\Delta$ of an entry of $A$, and it is the basis of their faster algorithms for integer programs with few constraints.

Setting

Fix natural numbers $m$ (rows) and $n$ (variables). The data are a matrix $A\in\mathbb Z^{m\times n}$, a right-hand side $b\in\mathbb Z^m$, an objective $c\in\mathbb Z^n$ and upper bounds $u\in\mathbb N^n$. A natural number $\Delta$ bounds the entries: $|a_{ij}|\le\Delta$ for all $i,j$. The integer program (10) is

$$\max\{c^Tx : Ax=b,\ 0\le x\le u,\ x\in\mathbb Z^n\},$$

and its LP relaxation is the same problem over $x\in\mathbb R^n$. Its feasible region $P=\{x\in\mathbb R^n: Ax=b,\ 0\le x\le u\}$ is a polytope, lpPolytope A b u. An optimal vertex solution is an optimal solution of the LP relaxation (IsLPOptimal) that is an extreme point of $P$. An optimal integer solution is IsIPOptimal. Both are maxima.

Distances are measured in the $\ell_1$-norm $\|z-x\|_1=\sum_i|z_i-x_i|$.

A vector $y\in\mathbb Z^n$ is a cycle of $z^*-x^*$ (Eq. (14)) if $Ay=0$ and, for every $i$, $|y_i|\le|(z^*-x^*)_i|$ and $y_i(z^*-x^*)_i\ge0$: an integer kernel vector that is sign-compatible with $z^*-x^*$ and dominated by it (IsCycle).

The Steinitz lemma (Theorem 1.1) concerns vectors $x_1,\dots,x_n$ in an $m$-dimensional normed space with $\sum_i x_i=0$ and $\|x_i\|\le1$. It asserts a permutation $\pi$ with $\|\sum_{j\le k}x_{\pi(j)}\|\le c(m)$ for all $k$, and the paper uses Sevast'anov's constant $c(m)=m$.

Formalization targets

Goal: Theorem 3.3 (p. 5:8)

If (10) has an integer feasible point and $x^*$ is an optimal vertex solution of its LP relaxation, then there is an optimal solution $z^*$ of (10) with

$$\|z^*-x^*\|_1\ \le\ m\cdot(2m\Delta+1)^m .$$

The constant is the paper's. The goal holds for all $m$, $n$, $b$, $c$ and $u$; only $m$ and $\Delta$ enter the bound.

Milestones, in the order the proof uses them

1. Lemma 3.1 (p. 5:8): for an LP optimum $x^*$, an integer optimum $z^*$ and a cycle $y$ of $z^*-x^*$, the vector $z^*-y$ is integer feasible, $x^*+y$ is LP feasible, and $c^Ty\le0$.
2. Lemma 3.2 (p. 5:8): if $z^*$ minimizes $\|z^*-x^*\|_1$ among the optimal integer solutions, then $z^*-x^*$ has no nonzero cycle.
3. Theorem 1.1 with $c(m)=m$ (p. 5:4): the Steinitz lemma in any $m$-dimensional real normed space.
4. Proof of Theorem 3.3 (pp. 5:8–5:9): round a vertex $x^*$ towards an integer vector and write $\{x^*\}$ for the remainder. Then $\|-A\{x^*\}\|_\infty\le\Delta m$ and $-A\{x^*\}=w_1+\dots+w_m$ with integer $w_j$, $\|w_j\|_\infty\le\Delta$.
5. Proof of Theorem 3.3, Eq. (20) (p. 5:9): a sequence of integer vectors of $\ell_\infty$-norm at most $m\Delta$ in which no value repeats $m+1$ times has length at most $m(2m\Delta+1)^m$.
6. Eq. (21) (p. 5:9), a consequence: $c^T(x^*-z^*)\le\|c\|_\infty\cdot m(2m\Delta+1)^m$ for every optimal integer solution $z^*$.

Significance

The bound is independent of the number of variables. Combined with the paper's dynamic program, it gives the paper's running-time results for integer programs with upper bounds: an optimal LP vertex is computed, and the integer optimum is searched for within an $\ell_1$-ball of radius $m(2m\Delta+1)^m$ around it. Eq. (21) bounds the absolute integrality gap by the same quantity, scaled by $\|c\|_\infty$. The Steinitz lemma with constant $m$ is a general tool in discrepancy theory and in scheduling algorithms.

All of these results have published proofs. No machine-checked proof of Theorem 3.3 or of the Steinitz lemma is known to this mission, and Mathlib has no Steinitz lemma. The mission asks for complete Lean proofs of the milestones and of the goal. A proof of the Steinitz lemma with constant $m$ for arbitrary norms is reusable well beyond integer programming.

Difficulty

Lemmas 3.1 and 3.2 and the counting step are elementary. The substance lies in two places. The first is the Steinitz lemma with the linear constant $m$ for an arbitrary norm: the bound must hold uniformly in the number $n$ of vectors, and the constant must be exactly $m$, because the goal's constant $(2m\Delta+1)^m$ counts integer points of $\ell_\infty$-norm at most $m\Delta$. The second is the passage from a vertex to at most $m$ fractional coordinates. The paper argues this in one sentence ("$x^*$ has at most $m$ positive entries"), which is not literally true for (10) with upper bounds: coordinates at their upper bound $u_i>0$ are positive. The correct fact concerns coordinates strictly between $0$ and $u_i$, and it has to be derived from the extreme-point property of $P$.

Formalization scope

• All declarations live in the namespace IPProximity.Eisenbrand. The data are integral: A : Matrix (Fin m) (Fin n) ℤ, b : Fin m → ℤ, c : Fin n → ℤ, u : Fin n → ℕ (entries $u_i=0$ allowed), Δ : ℕ. They are cast to ℝ once, inside the LP definitions. $m=0$ and $n=0$ are allowed.
• "Vertex" is Mathlib's Set.extremePoints ℝ (lpPolytope A b u). It is not defined through bases or by counting fractional coordinates.
• The $\ell_1$-distance is the explicit sum ∑ i, |(z i : ℝ) - x i|. Mathlib's norm on Fin n → ℝ is the sup norm, and it is used only where the paper has $\|\cdot\|_\infty$ (the $\|c\|_\infty$ of Eq. (21)).
• The goal adds one hypothesis the paper leaves implicit: (10) has an integer feasible point. The paper's proof begins with "Let $z^*$ be an optimal integer solution"; without this hypothesis the conclusion is false.
• Eq. (14) is formalized literally, so $y=0$ is a cycle, and Lemma 3.2 is stated for nonzero cycles, which is what its proof establishes. Dropping the vertex hypothesis would make the goal false, so the goal keeps it. The constant is exactly $m(2m\Delta+1)^m$, with no hidden existential constant.
• The Steinitz milestone is stated for any finite-dimensional real normed space of dimension $m$ with the explicit constant $m$. The goal needs only the $\ell_\infty$ case on $\mathbb R^m$.
• Out of scope: the dynamic program and the running-time theorems of Sections 2 and 4, and the refinement $\|z^*-x^*\|_1\le2\Delta$ for $m=1$.

Contributions welcome: proofs of any milestone, in particular the Steinitz lemma, and a proof of the goal from the milestones.

Selected references

• F. Eisenbrand, R. Weismantel, Proximity Results and Faster Algorithms for Integer Programming Using the Steinitz Lemma, ACM Transactions on Algorithms 16(1), Article 5, 2019. https://doi.org/10.1145/3340322
• W. Cook, A. M. H. Gerards, A. Schrijver, É. Tardos, Sensitivity theorems in integer linear programming, Mathematical Programming 34, 251–264, 1986. https://doi.org/10.1007/BF01582230
• E. Steinitz, Bedingt konvergente Reihen und konvexe Systeme, Journal für die reine und angewandte Mathematik 143, 128–176, 1913. https://doi.org/10.1515/crll.1913.143.128
• S. Sevast'janov, Approximate solution of some problems of scheduling theory (in Russian), Metody Diskretnogo Analiza 32, 66–75, 1978 (reference [31] of the paper).
• V. S. Grinberg, S. V. Sevast'yanov, Value of the Steinitz constant, Functional Analysis and Its Applications 14(2), 125–126, 1980 (reference [16] of the paper).

Motivation

The maximum flow problem asks how much of a commodity can be sent from a source to a sink through a network whose arcs have capacities. It underlies bipartite matching, transportation, scheduling and many reductions in combinatorial optimization. The classical method for it, the labeling method of Ford and Fulkerson (Flows in Networks, 1962), repeatedly finds an augmenting path and pushes flow along it. With integer capacities it terminates, but the number of augmentations can be as large as the maximum flow value itself, and Edmonds and Karp exhibit a four-node network on which this happens (p. 250). With irrational capacities the method need not terminate at all.

Edmonds and Karp, Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems, J. ACM 19(2):248–264, 1972 (doi:10.1145/321694.321699), showed that two simple rules for choosing the augmenting path repair this. The first, augmenting along a path with fewest arcs, is the subject of mission 1 of this series. This mission covers the second (§1.3): augment along a path that gives the largest possible augmentation. For integer capacities the number of augmentations then grows only logarithmically in the maximum flow value.

Setting

A network $N$ has a finite set $V$ of nodes, a source $s$ and a sink $t \neq s$, and a set of arcs, ordered pairs $(u,v)$ with $u \neq v$, at most one from each node to another. One arc is the return arc $(t,s)$; the other arcs form the set $A$, and each $(u,v) \in A$ has a capacity $c(u,v) > 0$. A flow is a nonnegative function $f$ on the arcs of $N$ with $f(u,v) \le c(u,v)$ on $A$ and flow conservation at every node, $s$ and $t$ included. Its value is $f(t,s)$, the flow returned along the return arc; a maximum flow has the largest value among all flows, and $f^*(t,s)$ denotes that value.

The residual network $N^f$ has an arc $(u,v)$ whenever $(u,v) \in A$ and $c(u,v) - f(u,v) > 0$, or $(v,u) \in A$ and $f(v,u) > 0$. An augmenting path is a directed path $s = u_1, \dots, u_p = t$ of distinct nodes in $N^f$. Each of its arcs $(u,v)$ has a residual amount $e(u,v)$, equal to $c(u,v) - f(u,v)$, $f(v,u)$, or $c(u,v) - f(u,v) + f(v,u)$ according to which of $(u,v)$, $(v,u)$ lie in $A$, and the path's augmentation is $\varepsilon = \min e(u_i, u_{i+1})$. Augmenting increases $f(t,s)$ by $\varepsilon$ and changes the flow on the arcs of the path accordingly, with the paper's own rule when both $(u,v)$ and $(v,u)$ are arcs. The labeling method produces flows $f^0, f^1, \dots$ by augmenting along a path relative to $f^k$ as long as one exists.

The rule studied here chooses, at every step, an augmenting path whose $\varepsilon$ is at least that of every other augmenting path relative to the current flow. The bound involves an integer $M > 1$ such that every partition of the nodes into $X \ni s$ and $\bar X \ni t$ has at most $M$ arcs of $N$ with one end on each side.

Formalization targets

Goal: Theorem 2 (p. 253)

For a network with integer capacities, $M$ as above, and a run $f^0, \dots, f^K$ of the labeling method with maximum augmentations started from an integer-valued flow,

$$K \;\le\; 1 + \log_{M/(M-1)} f^*(t,s),$$

and if no augmenting path relative to $f^K$ exists, then $f^K$ is a maximum flow.

Milestones

The milestone list follows the paper's argument:

1. augmentation produces a flow of value $f(t,s) + \varepsilon$ (§1.1, p. 249);
2. a flow is maximum if and only if it has no augmenting path (§1.1, pp. 249–250);
3. with integer capacities, $\varepsilon$ is a positive integer and the flows of the method stay integer-valued (§1.1, p. 250);
4. the cut inequality $c(X,\bar X) \ge f(X,\bar X) - f(\bar X,X) = f(t,s)$ (p. 254);
5. $f^*(t,s) - f^k(t,s) \le \varepsilon^k M$, where $\varepsilon^k = f^{k+1}(t,s) - f^k(t,s)$ (p. 254);
6. $f^*(t,s) - f^{k+1}(t,s) \le [f^*(t,s) - f^k(t,s)](1 - M^{-1})$ (p. 254);
7. $f^*(t,s) - f^k(t,s) \le f^*(t,s)(1 - M^{-1})^k$ (p. 254).

Significance

Theorem 2 was among the first bounds showing that a maximum flow algorithm can be made polynomial in the size of the numbers rather than in their values: since $M \le n^2/2$ and $f^*(t,s)$ is at most $n^2$ times the average capacity, the bound is $O(n^2 \log(n^2 \bar c))$ in terms of the number of nodes $n$ and the average capacity $\bar c$ (p. 254). The largest-augmentation rule, often called the fattest-path or maximum-capacity augmenting path rule, is a standard textbook variant, and its geometric-decrease argument is the model for later capacity-scaling methods, including the scaling algorithm for the Hitchcock problem in §2 of the same paper (mission 3 of this series).

The theorem has been proved since 1972 and appears in standard texts. As far as a platform search shows (2026-09-26), no machine-checked proof of it exists on Prove2Me. The platform does contain LinearOptimization.max_flow_min_cut and LinearOptimization.max_flow_ford_fulkerson_integer_termination, which state max-flow min-cut and termination of the generic method in a different network model (parallel arcs, extended nonnegative capacities, no return arc); they give no count of augmentations and are related work only. This mission would contribute a formal proof of the counting bound together with the general labeling-method facts (milestones 1–3), which mission 1 needs as well.

Difficulty

The obvious argument, that each augmentation raises the value by at least 1, gives only the bound $f^*(t,s)$, and on the four-node example of p. 250 that bound is attained by an arbitrary choice of paths. The logarithmic bound needs a lower bound on the size of the largest augmentation in terms of the remaining gap $f^*(t,s) - f^k(t,s)$. The largest augmentation is defined by comparison with all augmenting paths relative to the current flow, while the gap is a global quantity of the network, and neither integrality nor the maximum-augmentation rule alone controls it. Milestone 2's converse, that a non-maximum flow always admits an augmenting path, is itself the max-flow min-cut theorem in this model, and the formal proof has to establish it for the paper's return-arc model rather than import it from a different one.

Formalization scope

• Nodes form a finite type V with decidable equality. A : Finset (V × V) contains no loops and not $(t,s)$. Capacities are real, c : V → V → ℝ, positive on A. Integrality is the hypothesis IntegralCaps N, and for the initial flow IsIntegralOn N (f 0) (integer values on the arcs of $N$, the return arc included).
• Flows are functions V → V → ℝ constrained only on the arcs of $N$. A maximum flow is the predicate IsMaxFlow, comparing $f(t,s)$ with every flow, not a supremum. The goal takes a maximum flow g as a hypothesis and sets $f^*(t,s) = g(t,s)$; every network has one.
• Augmenting paths are duplicate-free node lists whose consecutive pairs are arcs of $N^f$. The page prints Case (b) of the definition of $\varepsilon_i$ with the same hypothesis as Case (c); the corrected Case (b), $(u,v) \notin A$ and $(v,u) \in A$, is used, as the definition of $N^f$ (p. 251) and the list for $e(u,v)$ (p. 253) confirm.
• A run is IsMaxAugRun N K f P. Its initial flow is arbitrary except for integrality, and each later flow is the augmentation of the previous one along a path of maximum $\varepsilon$ among all augmenting paths.
• The crossing bound CrossArcsBounded N M counts the arcs of $N$, return arc included, with one end on each side of every $s$–$t$ partition. This is the literal reading of p. 253.
• Explicit constants. The bound is exactly $1 + \log_{M/(M-1)} f^*(t,s)$, written (K : ℝ) ≤ 1 + Real.logb ((M : ℝ) / ((M : ℝ) - 1)) (g N.t N.s) with $M > 1$ a natural number. When $f^*(t,s) = 0$, Real.logb gives $0$ and the bound reads $K \le 1$. The contraction factor is 1 - (M : ℝ)⁻¹.
• A statement that bounds only runs of an unsatisfiable step predicate, drops the integrality of $f^0$ or of the capacities (the bound is false without them), or compares $\varepsilon$ only among paths of some restricted class does not formalize Theorem 2. A sorry-free check exhibits a four-node network with integer capacities and a valid maximum-augmentation step.
• Reusable beyond this mission: the return-arc network model, the augmentation step with the paper's opposite-arc rule, the integrality lemma, and the cut inequality. Proofs of any milestone are welcome, as are proofs of the converse in milestone 2 that could later be shared with mission 1.

Selected references

• J. Edmonds, R. M. Karp, Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems, Journal of the ACM 19(2):248–264, 1972. https://doi.org/10.1145/321694.321699
• L. R. Ford, D. R. Fulkerson, Flows in Networks, RAND report R-375-PR, 1962; Princeton University Press, 1962. https://www.rand.org/pubs/reports/R375.html

Motivation

The Steiner problem in graphs asks for the cheapest way to connect a prescribed set of nodes of a network, where intermediate nodes may be used freely. It is the network version of the classical Euclidean Steiner tree problem surveyed by Gilbert and Pollak (SIAM J. Appl. Math. 16, 1968), and it arises wherever a few sites must be joined through an existing network at minimum total cost: communication and pipeline layout, VLSI routing, and phylogenetics. With two terminals it is the shortest-path problem; with all nodes as terminals it is the minimum spanning tree problem; in between it is NP-hard.

Dreyfus and Wagner (Networks 1(3):195–207, 1971) gave the first exact algorithm whose running time is exponential only in the number $k$ of terminals and polynomial in the number $n$ of nodes. The paper states it, as Algorithm A, together with its proof of correctness and an exact count of its elementary operations.

Timeline. 1968: Gilbert and Pollak survey Steiner minimal trees. 1971: Dreyfus and Wagner, a dynamic program over subsets of terminals running in time proportional to $n^3/2 + n^2(2^{k-1}-k-1) + n(3^{k-1}-2^k+3)/2$. 1987: Erickson, Monma and Veinott give the same subset recursion for general network flow problems. 2007: Björklund, Husfeldt, Kaski and Koivisto (STOC 2007) improve the exponential dependence on $k$ for small integer weights. The Dreyfus–Wagner recursion remains the standard exact method and the basis of the fixed-parameter tractability of the problem in $k$.

Setting

A graph $G = (N, A)$ has a finite set $N$ of nodes and a set $A$ of undirected arcs, each arc $a$ having a positive length $|a|$; $G$ is connected. For a set $S \subseteq A$ of arcs, $|S| = \sum_{s \in S} |s|$. A set $S$ connects a node set $X$ if all members of $X$ are joined by paths composed only of arcs in $S$.

Given $Y \subseteq N$, a Steiner path (or Steiner tree) connecting $Y$ is a set $S \subseteq A$ that connects $Y$ with $|S|$ minimum. Its length is the Steiner length $\operatorname{St}(Y)$. For nodes $i, j$, $D(i,j)$ is the length of a shortest path from $i$ to $j$; $D(i,j) = \operatorname{St}(\{i,j\})$.

Algorithm A fixes a linear order of $N$ (so that each nonempty set $D$ has a first element $D[1]$), picks $q \in Y$, sets $C = Y - \{q\}$, and fills a table $S[D, I]$ for nonempty $D \subsetneq C$ and $I \in N$:

$$S[\{t\}, I] = D(t, I), \qquad S[D, I] = \min_{J \in N}\Big(D(I,J) + \min_{D[1] \in E \subsetneq D}\big(S[E,J] + S[D-E,J]\big)\Big),$$

and returns

$$v = \min_{J \in N}\Big(D(q,J) + \min_{C[1] \in E \subsetneq C}\big(S[E,J] + S[C-E,J]\big)\Big).$$

A minimum over an empty set is $+\infty$. In the Lean development these objects are steinerLength, pathDist, tableA and algorithmA in the namespace DreyfusWagner.Steiner.

Formalization targets

Goal: Algorithm A is exact

For every finite connected graph with positive arc lengths, every linear order on its nodes, every $Y$ with $\|Y\| \ge 3$ and every $q \in Y$,

$$v = \operatorname{St}(Y).$$

This is the caption of Algorithm A ("Computes the length of the Steiner tree connecting $Y$", p. 203). The statement is an equality, not a bound.

Milestones

In the order the proof uses them:

1. A Steiner path is a tree (§1, p. 197): a minimum connecting arc set contains no cycle.
2. The two-node case (Appendix A, p. 205): $\operatorname{St}(\{i,j\}) = D(i,j)$.
3. Theorem 1 (Appendix A, p. 206): for a Steiner tree $S$, a node $x$ on it, and a set $C$ of arcs of $S$ at $x$, the arcs of $S$ connecting $x$ to the terminals reached through $C$ form a Steiner tree for those terminals together with $x$.
4. Optimal Decomposition Theorem (Appendix A, p. 206): if $\|Y\| \ge 3$ and $q \in Y$, a Steiner tree for $Y$ splits into three disjoint Steiner paths, for $\{p,q\}$, $\{p\} \cup D$ and $\{p\} \cup (Y - D - \{q\})$, where $p \in N$ and $\emptyset \ne D \subsetneq Y - \{q\}$.
5. The recurrence (§2, pp. 199–200): for $\|D\| \ge 2$ and any node $m$,

$$\operatorname{St}(\{m\} \cup D) = \min_{k \in N}\Big(D(m,k) + \min_{\emptyset \ne E \subsetneq D}\big(\operatorname{St}(\{k\} \cup E) + \operatorname{St}(\{k\} \cup (D - E))\big)\Big).$$

6. The table invariant (§2, p. 200): $S[D, I] = \operatorname{St}(\{I\} \cup D)$ for every nonempty $D$ and every $I$.

Two companion items accompany the goal: the numerical illustration of §3 (seven nodes, $\operatorname{St}(Y) = 5$, Algorithm A returns $5$), and the exact count of elementary statements of §5, $n^2(2^{k-1}-k-1) + n(3^{k-1}-2^k+3)/2$.

Significance

The result turns the Steiner problem with few terminals into a polynomial computation in the size of the network: for fixed $k$ the running time is $O(n^3)$ including all-pairs shortest paths. It is the reference exact algorithm against which heuristics and approximation algorithms for Steiner trees are evaluated, a standard example of dynamic programming over subsets, and the origin of the fixed-parameter tractability of the Steiner tree problem parameterized by the number of terminals. The subset recurrence reappears in group Steiner, prize-collecting and directed Steiner variants.

The paper's proof is complete and the result is classical; it has not, to our knowledge, been machine-checked. This mission produces a checked account of the exactness of the recursion: the structural facts about minimum connecting arc sets (acyclicity, optimality of branches, the three-way decomposition) and the passage from these to the algorithm's table. These facts about weighted graphs, minimum connecting arc sets and shortest paths are reusable well beyond this paper.

Difficulty

The upper bound $v \ge \operatorname{St}(Y)$ is routine: each term of each minimum is the length of some connecting arc set, so no term can beat the optimum. The content is the reverse inequality, which needs the Optimal Decomposition Theorem: one must show that some optimal tree actually splits at a single node $p$ into a shortest path to $q$ and two optimal subtrees whose terminal sets partition $Y - \{q\}$ into two nonempty parts. The naive choice $p = q$ fails when $q$ is a leaf, and the choice of the first branching node fails when the path from $q$ meets another terminal first; the paper handles these as separate cases. A second difficulty is the passage from arc sets to trees: minimum connecting sets are forests only because lengths are positive, and "the arcs of $S$ involved in connecting" a set of terminals must be identified with a subtree. Finally the table recursion must be matched with the recurrence, including the restriction $D[1] \in E$ that enumerates each splitting once.

Formalization scope

Nodes are a finite type V with a LinearOrder (the paper's "(ordered) set"; the goal holds for every order). The graph is a SimpleGraph V with decidable adjacency, arcs are unordered pairs Sym2 V, and lengths are ℓ : Sym2 V → ℝ. Every theorem assumes the paper's standing hypotheses of p. 195: all arcs of $G$ have positive length (∀ e ∈ G.edgeSet, 0 < ℓ e) and $G$ is connected. The paper allows several arcs between the same two nodes; the simple-graph model keeps one, which does not change any Steiner length since an optimal set uses only the shortest of parallel arcs. Connecting means reachability in the graph formed by the arcs of $S$. Steiner lengths, $D(i,j)$ and all minima of the algorithm take values in WithTop ℝ, where ⊤ is $+\infty$, ⊤ + x = ⊤ and an empty minimum is ⊤; no real-valued infimum with a junk value is used. $D(i,j)$ is a minimum over paths of $G$.

The goal assumes $\|Y\| \ge 3$, the paper's own hypothesis (Appendix A, p. 205). For $\|Y\| = 2$ Algorithm A as printed returns $+\infty$ because line (18) admits no set $E$; the two-node case is covered by milestone 2. The algorithm is defined from $D(i,j)$, addition and minima only: a formalization in which tableA or algorithmA refers to Steiner lengths, or in which the goal only asserts $v \ge \operatorname{St}(Y)$, would be trivial and is ruled out. The loop order of lines (4)–(14) is replaced by recursion on $\|D\|$, which the paper states is immaterial (p. 203).

Useful infrastructure: sums of lengths along walks and paths, reachability in edge-subgraphs, acyclicity of minimum connecting sets, and splitting a tree at a node. Contributions of these as reusable lemmas are welcome, as are proofs of individual milestones in any order. Tree reconstruction (§2, p. 200) and the empirical running times (p. 205) are out of scope.

Selected references

• S. E. Dreyfus, R. A. Wagner, The Steiner Problem in Graphs, Networks 1(3):195–207, 1971. https://doi.org/10.1002/net.3230010302
• E. N. Gilbert, H. O. Pollak, Steiner Minimal Trees, SIAM Journal on Applied Mathematics 16(1):1–29, 1968. https://doi.org/10.1137/0116001
• R. W. Floyd, Algorithm 97: Shortest Path, Communications of the ACM 5(6):345, 1962. https://doi.org/10.1145/367766.368168
• R. E. Erickson, C. L. Monma, A. F. Veinott Jr., Send-and-Split Method for Minimum-Concave-Cost Network Flows, Mathematics of Operations Research 12(4):634–664, 1987. https://doi.org/10.1287/moor.12.4.634
• A. Björklund, T. Husfeldt, P. Kaski, M. Koivisto, Fourier Meets Möbius: Fast Subset Convolution, STOC 2007, 67–74. https://doi.org/10.1145/1250790.1250801

Motivation

Maximizing a submodular set function without constraints contains Max Cut, Max Directed Cut, maximum facility location and several graph and hypergraph cut problems as special cases, and it appears in operations research wherever a value exhibits diminishing returns but is not monotone (profit that combines coverage with a cost, for example). These problems are NP-hard, so the question is which fraction of the optimum an efficient algorithm can guarantee when the function is accessible only through a value 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 approximation algorithms for maximizing a general nonnegative submodular function. The simplest of them returns a uniformly random set and achieves $1/4$ of the optimum; this mission is about the next one, a nonadaptive algorithm: it decides all of its oracle queries before seeing any answer, then computes a set from the answers. Such an algorithm can be run in one round of parallel queries. The paper shows that this restricted access already beats $1/4$ and reaches $1/3$.

Timeline. For Max Directed Cut, a random cut achieves $1/4$. Feige, Mirrokni and Vondrák (FOCS 2007; journal version 2011) proved $1/4$ for a random set and $1/3$ nonadaptively for general nonnegative submodular functions, $1/3$ and $2/5$ by adaptive local search, and that $1/2$ requires exponentially many queries. Buchbinder, Feldman, Naor and Schwartz (FOCS 2012, SIAM J. Comput. 2015) later reached the optimal $1/2$ with a randomized double-greedy algorithm.

Setting

Let $X$ be a finite ground set with $n = |X| \ge 1$ elements. A function $f : 2^X \to \mathbb{R}$ is submodular (Definition 1.1) if

$$f(S \cup T) + f(S \cap T) \le f(S) + f(T) \qquad \text{for all } S, T \subseteq X .$$

Throughout, $f$ is nonnegative, the paper's standing assumption, and $OPT = \max_{S \subseteq X} f(S)$.

For $p \in [0,1]$, $X(p)$ denotes the random subset of $X$ containing each element independently with probability $p$; $R = X(1/2)$ is a uniformly random subset. For a set $A \subseteq X$, $A(p)$ is the analogous random subset of $A$. The averaged marginal value of an element (Definition 2.4) is

$$\omega(x) = \mathbf{E}\big[f(R \cup \{x\}) - f(R \setminus \{x\})\big], \qquad R = X(1/2).$$

Algorithm NA (p. 1139):

1. by random sampling, compute estimates $\tilde\omega(x)$ with $|\tilde\omega(x) - \omega(x)| < OPT/n^2$ for all $x$, with high probability;
2. independently, sample $R = X(1/2)$;
3. with probability $8/9$ return $R$;
4. with probability $1/9$ return $A = \{x \in X : \tilde\omega(x) > 0\}$.

Given the estimates, the expected value NA returns is $\tfrac89\,\mathbf{E}[f(X(1/2))] + \tfrac19 f(A)$.

Formalization targets

Goal: Theorem 2.6 in the explicit form of its proof

For every nonnegative submodular $f$ and every estimate $\tilde\omega$ with $|\tilde\omega(x) - \omega(x)| < OPT/n^2$ for all $x$,

$$\frac89\,\mathbf{E}[f(X(1/2))] + \frac19\, f\big(\{x : \tilde\omega(x) > 0\}\big) \ \ge\ \Big(\frac13 - \frac{4}{9n}\Big)\, OPT .$$

The printed theorem says "at least $(1/3 - o(1))\,OPT$"; the term $4/(9n)$ is what the proof establishes (p. 1140, last display).

Milestones

1. Lemma 2.2: $\mathbf{E}[g(A(p))] \ge (1-p)\,g(\emptyset) + p\,g(A)$ for submodular $g$.
2. Lemma 2.3: $\mathbf{E}[f(A(p) \cup B(q))] \ge (1-p)(1-q) f(\emptyset) + p(1-q) f(A) + (1-p)q f(B) + pq f(A \cup B)$ for independently sampled, possibly overlapping $A, B$.
3. For $B = X \setminus A$ and any $C$: $f(A) + f(B \cap C) + f(B \cup C) \ge f(C)$.
4. If $\omega \le OPT/n^2$ on $B$: $\mathbf{E}[f(R \cup (B \cap C))] \le \mathbf{E}[f(R)] + OPT/(2n)$.
5. $\mathbf{E}[f(R \cup (B \cap C))] \ge \tfrac14 f(B \cap C) + \tfrac14 f(C)$.
6. If $\omega \ge -OPT/n^2$ on $A$ and $B = X \setminus A$: $\mathbf{E}[f(R)] \ge \mathbf{E}[f(R \cap (B \cup C))] - OPT/(2n)$.
7. $\mathbf{E}[f(R \cap (B \cup C))] \ge \tfrac14 f(C) + \tfrac14 f(B \cup C)$.

Milestones 3–7 are the displayed steps of the proof of Theorem 2.6, stated for arbitrary sets where the page's argument does not use the optimality of $C$.

Significance

The theorem shows that nonadaptive access, a fixed batch of polynomially many value queries followed by a computation, suffices for a $1/3$-approximation of unconstrained nonnegative submodular maximization, strictly better than the $1/4$ of any algorithm that must return one of its queried sets (the paper shows $1/4$ is optimal in that class, §4.2). The quantity $\omega$ generalizes the in-degree/out-degree test for Max Directed Cut to arbitrary submodular functions, and Lemmas 2.2 and 2.3 are general sampling inequalities for submodular functions that the paper reuses for its adaptive smooth local search.

Formalizing it produces machine-checked versions of Lemmas 2.2 and 2.3 as statements about exact finite averages, a reusable expectation operator on product-distributed random subsets, and a checked version of the $1/3$ argument with its explicit error term. The result is proved in the paper; to our knowledge none of it has been formalized in a proof assistant.

Difficulty

The two regimes the proof separates, "$A$ is already good" and "one of $f(B \cap C)$, $f(B \cup C)$ is large", must be tied to the value of a uniformly random set, whereas the elements of $A$ and $B$ are chosen from estimated averages, not from the optimal set $C$. The natural attempt, comparing $f(R)$ with $f(C)$ element by element, fails because $f$ is not monotone: adding elements of $C$ to $R$ can decrease the value. The accuracy $OPT/n^2$ of the estimates must also be propagated through a sum over up to $n$ elements, which is where the error term $4/(9n)$ comes from. The sampling lemmas require handling expectations over pairs of independent random subsets of possibly overlapping sets.

Formalization scope

• The ground set is a Fintype X with DecidableEq, assumed Nonempty, so $n = |X| \ge 1$ and the divisions by $n$ and $n^2$ are genuine; sets are Finset X; $f$ is real valued with nonnegativity $\forall S,\ 0 \le f(S)$ as an explicit hypothesis. Lemmas 2.2 and 2.3 are stated for real $f$ with no sign condition, as printed.
• $OPT$ is Finset.univ.sup' _ f, the true maximum over all subsets.
• Every expectation over an independently sampled random set is the exact finite sum $F(x) = \sum_{S} f(S)\prod_{i \in S} x_i \prod_{i \notin S}(1 - x_i)$; $X(1/2)$ is $x \equiv 1/2$. Expectations over two independent samples (Lemma 2.3) are the corresponding iterated sums. Sampling probabilities carry the hypotheses $0 \le p, q \le 1$.
• The goal quantifies over every estimate $\tilde\omega$ satisfying the printed accuracy $|\tilde\omega(x) - \omega(x)| < OPT/n^2$ (strict), with $A = \{x : \tilde\omega(x) > 0\}$ (strict). The "with high probability" of NA's first step is this hypothesis; the sampling estimate that makes it likely (Lemma 2.5, a Chernoff-bound argument) is not part of the goal. When $OPT = 0$ the hypothesis is unsatisfiable, but then $f \equiv 0$ and nothing is lost.
• The left-hand side is exactly the mixture $\tfrac89\,\mathbf{E}[f(X(1/2))] + \tfrac19 f(A)$. A statement with the maximum of the two terms, with exact values $\tilde\omega = \omega$, or with the $o(1)$ replaced by an existential constant or a limit, is a different (and weaker or stronger) theorem and does not close this mission.
• Printed slip corrected: in the second display on p. 1140, the "$=$" before $-|A \setminus C|\,OPT/(2n^2)$ should be "$\ge$"; milestone 6 states the inequality.

Welcome contributions: proofs of Lemmas 2.2 and 2.3 (reusable for mission IV of this series), the identity $\mathbf{E}[f(R \cup \{x\}) - f(R)] = \tfrac12\omega(x)$, and general lemmas about the operator $F$ (splitting a uniform random set along a partition).

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. 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

Connecting a set of terminals by a network of direct links of least total length is one of the oldest problems of combinatorial optimization. R. C. Prim's 1957 paper in the Bell System Technical Journal (DOI) was motivated by the rate structure for Bell System leased-line services, in which the charge for connecting a set of terminals depends on the length of a shortest network connecting them. The paper states two local construction principles, P1 and P2, and shows that any sequence of their applications produces a shortest network, first for points in the plane and then for arbitrary connected labelled graphs with arbitrary real edge lengths. The paper's §V specialization of the principles, growing a single fragment, is what is now called Prim's algorithm, and its §IV statement is the form of the minimum spanning tree theorem used throughout network design, clustering and approximation algorithms.

Timeline. O. Borůvka (1926) solved the problem for an electrical network in Moravia; V. Jarník (1930) gave the single-fragment procedure; J. B. Kruskal (1956, Proc. AMS 7, 48–50) proved that adding globally shortest links avoiding cycles yields a shortest spanning tree; Prim (1957) gave the more permissive principles P1 and P2, which contain both the Jarník procedure and Kruskal's rule as special orders of application; E. W. Dijkstra (1959) rediscovered the single-fragment procedure.

Setting

Let $V$ be a finite set of $N$ terminals and $G$ a simple graph on $V$, the labelled graph whose edges are the possible links. Each edge $e$ carries a real length $w(e)$; lengths may be negative, zero, or tie. For a finite set $F$ of links, $H(F)$ denotes the graph on $V$ whose edges are the links of $F$.

• A spanning subtree of $G$ is a set $F$ of edges of $G$ such that $H(F)$ is a tree on $V$. Its length is $\ell_w(F) = \sum_{e \in F} w(e)$.
• A shortest spanning subtree (SSS) is a spanning subtree of least length among all spanning subtrees of $G$. Prim's dictionary is "shortest connection network (SCN) ↔ shortest spanning subtree (SSS)". $L(G,w)$ denotes that least length.
• Given the links $F$ made so far, the connected components of $H(F)$ are the isolated terminals (one terminal) and isolated fragments (two or more terminals).
• Principle 1: any isolated terminal $t$ can be connected to a nearest neighbor, a $G$-neighbor $n$ with $w(\{t,n\}) \le w(\{t,m\})$ for all $G$-neighbors $m$ of $t$.
• Principle 2: any isolated fragment $C$ can be connected to a nearest neighbor $n \notin C$ by a shortest available link $\{u,n\}$, $u \in C$; equivalently $\{u,n\}$ is a shortest edge of $G$ with one end in $C$ and the other outside.
• A construction is a sequence of links $e_0, e_1, \dots$, each an application of P1 or P2 with respect to the links before it. It is complete when it has $N-1$ links.

Only edges of $G$ are possible links; in Prim's distance table a missing edge has length $\infty$.

Formalization targets

Goal (§IV, p. 1396)

For every finite connected graph $G$ and every $w$,

$$\Bigl(\exists\ \text{a complete construction}\Bigr) \ \wedge\ \Bigl(\forall\ \text{complete constructions } e_0,\dots,e_{N-2}:\ \{e_0,\dots,e_{N-2}\} \text{ is a SSS of } G\Bigr).$$

This is the sentence "P1 and P2 will provide a SSS for any connected labelled graph with any set of real edge lengths." It fixes nothing about the order of applications, the component chosen, or the tie-breaking.

Milestones

1. Counting (§II, p. 1392): after any construction with $k$ links, $H(F)$ is acyclic with $N-k$ components; a complete construction is a spanning subtree; a construction with fewer than $N-1$ links can be extended.
2. Necessary Condition 1 (p. 1392): every terminal of a SSS is linked in it to at least one nearest neighbor.
3. Necessary Condition 2 (p. 1392): every fragment $S$ of a SSS, $\emptyset \ne S \ne V$, is linked in it to a nearest neighbor by a shortest available link.
4. Distinct lengths (§III, p. 1393): if the edge lengths are pairwise distinct, every link of every construction belongs to every SSS.
5. Continuity (§III, p. 1394): $w \mapsto L(G,w)$ is continuous.

Significance

The goal is the correctness theorem of a whole family of greedy minimum spanning tree procedures at once: Jarník–Prim (one growing fragment), Kruskal (globally shortest link first) and Borůvka-style interleavings all produce sequences of P1/P2 applications. Because lengths are arbitrary reals, it also covers maximum spanning trees by a sign change (p. 1397) and graphs that are not complete.

The result is classical and fully proved in the literature. What this mission adds is a machine-checked statement in exactly Prim's generality. Mathlib has spanning trees of connected graphs (SimpleGraph.Connected.exists_isTree_le) and the edge count of trees, but no minimum spanning tree theory. Existing Prove2Me items on minimum spanning trees are either restricted to complete graphs with distance matrices or state a cut property in existence form at a single vertex; none states Prim's principles or his necessary conditions.

Difficulty

The obvious argument, "each link P1 or P2 adds belongs to the shortest network", uses a unique shortest network, and that fails with ties: when two links tie, a P1/P2 link need not lie in a given SSS. Prim's own treatment of ties (§III) is an informal perturbation argument; the formal statement must hold for every tie-breaking choice made during a construction, not only for a generic perturbed instance. Negative lengths remove the easy reading "shortest connected spanning subgraph": the minimum must range over trees only. The statements also involve the component structure of $H(F)$ as it changes during a construction, and tree paths in an arbitrary, not necessarily complete, graph.

Formalization scope

Namespace ShortestConnection.Principles, Mathlib SimpleGraph. Conventions:

• $V$ is a Fintype with decidable equality; $G$ is a SimpleGraph V (at most one link per pair, no loops, which is Prim's setting). Lengths are w : Sym2 V → ℝ; only values on edges of $G$ matter.
• Link sets are Finset (Sym2 V); linkGraph F is SimpleGraph.fromEdgeSet F. A spanning subtree requires ↑F ⊆ G.edgeSet and (linkGraph F).IsTree.
• An isolated fragment is a whole connected component of linkGraph F; the P2 condition is a single inequality against every $G$-edge leaving it, which is equivalent to "nearest neighbor and shortest link" in Prim's sense.
• A construction is a List (Sym2 V) checked entrywise against l.take i; complete means length Fintype.card V - 1 (natural subtraction, used only for nonempty $V$).
• $L$ is sInf of the lengths of spanning subtrees; continuity is in the product topology.

Implicit hypotheses made explicit: $G$ connected (hence $V \ne \emptyset$) wherever an SSS or a complete construction is involved; at least two terminals for Necessary Condition 1; $S$ nonempty and $S \ne V$ for Necessary Condition 2; pairwise distinct edge lengths only in milestone 4, as in the paper's temporary assumption.

The goal's existence clause rules out a vacuous formalization in which no complete construction exists; the step predicates are defined from lengths and components only, never through shortest spanning subtrees, and they are not restricted to one growing fragment or to the globally shortest link.

Needed infrastructure: tree exchange (adding an edge to a spanning tree creates one cycle; removing any other cycle edge yields a spanning tree), component counts under edge addition, and minima of finitely many continuous functions. The exchange and counting lemmas are reusable for any matroid-greedy or spanning-tree mission. Contributions of intermediate lemmas, and proofs of the milestones in any order, are welcome.

Selected references

• R. C. Prim, Shortest Connection Networks And Some Generalizations, Bell System Technical Journal 36 (1957), 1389–1401. https://doi.org/10.1002/j.1538-7305.1957.tb01515.x
• J. B. Kruskal, On the shortest spanning subtree of a graph and the traveling salesman problem, Proceedings of the AMS 7 (1956), 48–50. https://doi.org/10.1090/S0002-9939-1956-0078686-7
• V. Jarník, O jistém problému minimálním, Práce Moravské Přírodovědecké Společnosti 6 (1930), 57–63.
• O. Borůvka, O jistém problému minimálním, Práce Moravské Přírodovědecké Společnosti 3 (1926), 37–58.
• R. L. Graham, P. Hell, On the history of the minimum spanning tree problem, Annals of the History of Computing 7 (1985), 43–57. https://doi.org/10.1109/MAHC.1985.10011

Motivation

Many combinatorial optimization problems ask for a subset of a finite ground set that maximizes a set function with diminishing returns: Max Cut and Max Directed Cut in graphs, facility location, maximum entropy sampling, and welfare problems in combinatorial auctions all fit this pattern. The common abstraction is the maximization of a submodular function, the discrete analogue of a concave function. Unlike the monotone case, where the objective only grows as elements are added, the non-monotone problem has no constraint at all and is still NP-hard, since Max Cut is a special case.

For Max Cut and Max Directed Cut, the simplest algorithm there is, putting every vertex on a side by an independent fair coin, already cuts half, respectively a quarter, of the optimum in expectation. Feige, Mirrokni and Vondrák (SIAM J. Comput. 40(4), 2011; extended abstract at FOCS 2007) showed that this is not a feature of cut functions: the same random choice achieves the same factors for every nonnegative submodular function, and for every symmetric one. This mission formalizes that result, Theorem 2.1 of the paper, together with the two sampling lemmas on which it rests. The paper's other results (a nonadaptive 1/3-approximation, deterministic and smoothed local search, and query lower bounds) are the subjects of companion missions in the same series.

Setting

Let $X$ be a finite set with $n = |X|$ elements. A set function assigns a real number $f(S)$ to every subset $S \subseteq X$. It is submodular if

$$f(S \cup T) + f(S \cap T) \le f(S) + f(T) \qquad \text{for all } S, T \subseteq X,$$

equivalently if the marginal value $f(B \cup \{x\}) - f(B)$ of an element $x$ does not increase as the set $B$ grows. It is symmetric if $f(X \setminus S) = f(S)$ for every $S \subseteq X$; the cut function of an undirected graph is the standard example. The optimum is

$$OPT = \max_{S \subseteq X} f(S).$$

For $p \in [0,1]$, $X(p)$ denotes the random subset of $X$ containing each element independently with probability $p$; similarly $A(p)$ is the random subset of a fixed $A \subseteq X$. The Random Set Algorithm (RS) returns $R = X(1/2)$, a uniformly random subset of $X$, without querying $f$. Its expected value is the average of $f$ over all subsets,

$$\mathbf{E}[f(R)] = F(\tfrac12, \dots, \tfrac12) = \frac{1}{2^n} \sum_{S \subseteq X} f(S),$$

where $F(x) = \sum_{S \subseteq X} f(S) \prod_{i \in S} x_i \prod_{i \notin S} (1 - x_i)$ is the multilinear extension of $f$, the expectation of $f$ on a random set that includes element $i$ independently with probability $x_i$.

Formalization targets

Goal: Theorem 2.1

For every nonnegative submodular $f : 2^X \to \mathbb{R}_+$,

$$\mathbf{E}[f(X(1/2))] \ge \tfrac14\, OPT,$$

and if $f$ is in addition symmetric,

$$\mathbf{E}[f(X(1/2))] \ge \tfrac12\, OPT.$$

Both parts form the goal, stated as one theorem. The constants $\tfrac14$ and $\tfrac12$ are exact, not asymptotic, and they are tight: the directed cut of a single arc attains $\tfrac14$, and the cut of a single edge attains $\tfrac12$.

Milestones

1. Lemma 2.2. For submodular $g : 2^X \to \mathbb{R}$, $A \subseteq X$ and $p \in [0,1]$,

$$\mathbf{E}[g(A(p))] \ge (1-p)\, g(\emptyset) + p\, g(A).$$

2. Lemma 2.3. For submodular $f : 2^X \to \mathbb{R}$, sets $A, B \subseteq X$ that need not be disjoint, independent samples $A(p)$, $B(q)$, and $p, q \in [0,1]$,

$$\mathbf{E}[f(A(p) \cup B(q))] \ge (1-p)(1-q) f(\emptyset) + p(1-q) f(A) + (1-p)q f(B) + pq f(A \cup B).$$

3. The display in the proof of Theorem 2.1. For submodular $f : 2^X \to \mathbb{R}$ and every $S \subseteq X$, with $\bar S = X \setminus S$,

$$\mathbf{E}[f(X(1/2))] \ge \tfrac14 f(\emptyset) + \tfrac14 f(S) + \tfrac14 f(\bar S) + \tfrac14 f(X).$$

The milestones need no sign on the function; nonnegativity enters only in the goal.

Significance

The result. Theorem 2.1 gives an algorithm that makes no query at all and is still a constant-factor approximation for unconstrained non-monotone submodular maximization. It sets the baseline that every later algorithm for the problem is measured against: the paper's own nonadaptive $\tfrac13$-algorithm and its local search algorithms with factors $\tfrac13$ and $\tfrac25$, followed by later work culminating in the tight $\tfrac12$-approximation of Buchbinder, Feldman, Naor and Schwartz (FOCS 2012). The paper also shows that $\tfrac14$ is optimal among nonadaptive algorithms required to return one of the queried sets, and that $\tfrac12$ is optimal for symmetric functions among all algorithms using polynomially many value queries, so both factors of Theorem 2.1 have a precise place in the complexity landscape. Lemma 2.3, the probabilistic inequality behind it, is reused in the analyses of the nonadaptive algorithm and of smooth local search.

Formalizing it. The result is proved, with a short proof. What this mission adds is a machine-checked version of the random-set guarantee and of the two sampling lemmas, stated for arbitrary finite ground sets and, for the lemmas, for real-valued submodular functions without a sign. To our knowledge none of these statements has a machine-checked proof; Mathlib has no theory of submodular set functions or of their multilinear extension.

Difficulty

The goal itself is a two-line consequence of the third milestone. The work sits in the lemmas and in one change of viewpoint.

Lemma 2.2 is not a pointwise statement: the random set $A(p)$ can be any subset of $A$, and $g$ can be smaller on it than both $g(\emptyset)$ and $g(A)$. The inequality holds only in expectation, and only because submodularity controls the marginal value of each element uniformly across the sets it can be added to. Lemma 2.3 needs a conditioning argument over two independent samples; the sets $A$ and $B$ may overlap, and on $A \cap B$ the union $A(p) \cup B(q)$ contains an element with probability $1 - (1-p)(1-q)$, so it is not the product distribution with probability $p$ on $A$ and $q$ on $B$. Finally, the third milestone requires identifying the uniform random subset $X(1/2)$ with the union of independent half-samples of $S$ and of its complement, as a statement about finite sums.

The obvious attempt at the goal, comparing $f(R)$ with $f(S^*)$ for an optimal $S^*$ set by set, fails: $f$ is not monotone, so a random set that contains most of $S^*$ may still have small value, and a random set can pick up elements that hurt.

Formalization scope

The ground set is a Lean type X with [Fintype X] [DecidableEq X]; subsets are Finset X and set functions are f : Finset X → ℝ. Submodularity is the lattice inequality of Definition 1.1, not the decreasing-marginals property. Nonnegativity, the paper's standing assumption $f : 2^X \to \mathbb{R}_+$, is the hypothesis ∀ S, 0 ≤ f S; it appears only in the goal. Symmetry is ∀ S, f Sᶜ = f S for all subsets, not only for an optimal one. $OPT$ is Finset.univ.sup' Finset.univ_nonempty f, a maximum over the always nonempty family of all subsets, so it is attained. The ground set may be empty; the goal holds there too and no nonemptiness is assumed.

Expectations are written as exact finite sums, not as integrals. $\mathbf{E}[f(X(1/2))]$ is the multilinear extension F f (fun _ => 1/2). $\mathbf{E}[g(A(p))]$ is $\sum_{T \subseteq A} p^{|T|}(1-p)^{|A \setminus T|} g(T)$, and $\mathbf{E}[f(A(p) \cup B(q))]$ is the double sum over independent samples $S \subseteq A$, $T \subseteq B$ with the product of the two weights. The ranges $0 \le p \le 1$ and $0 \le q \le 1$, implied in the paper by the word "probability", are explicit hypotheses; Lemma 2.2 is false without them.

Trivializing formalizations are excluded: the weights are exactly those of the uniform distribution on all $2^n$ subsets, $OPT$ is the true maximum rather than the value at one fixed set, and $f$ is required to be both nonnegative and submodular.

Reusable infrastructure produced by a complete development: the multilinear extension of a set function and its expression as an expectation, product-weight identities for independent sampling of subsets (including the decomposition of $X(1/2)$ along a set and its complement), and Lemmas 2.2 and 2.3, which the companion missions on the nonadaptive algorithm and on smooth local search also need. Proofs of any milestone are welcome independently.

Selected references

• U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing Non-Monotone Submodular Functions, SIAM Journal on Computing 40(4):1133–1153, 2011. https://doi.org/10.1137/090779346
• U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing non-monotone submodular functions, Proceedings of the 48th IEEE Symposium on Foundations of Computer Science (FOCS), 2007, pp. 461–471. https://doi.org/10.1109/FOCS.2007.29
• N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, SIAM Journal on Computing 44(5):1384–1402, 2015 (FOCS 2012). https://doi.org/10.1137/130929205
• G. L. Nemhauser, L. A. Wolsey, M. L. Fisher, An analysis of approximations for maximizing submodular set functions — I, Mathematical Programming 14:265–294, 1978. https://doi.org/10.1007/BF01588971