Combinatorics

Motivation

Many problems in signal processing, statistics and function interpolation ask for a solution of a linear system $Ax\approx b$ that uses as few columns of $A$ as possible: a sparse approximate solution. Natarajan's 1995 paper Sparse Approximate Solutions to Linear Systems (SIAM J. Comput. 24(2):227–234) was motivated by radial basis interpolation, where each column corresponds to a basis function and fewer columns mean a cheaper interpolant. The paper does two things. It proves that finding the sparsest approximate solution is computationally hard (§2, Theorem 1), and it analyses a greedy column-selection algorithm whose number of chosen columns is within a factor, depending on the conditioning of $A$, of the optimum (§3, Theorem 2; a separate mission of this series).

The hardness theorem is the reason the second half of the paper exists: once exact minimization is ruled out, one settles for approximation guarantees. It is cited throughout the compressed-sensing literature as the canonical statement that $\ell_0$-minimization under an $\ell_2$ error constraint is NP-hard, and is the starting point for the later theory of when convex relaxations recover sparse solutions.

The argument follows the classical reduction from Exact Cover by 3-sets (X3C) to minimum-weight solutions of linear systems in Garey and Johnson (1979), pp. 221 and 246, adapted to an approximate right-hand side.

Setting

Sparse approximate solution (SAS). Given a matrix $A\in\mathbb R^{m\times n}$, a vector $b\in\mathbb R^m$ and a tolerance $\varepsilon>0$, find a vector $x\in\mathbb R^n$ with $\|Ax-b\|_2\le\varepsilon$ whose number of nonzero entries, written $\|x\|_0=|\{j : x_j\neq0\}|$, is as small as possible. Here $\|\cdot\|_2$ is the Euclidean norm.

Exact Cover by 3-sets (X3C). An instance is a ground set $S=\{s_1,\dots,s_m\}$ and a list $C=c_1,\dots,c_n$ of subsets of $S$, each with exactly three elements. An exact cover is a sub-collection $\hat C=\{c_j : j\in J\}$, $J\subseteq\{1,\dots,n\}$, such that every element of $S$ occurs in exactly one set of $\hat C$.

The transformation. From an X3C instance build the SAS instance with

• the incidence matrix $A\in\mathbb R^{m\times n}$: $A_{ij}=1$ if $s_i\in c_j$ and $A_{ij}=0$ otherwise, so column $j$ is the characteristic vector of $c_j$;
• the all-ones vector $b=(1,1,\dots,1)\in\mathbb R^m$;
• the tolerance $\varepsilon=\tfrac12$.

In Lean, $S$ is Fin m, the collection is C : Fin n → Finset (Fin m) with hC : ∀ j, (C j).card = 3, an exact cover is an index set J with IsExactCover C J, the matrix is incidence C, the vector $b$ is onesVec m, $Ax$ is Matrix.toEuclideanLin (incidence C) x, and $\|x\|_0$ is nnz x.

Formalization targets

Goal: correctness of the reduction

For every X3C instance $(S,C)$ as above,

$$\bigl(\exists J,\ \{c_j\}_{j\in J}\text{ is an exact cover of }S\bigr)\iff\bigl(\exists x\in\mathbb R^n,\ \|Ax-b\|_2\le\tfrac12\ \text{and}\ 3\,\|x\|_0\le m\bigr).$$

This is the sentence the proof of Theorem 1 (p. 228) establishes: "the constructed instance of SAS has a solution with $m/3$ or fewer entries if and only if the given instance of X3C has a solution."

Milestones

1. Forward direction. If $\{c_j\}_{j\in J}$ is an exact cover, the indicator vector $x=\mathbf 1_J$ satisfies $Ax=b$ and $3\|x\|_0=m$.
2. Entry bounds. For every $x$ with $\|Ax-b\|_2\le\frac12$, each entry of $Ax$ lies in $[\frac12,\frac32]$.
3. Lower bound on sparsity. For every such $x$, $m\le3\|x\|_0$.
4. Exact cover from a sparse solution. If moreover $3\|x\|_0\le m$, the sets $c_j$ with $x_j\neq0$ form an exact cover.

Significance

The result. The equivalence shows that deciding whether a sparse approximate solution with a prescribed number of nonzeros exists is at least as hard as X3C, which is NP-complete. Consequently no polynomial-time algorithm computes the optimum of SAS unless P = NP, and approximation algorithms such as the greedy method of §3 are the natural object of study. The same instance shows hardness persists for 0/1 matrices, a right-hand side of all ones and a constant tolerance, so the difficulty does not come from ill-conditioned data or from vanishing precision.

Formalizing it. The reduction is proved in the paper; this mission produces a machine-checked proof of its correctness, the combinatorial core of every NP-hardness claim for $\ell_0$-constrained least squares. No prior machine-checked version is known to exist, on the platform or elsewhere. The complexity-theoretic wrapper is out of scope (see below).

Difficulty

The forward direction is a direct computation. The converse contains the only real step, which the paper passes over with "it is clear". From $\|Ax-b\|_2\le\frac12$ one gets only that every entry of $Ax$ is in $[\frac12,\frac32]$; the entries of $x$ themselves are arbitrary reals, possibly negative or not equal to $1$, so $x$ need not be an indicator vector and $Ax=b$ need not hold. The exact-cover property must therefore be extracted from support sizes alone: every element is covered by some column in the support, the support has at most $m/3$ columns of three elements each, and a counting argument forces the chosen sets to be pairwise disjoint. Reading off a cover from the values of $x$ (for instance, taking the $j$ with $x_j=1$) does not work.

Formalization scope

• Vectors live in EuclideanSpace ℝ (Fin m) and EuclideanSpace ℝ (Fin n), so ‖·‖ is the paper's $\|\cdot\|_2$. Using the sup norm of Fin m → ℝ would give a different statement.
• The tolerance is exactly $\varepsilon=\frac12$, as printed.
• The collection is indexed, C : Fin n → Finset (Fin m): repeated sets are allowed and are distinct indices; an exact cover is a set of indices, and on the SAS side one nonzero entry is counted per index, so both sides treat duplicates consistently.
• "$m/3$ or fewer" is written $3\|x\|_0\le m$, never with natural-number division. With this form the equivalence holds for every $m$ (both sides are false when $3\nmid m$), which absorbs the paper's "without loss of generality $m$ is a multiple of 3"; no divisibility hypothesis is assumed. For $m=0$ both sides are true.
• The hypothesis that every set has exactly three elements is essential for the converse (with $m=9$, $O=\{s_3,\dots,s_9\}$, $c_1=\{s_1\}\cup O$, $c_2=\{s_2\}\cup O$, $c_3=O$, the vector $x=(1,1,-1)$ solves $Ax=b$ with $3\|x\|_0=m$, yet $C$ has no exact cover since $c_1$ and $c_2$ must both be chosen) and is kept as hC.
• Not formalized: the infinite-precision RAM machine model, polynomial-time many-one reductions, polynomial-time computability of the transformation (evident: an $m\times n$ 0/1 matrix), and the NP-completeness of X3C (cited by the paper from Garey–Johnson). The goal is therefore the correctness of the transformation, not a statement titled "SAS is NP-hard". A statement that only records the forward direction, or that fixes $x$ to be a 0/1 vector on the SAS side, would trivialize the converse and is not the target.
• Tools a solver will need are in Mathlib: coordinate bounds for the Euclidean norm (PiLp.norm_apply_le), Finset.card_biUnion_le, and Finset.card_biUnion for disjoint unions. Contributions of a reusable exact-cover API, or of a polynomial-time reduction framework that could later wrap this equivalence into an NP-hardness theorem, are welcome.

Selected references

• B. K. Natarajan, Sparse Approximate Solutions to Linear Systems, SIAM Journal on Computing 24(2):227–234, 1995. https://doi.org/10.1137/s0097539792240406
• M. R. Garey and D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979 (X3C: problem [SP2], p. 221; minimum weight solution to linear equations: [MP5], p. 246).
• F. P. Preparata and M. I. Shamos, Computational Geometry: An Introduction, Springer, 1985 (the real RAM model). https://doi.org/10.1007/978-1-4612-1098-6

Motivation

Multistage stochastic programs are solved on a finite scenario tree: a discrete probability distribution whose support points are paths of a random process. Realistic trees have far too many scenarios for the resulting optimization problem, so practitioners reduce the tree, keeping $n$ of its $N$ scenarios and redistributing the probability of the deleted ones. The reduction should keep the reduced distribution as close as possible to the original one in a probability metric that controls the optimal value of the stochastic program (Dupačová, Gröwe-Kuska, Römisch, Math. Program. 95 (2003)).

Choosing the best $n$ scenarios is a set-covering problem and NP-hard, and the algorithms used in practice (backward reduction, fast forward selection) are heuristics without error guarantees. Heitsch and Römisch (2003) therefore derived test instances with an exactly known optimum: regular binary and ternary scenario trees, for which the minimal reduction distance has a closed form once $n$ is not too small. This mission formalizes the ternary case, Proposition 3.2 of that paper. The binary case (Proposition 3.1) is a separate mission of the same series.

Setting

Fix a depth $K \in \mathbb{N}$ and branch widths $\delta^1, \dots, \delta^K \ge 0$, with $\delta^0 = 0$. A regular ternary scenario tree has $N = 3^K$ scenarios, one for each index tuple $(i_1, \dots, i_K) \in \{1, 2, 3\}^K$, where $i_k$ is the successor chosen at level $k$. Choosing successor $i_k$ adds the increment $\delta^k_{i_k} = (i_k - 2)\,\delta^k \in \{-\delta^k, 0, \delta^k\}$, and scenario $i$ is the vector $\omega_i = (\omega_i^0, \dots, \omega_i^K) \in \mathbb{R}^{K+1}$ with

$$\omega_i^k = \sum_{j=0}^{k} \delta^j_{i_j}, \qquad k = 0, \dots, K \quad \text{(eq. (19))}.$$

All scenarios have probability $p_i = 1/N$. The distance between scenarios is the maximum norm $c(\omega_i, \omega_j) = \|\omega_i - \omega_j\|_\infty = \max_{0 \le k \le K} |\omega_i^k - \omega_j^k|$.

Deleting the scenarios of an index set $J$ and moving each deleted scenario's probability to a nearest kept scenario costs the reduction distance

$$D_J = \sum_{i \in J} p_i \min_{j \notin J} \|\omega_i - \omega_j\|_\infty \quad \text{(eq. (8))},$$

which by Theorem 2.1 of the paper is the optimal transport-type distance between the original distribution and the best distribution supported on the kept scenarios. The minimal reduction distance to $n$ scenarios is $D^{min}_n = \min\{D_J : \#J = N - n\}$.

Formalization targets

Goal: Proposition 3.2 (7/9-solution)

Let $K \ge 3$ and let $k_0 \in \arg\min_{1 \le k \le K} \delta^k$ with $k_0 \le K - 2$ and $\max\{\delta^{k_0+1}, \delta^{k_0+2}\} \le 2\delta^{k_0}$. Then any two distinct scenarios are at distance at least $\delta^{k_0}$; there is a set of $\tfrac79 N$ scenarios each paired with a scenario outside it at distance exactly $\delta^{k_0}$; and for each $n \in \mathbb{N}$ with $\tfrac29 N \le n < N$,

$$D^{min}_n = \min\{D_J : \#J = N - n\} = \frac{N - n}{N}\,\delta^{k_0} \quad \text{(eq. (21))},$$

with the minimum attained.

Milestones

1. Distinct scenarios satisfy $\|\omega_i - \omega_j\|_\infty \ge \delta^{k_0}$.
2. Every $J$ with $\#J = N - n$ has $D_J \ge \frac{N-n}{N}\delta^{k_0}$.
3. The index set $I_{**}$ of the proof has $\#I_{**} = \tfrac29 N$, and its complement $J_{**}$ has $\tfrac79 N$ elements.
4. Every $j \in J_{**}$ has a partner $i \in I_{**}$ with $\|\omega_i - \omega_j\|_\infty = \delta^{k_0}$.
5. Example 4.2: for $K = 6$ and $(\delta^1, \dots, \delta^6) = (0.7, 0.9, 1.2, 1.5, 2.6, 3.3)$, $D^{min}_n = 0.7\,\frac{N-n}{N}$ for $162 \le n < 729$.

Significance

The result gives an exact optimal value for an NP-hard reduction problem on an infinite family of instances. Heitsch and Römisch use it in their numerical section to measure how far the heuristics' reduced trees are from optimal (Examples 4.1 and 4.2 are the binary and ternary test trees of that study). A closed form of this kind is also the only way to certify that a heuristic is exactly optimal on some instances rather than only competitive with other heuristics.

The proposition is proved in the paper, but the published proof of its central step is one sentence: "Similarly as in Proposition 3.1 it can be shown that there exists an index $i \in I_{**}$ for each $j \in J_{**}$ …". A formal proof supplies that case analysis, which is absent from the literature. The formalization also settles two points the printed statement leaves loose (see Formalization scope): the count of pairs at distance $\delta^{k_0}$, and the definition of $I_{**}$ when some widths vanish. No machine-checked version of this result or of the reduction distance $D_J$ is known to exist.

Difficulty

The lower bound is routine: two distinct scenarios first differ at some level $l$, where their coordinates differ by $\delta^l$ or $2\delta^l$. The substance is attainment: one must exhibit, for every $n \ge \tfrac29 N$, a kept set of size $n$ whose every deleted scenario lies at distance exactly $\delta^{k_0}$ from some kept one. The obvious candidate, keeping the scenarios that take the middle branch at level $k_0$, has every other scenario at distance exactly $\delta^{k_0}$ from a kept one, but it keeps $\tfrac13 N$ scenarios and so covers only $n \ge \tfrac13 N$. Going down to $\tfrac29 N$ kept scenarios forces a deleted scenario and its partner to differ at more than one level, and since coordinates are running sums the differences at levels $k_0+1$ and $k_0+2$ accumulate on top of the one at level $k_0$. The paper's proof of this step is not written out, and it depends on the widths of the two levels below $k_0$: the hypothesis $\max\{\delta^{k_0+1}, \delta^{k_0+2}\} \le 2\delta^{k_0}$ is essential, and the result is false without it (for $K = 3$ and $(\delta^1, \delta^2, \delta^3) = (1, 3, 3)$ one has $D^{min}_6 = 31/27$, not $7/9$).

Formalization scope

• A scenario is an index tuple $\sigma : \mathrm{Fin}\,K \to \mathrm{Fin}\,3$; $\sigma(r)$ is the successor at paper level $r + 1$, with $\mathrm{Fin}\,3$ values $0, 1, 2$ standing for the paper's $i = 1, 2, 3$. The widths are $\delta : \mathbb{N} \to \mathbb{R}$, of which only $\delta(1), \dots, \delta(K)$ are used; the standing assumption $\delta^k \in \mathbb{R}_+$ (p. 196) is the hypothesis $\delta(k) \ge 0$ for $1 \le k \le K$. Scenarios live in $\mathrm{Fin}(K+1) \to \mathbb{R}$, whose Mathlib norm is the maximum norm. Probabilities are uniform, $1/3^K$.
• $D_J$ is defined for a general finite index set, probabilities and cost, with the inner minimum a Finset.inf' over the complement of $J$; the complement must be nonempty, so no default value arises. $D^{min}_n$ is stated as IsLeast of the set of all values $D_J$ with $\#J = N - n$: the goal asserts both the lower bound for every $J$ and attainment by some $J$. A formalization that exhibits a single $J$ with $D_J = \frac{N-n}{N}\delta^{k_0}$, or states an infimum without attainment, or drops any hypothesis on $k_0$, is a different (and in the last case false) statement.
• $\tfrac29 N \le n$ is written $2 \cdot 3^K \le 9n$, and $\tfrac79 N$ as $7 \cdot 3^{K-2}$.
• Pairs. As printed, "there are $\tfrac79 N$ distinct pairs of scenarios such that the distance between the members of each pair is exactly $\delta^{k_0}$" is false as an exact count (for $K = 3$ and $\delta = (1,1,1)$ there are 130 such pairs, not 21). The goal states what the proof constructs: a set $J_{**}$ of $\tfrac79 N$ scenarios, each paired with a scenario outside $J_{**}$ at distance exactly $\delta^{k_0}$.
• $I_{**}$. The paper defines $I_{**}$ by testing whether the increments $\delta^k_{i_k}$ vanish. When one of $\delta^{k_0}, \delta^{k_0+1}, \delta^{k_0+2}$ is $0$ this no longer identifies the middle branch and the count $\tfrac29 N$ fails, although the proposition remains true. The formalization defines $I_{**}$ by branch indices (middle branch versus outer branches), which agrees with the paper whenever these three widths are positive. No positivity hypothesis is added to the goal.
• Welcome contributions: a reusable library for regular scenario trees (first differing level, distance of paths), and the case analysis of milestone 4. The binary mission of this series needs the same lower-bound argument with the constant $2\delta^{k_0}$.

Selected references

• H. Heitsch, W. Römisch, Scenario Reduction Algorithms in Stochastic Programming, Computational Optimization and Applications 24 (2003), 187–206. https://doi.org/10.1023/A:1021805924152
• J. Dupačová, N. Gröwe-Kuska, W. Römisch, Scenario reduction in stochastic programming: An approach using probability metrics, Mathematical Programming 95 (2003), 493–511. https://doi.org/10.1007/s10107-002-0331-0

Why exact reduction distances matter

Multistage stochastic programs are solved on a finite scenario tree, a discrete probability measure whose atoms are paths of a stochastic process. The size of the deterministic equivalent grows with the number of scenarios, so practitioners replace the original measure $P=\sum_{i=1}^N p_i\delta_{\omega_i}$ by a measure supported on $n<N$ of its scenarios. Stability theory for stochastic programs (Dupačová, Gröwe-Kuska and Römisch, Math. Program. 95 (2003), doi:10.1007/s10107-002-0331-0) bounds the change of the optimal value by a probability metric between the two measures, which leads to the optimal scenario reduction problem: choose which $N-n$ scenarios to delete so that this distance is smallest.

That problem is a set-covering problem and is NP-hard, and the algorithms that Heitsch and Römisch study in the same paper (backward reduction, fast forward selection) are heuristics without error guarantees. To test them one needs original measures whose optimal reduction distance is known exactly. Section 3 of Heitsch and Römisch, Scenario Reduction Algorithms in Stochastic Programming, Comput. Optim. Appl. 24 (2003) (doi:10.1023/A:1021805924152) supplies such instances: regular binary and ternary scenario trees, for which the minimal distance to any reduced tree with at least a fixed fraction of the scenarios is an explicit formula. This mission formalizes the binary case, Proposition 3.1.

Setting

Fix a horizon $K\in\mathbb N$ and level parameters $\delta^1,\dots,\delta^K\ge0$, with $\delta^0=0$. A regular binary scenario tree has $N=2^K$ scenarios. A scenario is determined by a branch $i_k\in\{1,2\}$ at every level $k=1,\dots,K$, and is the vector $\omega_i=(\omega_i^0,\dots,\omega_i^K)\in\mathbb R^{K+1}$ with

$$\omega_i^k=\sum_{j=0}^k\delta^j_{i_j},\qquad \delta^j_{i_j}=(2i_j-3)\,\delta^j\in\{-\delta^j,+\delta^j\}.\tag{19}$$

All scenarios start at the root $\omega_i^0=0$ and carry probability $p_i=1/N$. Scenarios are compared in the maximum norm $\|\omega-\tilde\omega\|_\infty=\max_{k=0,\dots,K}|\omega^k-\tilde\omega^k|$.

Deleting the scenarios with indices in $J\subset\{1,\dots,N\}$ and moving each deleted scenario's probability to a nearest kept scenario costs the reduction cost

$$D_J=\sum_{i\in J}p_i\min_{j\notin J}\|\omega_i-\omega_j\|_\infty,\tag{8}$$

which by Theorem 2.1 of the paper is the minimal Kantorovich-type distance between $P$ and a measure supported on the kept scenarios. The minimal reduction distance for $n$ kept scenarios is $D^{min}_n=\min\{D_J:\#J=N-n\}$.

In the Lean development, scenarios are indexed by σ : Fin K → Fin 2 (Fin-index $r$ is tree level $r+1$, value $0$ is the branch $-\delta$, value $1$ is $+\delta$), lev σ k is the branch at level $k$, scenario δ σ : Fin (K+1) → ℝ is $\omega_\sigma$, and redCost δ J hJ is $D_J$.

Formalization targets

Goal: Proposition 3.1 (3/4-solution)

Let $K\ge3$, $k_0\in\arg\min_{1\le k\le K}\delta^k$, $k_0\le K-2$ and $\max\{\delta^{k_0+1},\delta^{k_0+2}\}\le2\delta^{k_0}$. Then any two distinct scenarios are at distance at least $2\delta^{k_0}$; there is a set $J_*$ of $\frac34N$ scenarios each of which has a partner outside $J_*$ at distance exactly $2\delta^{k_0}$; and for every $n\in\mathbb N$ with $\frac N4\le n<N$

$$D^{min}_n=\min\{D_J:\#J=N-n\}=\frac{N-n}{N}\,2\delta^{k_0}.\tag{20}$$

Milestones

1. Two scenarios that first differ at level $l$ are at distance $\ge2\delta^l\ge2\delta^{k_0}$.
2. $D_J\ge\frac{N-n}{N}2\delta^{k_0}$ for every $J$ with $\#J=N-n$.
3. The index set $I_*$ (branch at $k_0$ opposite to the common branch at $k_0+1,k_0+2$) has $\#I_*=N/4$, so $\#J_*=\frac34N$.
4. Every $j\in J_*$ has a partner $i\in I_*$ with $\|\omega_i-\omega_j\|_\infty=2\delta^{k_0}$.
5. Example 4.1: for $K=10$ and the paper's parameters, Proposition 3.1 applies with $k_0=1$ and $D^{min}_n=\frac{N-n}{N}$ for $256\le n<1024$.

Significance

The result. Proposition 3.1 gives the exact optimum of an NP-hard combinatorial problem on an explicit, parametrized family of instances of every size $N=2^K$. Section 4 of the paper uses it (Example 4.1, $N=1024$) as ground truth for the relative accuracy of backward reduction and fast forward selection. Without it, the quality of a heuristic reduction on a large tree could only be compared with other heuristics or with lower bounds.

The formalization. The proposition is proved in the paper; to our knowledge no machine-checked version exists. A formal proof certifies the benchmark values, and the statement also corrects the printed text in two places. First, "there are $\frac34N$ distinct pairs … at distance exactly $2\delta^{k_0}$" is false as an exact count (for $K=3$, $\delta=(1,1,1)$ there are twenty such pairs, not six), so the goal states "at least", in the form the proof exhibits. Second, the paper's sign-based definition of $I_*$ degenerates when some $\delta^k=0$, although the proposition still holds; the mission defines $I_*$ by branch indices.

Difficulty

The lower bound is a direct computation. The content is the matching upper bound: a set $J$ of the prescribed size for which every deleted scenario has a kept scenario at the minimal possible distance. A natural first attempt pairs scenarios that differ only at level $k_0$. That handles only half of the scenarios with a single partner each, and it cannot reach $\frac34N$ deleted scenarios. Once scenarios differ at more than one level, their maximum-norm distance is a maximum of several partial sums, and keeping all of them at most $2\delta^{k_0}$ is exactly where the hypothesis $\max\{\delta^{k_0+1},\delta^{k_0+2}\}\le2\delta^{k_0}$ enters. Without it, eq. (20) fails: for $K=3$, $\delta=(1,3,3)$ and $n=2$ the true minimum is $\frac52$, not $\frac32$. The passage from $n=N/4$ to general $n\ge N/4$ also needs care: the deleted set must shrink while each remaining deleted scenario keeps its partner among the kept ones.

Formalization scope

• The index type is Fin K → Fin 2, which has exactly $2^K$ elements. The paper's $(K+1)$-tuple has a level-0 entry with no choice, so it is dropped, and the vector $\omega$ keeps its $K+1$ coordinates with $\omega^0=0$.
• The parameters are δ : ℕ → ℝ, with $\delta^k\ge0$ and the arg min stated for $k=1,\dots,K$ only. $\delta^k>0$ is not assumed, because the paper allows $\delta^k\in\mathbb R_+$ and the proposition holds with zeros.
• The cost is Mathlib's norm on Fin (K+1) → ℝ, which is the maximum norm, and $p_i=1/2^K$ is written out.
• $D_J$ requires a nonempty set of kept scenarios, and its inner minimum is a finite Finset.inf'.
• $D^{min}_n$ is stated with IsLeast over the set of attained values $D_J$, $\#J=N-n$, so both the lower bound and attainment are part of the goal. A proof of $D_{J}\le\frac{N-n}{N}2\delta^{k_0}$ for a single exhibited $J$, or a real infimum without attainment, does not prove the goal.
• "$\frac N4\le n$" is written $2^K\le4n$, and $\frac34N$ is $3\cdot2^{K-2}$.
• The pairs claim is "at least $\frac34N$ pairs", expressed as a set $J_*$ of that size with a partner outside $J_*$ for every member.
• All hypotheses on $k_0$ appear in the goal; dropping any of them makes (20) false.

Useful infrastructure: sup-norm lemmas for Fin n → ℝ (pi_norm_le_iff_of_nonneg, norm_le_pi_norm), Finset.inf' lemmas, and counting functions Fin K → Fin 2 with prescribed values (Fintype.card_fun, Fintype.card_pi). The tree and reduction-cost definitions are shared in spirit with the ternary-tree mission of this series (Proposition 3.2), and a proof whose structure transfers to $d=3$ is welcome. Contributions of proofs of the milestones individually, in any order, are welcome.

Selected references

• H. Heitsch, W. Römisch, Scenario Reduction Algorithms in Stochastic Programming, Computational Optimization and Applications 24 (2003), 187–206. doi:10.1023/A:1021805924152
• J. Dupačová, N. Gröwe-Kuska, W. Römisch, Scenario reduction in stochastic programming: An approach using probability metrics, Mathematical Programming 95 (2003), 493–511. doi:10.1007/s10107-002-0331-0

Motivation

The nearest common ancestor (nca) problem asks, for a fixed rooted tree and a sequence of vertex pairs $(v, w)$, for the deepest vertex that is an ancestor of both. It is a basic step in suffix-tree string algorithms and is equivalent to range-minimum queries (Bender, Farach-Colton, 2000). Harel and Tarjan, Fast Algorithms for Finding Nearest Common Ancestors, SIAM J. Comput. 13 (1984) 338–355, gave the first algorithm answering each query on a static tree in constant time on a random-access machine after linear preprocessing.

Their construction reduces the general problem to the case of a complete binary tree, where §3 of the paper shows that nca queries can be answered "by direct calculation" on vertex numbers: multiplication, division, powers of two, the base-two logarithm and bitwise exclusive or. The later simplification of Schieber and Vishkin (1988) is built on the same in-order numbering of a complete binary tree. This mission formalizes that arithmetic core.

Timeline, as reviewed in the paper's §1 (pp. 338–340):

• 1976: Aho, Hopcroft and Ullman (SIAM J. Comput. 5) give an $O(n + m\alpha(m+n, n))$-time off-line algorithm on a pointer machine, and for static trees a random-access algorithm with $O(n \log\log n)$ preprocessing and $O(\log\log n)$ time per query.
• 1976: van Leeuwen (unpublished report) gives an $O(n + m \log\log n)$-time algorithm for linking roots and static trees that runs on a pointer machine in $O(n)$ space.
• 1980: Harel (Proc. 21st FOCS) gives a preliminary version of the paper's results.
• 1984: Harel and Tarjan prove that pointer machines need $\Omega(\log\log n)$ time per query on static trees (Theorem 1), and give the $O(n)$-preprocessing, $O(1)$-query random-access algorithm whose base case is the subject of this mission.

Setting

Fix $d \ge 0$ and let $T$ be the complete binary tree of depth $d$. A vertex is identified with the path from the root to it, a word of at most $d$ left or right turns; the root is the empty word and $T$ has $n = 2^{d+1} - 1$ vertices. Following the paper's Appendix (pp. 354–355):

• $w$ is an ancestor of $v$ ($v$ a descendant of $w$) if the word $w$ is a prefix of the word $v$; every vertex is its own ancestor. $v$ and $w$ are unrelated if neither is an ancestor of the other.
• The depth of $v$ is its distance to the root; its height $h(v)$ is the length of the longest path from a leaf to $v$, which in $T$ is $d - \operatorname{depth}(v)$.
• $\operatorname{nca}(v, w)$ is the vertex of greatest depth that is an ancestor of both: the longest common prefix.

The vertices of $T$ are numbered from $1$ to $n$ in symmetric order (in-order): at every vertex, first the left subtree, then the vertex, then the right subtree. $\mathrm{sym}(v)$ is the number of $v$ and $\mathrm{sym}^{-1}(i)$ the vertex numbered $i$. For $d = 4$ (Fig. 1 of the paper) the root is $16$, its children $8$ and $24$, and the leaves $1, 3, 5, \dots, 31$. $i \oplus j$ denotes bitwise exclusive or and $\lg$ the base-two logarithm.

Two procedures of §3 use only numbers, heights and $d$:

• the nca depth algorithm: return $d - h(v)$ if $\mathrm{sym}(w) \in [\mathrm{sym}(v) - 2^{h(v)} + 1, \mathrm{sym}(v) + 2^{h(v)} - 1]$; else $d - h(w)$ if the same holds with $v, w$ exchanged; else $d - \lfloor \lg(\mathrm{sym}(v) \oplus \mathrm{sym}(w)) \rfloor$;
• the depth algorithm: given $v$ and a depth $d_2 \le \operatorname{depth}(v)$, with $h = d - d_2$, return $\mathrm{sym}^{-1}\bigl(2^{h+1}\lfloor \mathrm{sym}(v)/2^{h+1}\rfloor + 2^h\bigr)$.

Formalization targets

Goal: the nca algorithm is correct

The algorithm to compute $\operatorname{nca}(v,w)$ (p. 342) runs the nca depth algorithm to obtain $d_0$ and then the depth algorithm on $(v, d_0)$. The goal states that it returns the nearest common ancestor: for all vertices $v, w$ of $T$, with $d_0$ the output of the nca depth algorithm and $h = d - d_0$,

$$\mathrm{sym}(\operatorname{nca}(v,w)) = 2^{h+1}\left\lfloor \frac{\mathrm{sym}(v)}{2^{h+1}} \right\rfloor + 2^h .$$

Milestones

In the order the paper uses them:

1. Numbers at height $h$ (p. 341): the vertices of height $h$ are numbered $2^h, 3\cdot 2^h, 5\cdot 2^h, \dots$ from left to right.
2. Lemma 1: $h(v)$ is the largest $h$ with $2^h \mid \mathrm{sym}(v)$.
3. Lemma 2: the descendants of $v$ are the vertices numbered in $[\mathrm{sym}(v) - 2^{h(v)} + 1, \mathrm{sym}(v) + 2^{h(v)} - 1]$.
4. Lemma 3: for a height $h \ge h(v)$, the height-$h$ ancestor of $v$ has number $2^{h+1}\lfloor \mathrm{sym}(v)/2^{h+1}\rfloor + 2^h$.
5. Lemma 4: for unrelated $v, w$,

$$h(\operatorname{nca}(v,w)) = \lfloor \lg(\mathrm{sym}(v) \oplus \mathrm{sym}(w)) \rfloor .$$

6. The nca depth algorithm returns $\operatorname{depth}(\operatorname{nca}(v,w))$.
7. The depth algorithm returns the number of the depth-$d_2$ ancestor of $v$.

Two supporting statements pin the definitions to the paper: $\mathrm{sym}$ is a bijection onto $\{1, \dots, 2^{d+1} - 1\}$, and the longest common prefix is the deepest common ancestor.

Significance

The constant-time nca computation on complete binary trees is the base case of the whole paper: §§4–5 embed an arbitrary tree into a moderately sized complete binary tree through a compressed tree and a balanced binary tree, and every query ends with the arithmetic of §3. The same idea, that in-order numbers encode ancestry in their low-order bits, underlies the Schieber–Vishkin algorithm. Lemma 1 identifies the height with the 2-adic valuation of the number, and Lemma 4 identifies the nca height with the position of the highest differing bit.

The results are proved in the paper, with the proofs left as "easy to verify". No machine-checked version of this numbering or of these four lemmas is known to exist in Mathlib or on this platform. A formal development supplies proofs of the four lemmas and the two algorithms, and a reusable library connecting in-order ranks of a complete binary tree to binary arithmetic (Nat.log, bitwise xor, 2-adic valuation).

Difficulty

The numbering is defined by a traversal order, while the lemmas speak about divisibility, floor division and exclusive or. The work lies in connecting the rank of a vertex in symmetric order to its closed form $(2j+1)\cdot 2^{h(v)}$, where $j$ is its left-to-right position. That counting argument sums the sizes of the subtrees that precede $v$ and is where most of the effort goes. Lemma 4 then needs the observation that two unrelated numbers agree in all bits above the height of their nca and differ in the bit at that height. This is a statement about Nat.testBit of the exclusive or, and it fails for related vertices. The algorithm statements add a case analysis whose first two cases overlap when $v = w$.

Formalization scope

• A vertex of the tree of depth $d$ is a List Bool of length at most $d$ (false = left). Ancestry is the prefix relation, $\operatorname{nca}$ the longest common prefix, depth the length, and height $d - \text{length}$. None of these structural notions uses the numbering.
• $\mathrm{sym}(v)$ is the number of vertices whose in-order sort key is lexicographically at most that of $v$. The key is the path with left $\mapsto 0$, right $\mapsto 2$, followed by $1$. The numbering is not defined by the closed form or by a recursion on numbers: a definition of that kind would make the height-$h$ numbering and Lemma 1 immediate and move the content of the mission into an uncheckable definition.
• $\lfloor \lg x \rfloor$ is Nat.log 2 x, which agrees for $x \ge 1$. $\oplus$ is ^^^ on $\mathbb N$, and floor division is / on $\mathbb N$.
• Interval tests $a \in [b - c + 1, b + c - 1]$ are written additively as $b + 1 \le a + c$ and $a + 1 \le b + c$. The subtractions $d - h(v)$ and $d - d_2$ never truncate for heights and depths of vertices.
• Lemma 3 states explicitly that $h \le d$ ("$h$ is a height") and that the ancestor exists. The depth algorithm assumes $d_2 \le \operatorname{depth}(v)$, as printed.
• $\mathrm{sym}^{-1}$ is not defined as a function. The goal and the depth algorithm state that a vertex has the computed number if and only if it is the nearest common ancestor (respectively the ancestor at depth $d_2$), which says that $\mathrm{sym}^{-1}$ of that number is that vertex.
• The $O(1)$ time bounds are not formalized, since the random-access machine model is out of scope.

Proofs of any milestone are welcome.

Selected references

• D. Harel and R. E. Tarjan, Fast Algorithms for Finding Nearest Common Ancestors, SIAM J. Comput. 13(2) (1984), 338–355. https://doi.org/10.1137/0213024
• A. V. Aho, J. E. Hopcroft and J. D. Ullman, On Finding Lowest Common Ancestors in Trees, SIAM J. Comput. 5(1) (1976), 115–132. https://doi.org/10.1137/0205011
• B. Schieber and U. Vishkin, On Finding Lowest Common Ancestors: Simplification and Parallelization, SIAM J. Comput. 17(6) (1988), 1253–1262. https://doi.org/10.1137/0217079
• M. A. Bender and M. Farach-Colton, The LCA Problem Revisited, LATIN 2000, LNCS 1776, 88–94. https://doi.org/10.1007/10719839_9

Motivation

The nearest common ancestor problem asks, for a rooted tree and two of its vertices $x$ and $y$, for the deepest vertex that is an ancestor of both, written $\operatorname{nca}(x,y)$. It appears as a subroutine in string algorithms (suffix trees), in graph algorithms (path queries, dominators) and in the analysis of set-union structures. Aho, Hopcroft and Ullman (On finding lowest common ancestors in trees, SIAM J. Comput. 5, 1976) posed it in several versions, differing in how much the tree changes while the queries are answered.

Harel and Tarjan (Fast Algorithms for Finding Nearest Common Ancestors, SIAM J. Comput. 13, 1984) study how the answer depends on the machine model. On a random-access machine, where addresses can be computed arithmetically, they preprocess a static tree in linear time and then answer each query in constant time. On a pointer machine, where memory can only be traversed by following pointers, their §2 shows that no representation of the tree allows constant-time queries: $\Omega(\log\log n)$ steps are needed in the worst case. This mission formalizes that lower bound.

Timeline.

• 1976: Aho, Hopcroft and Ullman give an $O(\log\log n)$-per-query random-access algorithm for static trees.
• 1976: van Leeuwen (Finding lowest common ancestors in less than logarithmic time, unpublished report, reference [14] of Harel–Tarjan) gives an $O(n + m\log\log n)$ algorithm for static trees that runs on a pointer machine.
• 1984: Harel and Tarjan prove Theorem 1, the matching $\Omega(\log\log n)$ lower bound for pointer machines, and the $O(1)$-per-query random-access algorithm.

Setting

A pointer machine stores its data as a collection of nodes. Each node has a fixed number of fields, and a pointer field holds either a node or nil. The machine can follow a pointer from a node it holds, but it cannot compute an address. Following Harel and Tarjan (p. 340), a static tree is represented by a list structure: each tree vertex $v$ is represented by a single node $\mathrm{rep}(v)$, distinct vertices by distinct nodes, and the structure may contain further nodes that represent no vertex. Each node has two pointer fields; the paper reduces any fixed number of pointers to two "without loss of generality". To answer a query on $x$ and $y$, the machine is given pointers to $\mathrm{rep}(x)$ and $\mathrm{rep}(y)$ and must return a pointer to $\mathrm{rep}(\operatorname{nca}(x,y))$.

The node $b$ is accessible from $a$ in $j$ steps or less if it can be reached from $a$ by following at most $j$ pointers. Write $\mathrm{acc}_j(a)$ for the set of such nodes. A run of $t$ steps from input nodes $a$ and $b$ is a sequence $n_1,\dots,n_t$ in which each $n_s$ is the content of a pointer field of a node among $a, b, n_1, \dots, n_{s-1}$. A query with answer $c$ is answered in $k$ steps if some run of at most $k$ steps holds $c$.

The tree is the complete binary tree $T$ of height $h$, with $n = 2^h$ leaves. Its vertices are the words $w \in \{0,1\}^{\le h}$ (the root-to-vertex path, $0$ = left), the ancestors of $v$ are its prefixes, the depth of $w$ is $|w|$ and its height is $h - |w|$. Then $\operatorname{nca}(x,y)$ is the longest common prefix of $x$ and $y$. Logarithms are binary: $\lg = \log_2$.

Formalization targets

Goal: Theorem 1 in the explicit form of its proof

For every $h$, every node type, every list structure with two pointers per node and every injective representation $\mathrm{rep}$ of the complete binary tree with $n = 2^h$ leaves: if every nca query on two leaves is answered in $k$ steps, then

$$k > \lg\lg n - 2 .$$

This is the last display of the proof (p. 341), which is what the paper's $\Omega(\log\log n)$ means. The representation is arbitrary and is quantified before the query bound, so the bound holds for every representation.

Milestones: the claims of the proof

1. A query answered in $k$ steps reaches only nodes in $\mathrm{acc}_k(\mathrm{rep}(x)) \cup \mathrm{acc}_k(\mathrm{rep}(y))$.
2. $|\mathrm{acc}_j(a)| \le 2^{j+1} - 1$ for every node $a$.
3. With $A_x$ the set of vertices whose nodes are accessible from $\mathrm{rep}(x)$ in $k$ steps or less: for a nonleaf $w$ with children $u, v$, either $w \in A_x$ for every leaf $x$ below $u$, or $w \in A_y$ for every leaf $y$ below $v$.
4. A vertex of height $i \ge 1$ lies in $A_x$ for at least $2^{i-1}$ leaves $x$.

$$\sum_{x \in L} |A_x| \ge \frac{n}{2}\lg n,$$

where $L$ is the set of leaves.

Significance

The result. Theorem 1 shows that van Leeuwen's pointer-machine algorithm for static trees is optimal up to a constant factor, and that the constant-time queries of the paper's §§3–5 depend on address arithmetic. It is an early nontrivial lower bound for pointer machines on a natural problem; the paper compares it with Tarjan's lower bound for disjoint-set union on a pointer machine (J. Comput. System Sci. 18, 1979).

Formalizing it. The theorem is proved in the paper; as far as could be determined no machine-checked version exists, and Mathlib has no pointer-machine model. The mission produces an explicit, reusable definition of pointer-machine runs and accessibility together with a complete proof of the explicit bound. A formal model of this kind is the precondition for stating any other pointer-machine lower bound.

Difficulty

The statement must hold for every representation, including structures with many auxiliary nodes and arbitrary pointers between tree nodes. Arguing about one natural representation, such as parent pointers, where a leaf is far from its ancestors, says nothing about other representations: a structure with shortcut pointers or auxiliary nodes may bring some ancestors close to some leaves, and the bound must survive every such choice. In the formal setting the counting also has to handle overlaps: nodes reachable from several leaves, nodes that represent no vertex, and pointer cycles.

Formalization scope

• Model. Nodes form an arbitrary type N, not necessarily finite. ptr : N → Fin 2 → Option N gives the two pointer fields (none = nil), and rep : Vertex h → N is required to be injective. acc ptr j a is defined recursively. Run ptr a b t held is an inductive predicate for runs of $t$ steps, AnsweredIn asks for some run of at most $k$ steps holding the answer, and AnswersLeafQueriesIn ptr rep k requires this for every pair of leaves.
• Conventions.
  • Two pointer fields per node, as the paper's "without loss of generality" reduction allows; the reduction itself is not formalized.
  • Only queries on two leaves are assumed answerable. This is weaker than all queries, so the theorem is at least as strong as the paper's.
  • Time is counted as pointer-following steps. Mutation of the structure during a query and non-pointer fields are not modelled: neither lets the machine hold a node it has not reached by following pointers. The clause "the algorithm remembers nothing between queries" is built into the static structure.
  • Vertex h is {s : List Bool // s.length ≤ h}, nca is the longest common prefix, and a separate theorem identifies it with the Appendix's deepest common ancestor. $n = 2^h$ counts leaves, not vertices.
  • $\lg$ is Real.logb 2. For $h = 0$ Lean's $\log_2 0 = 0$ gives the true statement $k > -2$; for $h \ge 1$, $\lg\lg n = \log_2 h$.
  • Cardinalities in the milestones are Set.encard in $\mathbb N \cup \{\infty\}$, so finiteness is part of each claim. Divisions are cleared: $h\,2^h \le 2\sum_x |A_x|$.
• Ruling out trivial formalizations. The hypothesis AnswersLeafQueriesIn is satisfiable: the parent-pointer representation answers every leaf query in $h$ steps. If rep were not injective, a constant rep would answer every query in zero steps, so injectivity is kept in the goal. The milestones do not need it and do not assume it.
• Infrastructure. The goal needs finite-set counting over the leaves of the complete binary tree and a double count over heights. The run and accessibility definitions are reusable for other pointer-machine arguments. Proofs of the milestones, and of the ℕ form $h < 2^{k+2}$ that the goal reduces to, are welcome.

Selected references

• D. Harel, R. E. Tarjan, Fast Algorithms for Finding Nearest Common Ancestors, SIAM J. Comput. 13(2):338–355, 1984. https://doi.org/10.1137/0213024
• A. V. Aho, J. E. Hopcroft, J. D. Ullman, On finding lowest common ancestors in trees, SIAM J. Comput. 5(1):115–132, 1976. https://doi.org/10.1137/0205011
• A. Schönhage, Storage modification machines, SIAM J. Comput. 9(3):490–508, 1980. https://doi.org/10.1137/0209036
• R. E. Tarjan, A class of algorithms which require nonlinear time to maintain disjoint sets, J. Comput. System Sci. 18(2):110–127, 1979. https://doi.org/10.1016/0022-0000(79)90042-4

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