Motivation

Set covering asks for the fewest members of a family of sets whose union is everything the family covers. It models crew scheduling, facility siting, test-suite reduction, logic minimization and fault testing; Johnson names the last two as its practical applications. Karp showed in 1972 that the decision version is NP-complete (Karp 1972), so in practice one runs a heuristic and asks how far from optimal it can be.

David S. Johnson's 1974 paper Approximation Algorithms for Combinatorial Problems (JCSS 9, 256–278) is one of the founding papers of the worst-case analysis of approximation algorithms. For set covering it analyses the obvious greedy rule, repeatedly take a set that covers the most still-uncovered points, and proves that on families whose sets have at most $k$ elements its output is never more than the harmonic number $H(k) = \sum_{j=1}^k 1/j$ times the optimum, and that this factor is attained.

Timeline.

• 1974: Johnson proves the $H(k)$ bound for unweighted set cover with sets of size at most $k$, together with a matching family of examples (this mission).
• 1975: Lovász proves the same bound for the fractional relaxation, giving an integrality-gap statement (Lovász 1975).
• 1979: Chvátal extends the bound to weighted set cover, with the greedy rule choosing the set of least cost per newly covered point (Chvátal 1979).
• 1998: Feige shows that no polynomial-time algorithm achieves $(1-\varepsilon)\ln n$ unless NP has slightly superpolynomial deterministic algorithms (Feige 1998), so the greedy guarantee is essentially the best possible.

Setting

An input $F$ of SET COVERING I is a finite family $\{S_1, \dots, S_p\}$ of finite sets. The set to be covered is $T = \bigcup_{S \in F} S$. A subcover is a subfamily $F' \subseteq F$ with $\bigcup_{S \in F'} S = T$, and its measure is $|F'|$. The optimum $F^*$ is the minimum measure of a subcover; $F$ itself is a subcover, so the minimum exists. The subproblem SC(k) restricts the inputs to families no set of which has more than $k$ elements.

Algorithm C1 keeps a family SUB of chosen sets, the set UNCOV of uncovered points, and an array SET$[i]$ holding the still-uncovered part of $S_i$. It starts with SUB $= \emptyset$, UNCOV $= T$, SET$[i] = S_i$. While UNCOV is nonempty it chooses an index $j$ with $|\mathrm{SET}[j]|$ maximal, adds $S_j$ to SUB, and removes SET$[j]$ from UNCOV and from every SET$[i]$. When UNCOV is empty it returns SUB. When several indices tie at Step 3 any of them may be chosen, so one input can have several choosable outputs. Following Section 2 of the paper, the algorithm's value $C1(F)$ is the worst choosable output, here the largest, and the ratio is $r(C1, F) = C1(F)/F^*$.

For the proof the paper introduces configurations $K = \langle N_K, \mathrm{UNCOV}_K, \langle \mathrm{SET}_K[1], \dots, \mathrm{SET}_K[N_K]\rangle\rangle$ with $\bigcup_i \mathrm{SET}_K[i] = \mathrm{UNCOV}_K$, runs from a configuration (sequences of admissible choices ending when UNCOV is empty), $\mathrm{Numbers}(R)$, the set of indices chosen in a run $R$, and calls a set $M$ selectable from $K$ if $M = \mathrm{Numbers}(R)$ for some run $R$ from $K$. Write $n(K, i) = |\mathrm{SET}_K[i]|$.

Formalization targets

Goal: Theorem 4

For every $k \ge 1$:

$$\text{for every input } F \in SC(k) \text{ and every choosable } F_1:\quad |F_1| \le H(k)\cdot F^*,$$ $$\text{and some } F \in SC(k) \text{ with } F^* > 0 \text{ has a choosable } F_1 \text{ with } |F_1| = H(k)\cdot F^*.$$

The paper states this as $R[C1, SC(k)](n) \le \sum_{j=1}^k (1/j)$ for all $n > 0$, with equality for all sufficiently large $n$. The two-part form above is the size-free equivalent.

Milestones

1. Lemma 1. For a subcover $F_1$ with index set $M1 = \{i : S_i \in F_1\}$ and $K$ the configuration after Step 1: $F_1$ is choosable by C1 if and only if $M1$ is selectable from $K$.
2. Lemma 2. For any configuration $K$, any $M1$ selectable from $K$ and any $M0$ with $\bigcup_{i \in M0} \mathrm{SET}_K[i] = \mathrm{UNCOV}_K$:

$$|M1| \le \sum_{i \in M0} \sum_{j=1}^{n(K,i)} \frac{1}{j}.$$

3. Fig. 1. For every $k \ge 1$ there is an explicit input of $SC(k)$ on $k \cdot k!$ points with $F^* = k!$ and a choosable output of $k!\,H(k)$ sets.

Significance

The result. Theorem 4 is the first proof that greedy set cover has a worst-case guarantee depending only on the largest set size, and it pins the guarantee down exactly: the constant $H(k)$ cannot be lowered for any $k$. Since $H(k) \le 1 + \ln k$, it also gives the well-known $1 + \ln n$ bound for general inputs. The $H(k)$ bound and its later refinements are the standard reference point for analyses of greedy covering, dual fitting and submodular covering.

Formalizing it. The theorem has been proved since 1974. As far as a search of the platform shows, no machine-checked proof of it exists: the platform holds a Kearns–Vazirani-style statement ComputationalLearning.greedy_set_cover (the $\mathrm{opt}\cdot\ln|U|$ form for a greedy sequence, still open) and a dual-fitting certificate lemma for weighted set cover, neither of which covers the $SC(k)$ bound, the tie-breaking semantics or the tightness construction. A complete development provides both halves of Theorem 4, the configuration and run machinery of Lemmas 1–2, and the explicit Fig. 1 family.

Difficulty

The obvious argument charges each chosen set to the points it newly covers and compares the charges with an optimal cover. A statement about the initial input alone, with the original sizes of the optimal sets, does not survive a single greedy step: after a step the optimal sets are only partly uncovered and the remaining run faces a different instance. This is why Lemma 2 is stated for an arbitrary configuration, in terms of the current sizes $n(K, i)$, and for an arbitrary covering subfamily $M0$. Because Step 3 breaks ties arbitrarily, the statement must hold for every admissible run, and a formalization that fixes one tie-breaking rule proves a weaker upper bound and cannot express the tightness example, which relies on adversarial ties at every stage.

For the tightness half, the difficulty is bookkeeping: showing that the $k!/j$ blocks of each segment are admissible choices at each stage and that no cover uses fewer than $k!$ sets.

Formalization scope

• An input is an indexed family S : ι → Finset α over a finite index type ι and a ground type with decidable equality. The indices play the role of $1, \dots, N$; two indices may carry the same set, which only widens the input class. The family, subcovers and $F^*$ are taken over the set of sets family S, as on the page. $F^*$ is a Finset.inf' over the nonempty finite set of subcovers; if $T = \emptyset$ then $F^* = 0$.
• C1 is a nondeterministic step relation: a step is allowed for every index maximizing $|\mathrm{SET}[j]|$. An output is choosable if a finite chain of steps from the initial state reaches a halting state with that SUB. No tie-breaking rule is fixed.
• The paper's $R[A, P](n)$ is a maximum over inputs of size at most $n$ in an unspecified notation; it is replaced by the size-free two-part statement above, which is equivalent because $R$ is a maximum over finitely many inputs and nondecreasing in $n$.
• Ratios are stated multiplicatively in $\mathbb{Q}$ ($|F_1| \le H(k)\cdot F^*$), never as a quotient, so an input with $F^* = 0$ does not make the bound vacuous, and the attainment part requires $F^* > 0$. $H(k)$ is Mathlib's harmonic k.
• Configurations carry the covering condition as a field; runs are an inductive predicate on the list of chosen indices; Selectable K M means $M$ is the set of indices of some run.
• Lemma 1 assumes the family's sets are pairwise distinct (the paper's family is a set of sets); without that the index set $\{i : S_i \in F_1\}$ may contain a duplicate index C1 never chose.
• Trivializing formalizations are ruled out: a deterministic tie-break, a ratio written as a division, the original set sizes in place of $n(K, i)$ in Lemma 2, or an attaining input with $F^* = 0$ would each change the theorem.

Contributions welcome: proofs of Lemma 2 (the core induction), of Lemma 1, of the Fig. 1 run, and of Theorem 4 from these; the configuration/run layer and the Fig. 1 family are reusable for other greedy covering analyses.

Selected references

• David S. Johnson, Approximation algorithms for combinatorial problems, Journal of Computer and System Sciences 9 (1974), 256–278. https://doi.org/10.1016/S0022-0000(74)80044-9
• Richard M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972, 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9
• László Lovász, On the ratio of optimal integral and fractional covers, Discrete Mathematics 13 (1975), 383–390. https://doi.org/10.1016/0012-365X(75)90058-8
• Vašek Chvátal, A greedy heuristic for the set-covering problem, Mathematics of Operations Research 4 (1979), 233–235. https://doi.org/10.1287/moor.4.3.233
• Uriel Feige, A threshold of ln n for approximating set cover, Journal of the ACM 45 (1998), 634–652. https://doi.org/10.1145/285055.285059

Motivation

Many problems in scientific computing and statistics ask for a solution of a linear system $Ax\approx b$ that uses as few unknowns as possible. In statistics this is subset selection (Golub and Van Loan, Matrix Computations, 1983). In coding theory over binary matrices it is the minimum weight solution problem (Gallager, 1968). Natarajan's own motivation was radial basis interpolation (Hardy, 1988). There the coefficients of the interpolant solve a square nonsingular linear system (Michelli, 1986). Few nonzero coefficients make the interpolant cheap to evaluate and, by Occam's razor, less prone to fitting noise.

Natarajan's paper (SIAM J. Comput. 24 (1995) 227–234) makes two contributions. First, finding the sparsest approximate solution over the reals is NP-hard (Theorem 1, the subject of the companion mission). Second, the obvious greedy heuristic, a QR factorization whose column pivots are chosen by their correlation with the right-hand side, is provably good (Theorem 2). This mission formalizes Theorem 2. The greedy method is known today as orthogonal least squares (OLS), a variant of orthogonal matching pursuit. Natarajan's bound is among the earliest worst-case guarantees for this family of algorithms and is widely cited in the sparse approximation and compressed sensing literature.

Setting

Let $A\in\mathbb R^{m\times n}$ have columns $a_1,\dots,a_n$, let $b\in\mathbb R^m$ and $\varepsilon>0$. Write $\|\cdot\|_2$ for the Euclidean norm and $\|x\|_0$ for the number of nonzero entries of $x$. The sparse approximate solution problem asks for $x$ with $\|Ax-b\|_2\le\varepsilon$ and $\|x\|_0$ minimal. Define

$$\operatorname{Opt}(\delta)=\min\{\|x\|_0 : \|Ax-b\|_2\le\delta\}.$$

Let $\mathbf A$ be $A$ with every column divided by its Euclidean norm. Let $\mathbf A^+$ be its Moore–Penrose pseudo-inverse, the unique matrix $P$ with $\mathbf AP\mathbf A=\mathbf A$, $P\mathbf AP=P$ and $\mathbf AP$, $P\mathbf A$ symmetric. Let $\|\mathbf A^+\|_2$ be its spectral norm, the $\ell_2\to\ell_2$ operator norm.

Algorithm Greedy keeps a working matrix $A^{(r)}$ with columns $a^{(r)}_j$, a working vector $b^{(r)}$ and a set $\tau$ of chosen indices. It starts from $A^{(0)}=\mathbf A$, $b^{(0)}=b$, $\tau=\emptyset$. While $\|b^{(r)}\|_2>\varepsilon$, it chooses an index $k\notin\tau$ that maximizes $|a_k^{(r)T}b^{(r)}|$ and replaces $b^{(r)}$ by its projection onto the orthogonal complement of $a^{(r)}_k$. It adds $k$ to $\tau$ and replaces every column outside $\tau$ by its normalized projection onto that complement. If every correlation $a_j^{(r)T}b^{(r)}$ vanishes, the algorithm stops ("no solution exists"). A final solution phase solves the linear system $Bx=b^{(0)}-b^{(r)}$ in the chosen columns $B$ of $A$. The number of nonzero entries of the output is therefore at most the number $t$ of selection iterations.

Formalization targets

Goal: Theorem 2, for $A$ with linearly independent columns

If the columns of $A$ are linearly independent and some $x$ satisfies $\|Ax-b\|_2\le\varepsilon/2$, then every run of the selection phase, with any tie-breaking, performs

$$t\le\Big\lceil 18\,\operatorname{Opt}(\varepsilon/2)\,\|\mathbf A^+\|_2^2\,\ln\frac{\|b\|_2}{\varepsilon}\Big\rceil$$

iterations. The paper prints the theorem without the independence hypothesis. The hypothesis is needed (see Formalization scope).

Milestones

The proof on pp. 230–233 passes through the following statements, in order:

1. (12): some column satisfies $|a_j^{(r)T}b^{(r)}|\ge\|b^{(r)}\|_2^2/(2\sqrt{N^{(r)}}\|u^{(r)}\|_2)$. Here $u^{(r)}$ is a sparsest vector with $\|A^{(r)}u^{(r)}-b^{(r)}\|_2\le\varepsilon/2$ and $N^{(r)}=\|u^{(r)}\|_0$.
2. (18): $\|b^{(r+1)}\|_2^2\le(1-1/\rho)\|b^{(r)}\|_2^2$ whenever $\rho\ge 4N^{(r)}\|u^{(r)}\|_2^2/\|b^{(r)}\|_2^2$.
3. Lemma 1: $t\le\lceil2\rho\ln(\|b\|_2/\varepsilon)\rceil$ for any such $\rho$ valid at every iteration.
4. Lemma 3: $N^{(r+1)}\le N^{(r)}\le N^{(0)}$.
5. $N^{(0)}=\operatorname{Opt}(\varepsilon/2)$.
6. The columns of $\mathbf A$ indexed by the support $\sigma$ of $u^{(r)}$ and by the chosen set $\tau$ are linearly independent, and $\sigma\cap\tau=\emptyset$.
7. (31): $\|u^{(r)}\|_2\le\frac32\|Z^+\|_2\|b^{(r)}\|_2$ for the matrix $Z$ of those columns.
8. The singular-value comparison $\|Z^+\|_2\le\|M^+\|_2$ for a column submatrix $Z$ of a matrix $M$ with independent columns.
9. Lemma 2: $\|u^{(r)}\|_2\le\frac32\|\mathbf A^+\|_2\|b^{(r)}\|_2$, for $A$ with independent columns.

Items 1–7 hold for every matrix $A$. Items 8, 9 and the goal carry the independence hypothesis.

Significance

Theorem 2 is a bicriteria approximation guarantee for an NP-hard problem. The greedy output meets the error $\varepsilon$ with at most a factor $18\|\mathbf A^+\|_2^2\ln(\|b\|_2/\varepsilon)$ more nonzeros than the best solution at error $\varepsilon/2$. The factor depends only on the conditioning of the normalized matrix and logarithmically on the required accuracy. Its structure follows Johnson's analysis of the greedy set cover algorithm (1974): a potential decreases by a constant factor per step, which gives a logarithmic number of steps. The intermediate facts (12), (18) and Lemma 1 are the template of many later analyses of matching pursuit and OLS.

The result is proved on paper, with a gap. The last step of the proof of Lemma 2 compares singular values of a submatrix with those of $\mathbf A$, and this comparison holds only when $\mathbf A$ has full column rank. For general $A$, Theorem 2 and Lemma 2 are false as printed. The formalization produces a machine-checked proof of the corrected theorem and pins down exactly where the hypothesis enters. The hypothesis-free statements (12), (18), Lemma 1, Lemma 3 and (31) form reusable infrastructure for greedy sparse approximation. No existing formalization of this algorithm or of its guarantee, in Lean or elsewhere, was found for this mission.

Difficulty

Each step of the proof is short, but the objects are defined by an iteration. The columns $a^{(r)}_j$ are repeatedly projected and renormalized, and the columns already chosen are left untouched. Every claim about iteration $r$ therefore needs invariants: chosen columns are orthonormal and orthogonal to $b^{(r)}$, and the remaining columns are normalized projections of the original ones onto the orthogonal complement of the chosen ones. A proof has to establish these by induction before any lemma can be applied. The sparsest vector $u^{(r)}$ is defined by minimality, so Lemma 3 and the linear-independence claim are exchange arguments on supports rather than computations. Finally, the passage from (31) to Lemma 2 needs a quantitative fact about pseudo-inverses of column submatrices. Mathlib has neither the Moore–Penrose inverse of a rectangular matrix nor its norm as a reciprocal singular value.

A naive attempt to bound $\|u^{(r)}\|_2$ directly by $\|\mathbf A^+\|_2\|A^{(r)}u^{(r)}\|_2$ fails: $u^{(r)}$ multiplies the projected columns $A^{(r)}$, not $\mathbf A$, and different sparsest solutions can have different norms.

Formalization scope

Vectors live in EuclideanSpace ℝ (Fin m), so every $\|\cdot\|_2$ is the Euclidean norm. The only $\|\cdot\|_\infty$ is the maximum of $|a_j^{(r)T}b^{(r)}|$, which is written out explicitly. The algorithm is a recursion greedyState A b k r in the sequence of choices k : ℕ → Fin n. A run of $t$ iterations (IsGreedyRun) requires, at each $r<t$: the strict while-condition $\|b^{(r)}\|_2>\varepsilon$, an unchosen index, a nonzero correlation, and maximality over the unchosen columns. The residual and the columns are computed, never assumed. Normalization sends $0$ to $0$, so a column lying in the span of the chosen ones stays zero and is never chosen. $\operatorname{Opt}$ is an infimum over ℕ, and the goal assumes that some $x$ has $\|Ax-b\|_2\le\varepsilon/2$, since otherwise the infimum would be $0$. The ceiling is the natural-number ceiling. It agrees with the printed one whenever the loop runs at least once, because then $\|b\|_2>\varepsilon$. The pseudo-inverse is any matrix satisfying the four Penrose equations. It is never defined as $(\mathbf A^T\mathbf A)^{-1}\mathbf A^T$, which would hide the rank assumption.

Added hypothesis. The goal, Lemma 2 and the singular-value step assume that the columns of $A$ are linearly independent, which forces $n\le m$. Without it, Theorem 2 fails. Take $m=2$, $n=200$, columns $(\cos\theta_j,\sin\theta_j)$ and $(\sin\theta_j,\cos\theta_j)$ for 100 distinct $\theta_j\in[0.001,0.01]$, $b=\sqrt2(1,1)$ and $\varepsilon=1$. Then $\operatorname{Opt}(1/2)=2$ and the bound evaluates to $1$, but Greedy selects two columns. Lemma 2 fails for $\mathbf A=[e_1,e_2,(e_1+e_2)/\sqrt2]$ and $b=\beta(-1,1)/\sqrt2$. The paper's motivating interpolation systems are square and nonsingular, so they satisfy the hypothesis. A hypothesis-free goal would replace $\|\mathbf A^+\|_2$ by the largest $\|Z^+\|_2$ over linearly independent column subsets $Z$ of $\mathbf A$, which is what (31) gives. That quantity is not printed in the paper, so it is not the goal here.

A statement in which the iterates are free sequences constrained by hypotheses, the greedy choice is dropped, or $\operatorname{Opt}$ is taken over an empty set would be trivially true or would not describe this algorithm. The encoding above rules these out.

A complete development needs Gram–Schmidt-type invariants of the iteration, exchange arguments for sparsest solutions, and the Moore–Penrose inverse with its spectral norm. The last of these is reusable well beyond this mission. Contributions of any milestone, of the general Penrose-inverse facts, or of alternative proofs are welcome.

Selected references

• B. K. Natarajan, Sparse Approximate Solutions to Linear Systems, SIAM J. Comput. 24(2):227–234, 1995. https://doi.org/10.1137/s0097539792240406
• G. H. Golub and C. F. Van Loan, Matrix Computations, Johns Hopkins University Press, 1983.
• D. S. Johnson, Approximation algorithms for combinatorial problems, J. Comput. System Sci. 9:256–278, 1974. https://doi.org/10.1016/S0022-0000(74)80044-9
• R. Penrose, A generalized inverse for matrices, Proc. Cambridge Philos. Soc. 51:406–413, 1955. https://doi.org/10.1017/S0305004100030401

Motivation

Maximum satisfiability asks for a truth assignment satisfying as many clauses of a propositional formula as possible. The paper notes that the restriction $MS(k)$, in which every clause has at least $k$ literals, is polynomial complete for every $k \ge 1$, so exact optimization is out of reach in general and one asks instead how close a fast algorithm is guaranteed to come. David S. Johnson's 1974 paper Approximation Algorithms for Combinatorial Problems (J. Comput. System Sci. 9, 256–278) set up a framework for exactly this question — optimization problems, nondeterministic approximation algorithms, and the worst-case ratio between the optimum and the algorithm's output — and applied it to subset-sum, maximum satisfiability, set covering, graph coloring and maximum clique. It is one of the founding papers of the theory of approximation algorithms.

Section 4 of the paper treats maximum satisfiability with two algorithms. This mission covers the first, a greedy literal-selection rule called B1, and its exact worst-case ratio (Theorem 2). A companion mission covers the weighted algorithm B2 (Theorem 3).

Timeline, for orientation:

• 1971–1972: Cook and Karp establish NP-completeness of satisfiability and of many combinatorial problems.
• 1974: Johnson proves that B1 has worst-case ratio exactly $(k+1)/k$ on $MS(k)$ and that the weighted algorithm B2 achieves $2^k/(2^k-1)$ (Theorems 2 and 3).
• 1990s: semidefinite and LP-based algorithms (Goemans–Williamson, SIAM J. Discrete Math. 1994) improve the constants for general MAX-SAT.

Setting

Let $L = \bigcup_{i>0}\{x_i, \bar x_i\}$ be the set of literals; the complement of $x_i$ is $\bar x_i$ and conversely. A clause is a finite set $C \subseteq L$. A truth assignment is a set $T \subseteq L$ containing no complementary pair $\{x_i, \bar x_i\}$; it may leave variables unassigned. $T$ satisfies $C$ if $C \cap T \ne \emptyset$.

An input is a finite set $S$ of clauses. Its feasible solutions are the subsets $S' \subseteq S$ satisfied by a single truth assignment, measured by $|S'|$, and the optimum is

$$S^* = \max\{|S'| : S' \subseteq S,\ \text{some truth assignment satisfies every } C \in S'\}.$$

The subproblem $MS(k)$ admits only inputs whose clauses each contain at least $k$ distinct literals.

Algorithm B1 keeps four variables: SUB (clauses already satisfied), LEFT (clauses not yet satisfied), TRUE (literals made true) and LIT (literals still available). It starts with SUB $=$ TRUE $= \emptyset$, LEFT $= S$, LIT $= L$. While some literal of LIT occurs in a clause of LEFT, it picks a literal $y \in$ LIT contained in the most clauses of LEFT, moves those clauses $YT$ from LEFT to SUB, adds $y$ to TRUE, and removes $y$ and $\bar y$ from LIT. When no literal of LIT occurs in LEFT it returns SUB.

The choice of $y$ is not determined when several literals tie. Following the paper's framework, every output reachable by some sequence of admissible choices is choosable, and the performance of B1 on $S$ is the smallest $|X|$ over choosable outputs $X$. The worst-case ratio on inputs of size at most $n$ is

$$R[B1, MS(k)](n) = \max\{S^*/B1(S) : S \in MS(k),\ |S| \le n\}.$$

Formalization targets

Goal: Theorem 2 (p. 262)

For all $k \ge 1$,

$$R[B1, MS(k)](n) \le \frac{k+1}{k}\quad\text{for all } n > 0,$$

with equality for all sufficiently large $n$. In the size-free form used here: every choosable output $X$ on every $S \in MS(k)$ satisfies $k\,S^* \le (k+1)\,|X|$, and for every $k \ge 1$ some $S \in MS(k)$ has a choosable $X$ with $|X| > 0$ and $k\,S^* = (k+1)\,|X|$.

Milestones (from the proof of Theorem 2, pp. 262–263)

1. In each iteration, the number of clauses saved (added to SUB) is at least the number of clauses remaining in LEFT that are wounded (lose a literal from LIT without being satisfied).
2. When B1 halts, every clause left in LEFT is dead: each of its literals has had its complement made true.
3. When B1 halts on an input of $MS(k)$, $|\mathrm{SUB}| \ge k\,|\mathrm{LEFT}|$, and SUB and LEFT partition $S$.
4. On the four-clause input $\{\{x_1,x_2,x_3\},\{\bar x_1,x_4,x_5\},\{\bar x_2,x_6,x_7\},\{\bar x_3,x_8,x_9\}\}$ of $MS(3)$, $S^* = 4$ while B1 may return three clauses.

Significance

The bound is stronger than a ratio: milestone 3 shows that B1 always satisfies at least $\tfrac{k}{k+1}|S|$ clauses, whatever the optimum. The tightness half shows that this simple greedy rule cannot be analysed any better, which is what motivated the weighted algorithm B2 of the same section, with ratio $2^k/(2^k-1)$. The pair of theorems is an early instance of a now standard pattern: a potential-style counting argument for an upper bound, and an adversarial tie-breaking instance for the matching lower bound.

The result is proved in the paper; it has not, to our knowledge, been machine-checked. This mission produces a formal model of Johnson's framework for a maximization problem with a nondeterministic algorithm, a formal proof of the upper bound through the "saved versus wounded" accounting, and explicit tightness instances for every $k \ge 1$. The paper spells out only $k = 3$ and states that "similar examples can be constructed for any other $k > 0$"; the formal goal requires them for all $k$.

Difficulty

The upper bound needs an invariant over entire runs, not over a single step: a clause wounded in one iteration may be saved in a later one, so wounds and saves must be tallied globally, and the count of wounds received by a clause that ends in LEFT must be matched with its number of literals. That matching relies on the facts that B1 never makes both a literal and its complement true and that a clause containing a true literal has already left LEFT. Clauses containing both $x_i$ and $\bar x_i$ are allowed and have to be handled.

The lower bound cannot be obtained from a fixed tie-breaking rule: the attaining run chooses negative literals whose count merely ties the maximum. For general $k$ the instance has to be built so that every literal occurs in few enough clauses that the adversarial choice is admissible at every step; at $k = 1$ the paper's pattern degenerates and needs adjusting.

Formalization scope

• A literal is a pair (variable index in $\mathbb N$, sign); a clause is a Finset of literals; an input is a Finset of clauses, so duplicate clauses are not allowed, as on the page. Tautological clauses are allowed.
• A truth assignment is a Set of literals without a complementary pair (partial, as in the paper). $S^*$ is the maximum of $|S'|$ over the finite nonempty family of satisfiable subsets, taken with Finset.sup'.
• B1 is a nondeterministic run relation: a state holds SUB, LEFT, TRUE and the set of decided variables (LIT is its complement, since $L$ is infinite); one step chooses any literal of LIT, of either sign, with maximum count; "choosable" is reachability of a halting state with the given SUB. No tie-break is fixed. A formalization that picks a variable and then its better sign, or that resolves ties deterministically, is a different algorithm and would make the tightness half false.
• The ratio $R[B1, MS(k)](n)$, whose problem size is left unspecified in the paper, is replaced by its size-free equivalent, and ratios are written multiplicatively in $\mathbb N$: $k\,S^* \le (k+1)|X|$. The tightness half requires $|X| > 0$, so the empty input cannot witness it.
• The running time $O(n \log n)$ is not stated.

Welcome contributions: proofs of the milestones, the invariants of reachable B1 states (SUB and LEFT partition $S$; TRUE is consistent and exactly covers the decided variables; no clause of LEFT meets TRUE), and the family of tightness instances for general $k$. The run-relation encoding of choosable outputs is reusable for the other algorithms of the paper.

Selected references

• D. S. Johnson, Approximation algorithms for combinatorial problems, Journal of Computer and System Sciences 9 (1974), 256–278. https://doi.org/10.1016/S0022-0000(74)80044-9
• R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972, 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9
• M. X. Goemans and D. P. Williamson, New 3/4-approximation algorithms for the maximum satisfiability problem, SIAM Journal on Discrete Mathematics 7 (1994), 656–666. https://doi.org/10.1137/S0895480192243516

Motivation

David S. Johnson's 1974 paper Approximation Algorithms for Combinatorial Problems (J. Comput. System Sci. 9 (1974) 256–278) is one of the founding papers of the theory of approximation algorithms. It asks, for optimization problems whose decision versions Karp had just shown to be polynomial complete, how close a fast heuristic can be guaranteed to come to the optimum in the worst case, and it measures this with a worst-case performance ratio that is still the standard yardstick.

Its first example is SUBSET-SUM, the simplest form of the knapsack problem: pack items of given sizes into a knapsack of capacity $b$ so as to fill it as much as possible. For this problem the paper gives a family of algorithms $A_k$, one for each $k \ge 1$, whose guaranteed ratio $(k+1)/k$ tends to $1$. It is one of the first examples of what is now called a polynomial-time approximation scheme: for every $\epsilon > 0$ there is a polynomial-time algorithm within a factor $1 + \epsilon$ of optimal. Sahni (1975) extended the idea to the knapsack problem with utilities, and Ibarra and Kim (1975) later obtained fully polynomial schemes for knapsack and subset-sum.

This mission formalizes Theorem 1 of the paper, the performance guarantee of $A_k$ together with its tightness.

Setting

An input $\langle T, s, b\rangle$ of SUBSET-SUM is a finite set $T$, a positive rational size $s(x)$ for every $x \in T$, and a positive rational bound $b$. An approximate solution is a subset $T' \subseteq T$ with $m(T') \le b$, where the measure is $m(T') = \sum_{x \in T'} s(x)$. The problem is a maximization problem with optimal measure

$$\langle T, s, b\rangle^* = \max\{\, m(T') : T' \subseteq T,\ m(T') \le b \,\}.$$

Fix $k \ge 1$ and call $x$ big if $s(x) > b/(k+1)$ and small otherwise. Algorithm $A_k$ keeps a set $\mathrm{SUB}$, its measure $\mathrm{SUM}$, and the remaining elements $\mathrm{LEFT}$:

1. $\mathrm{SUB}$ is a subset of the big elements whose measure is as large as possible without exceeding $b$; $\mathrm{SUM} = m(\mathrm{SUB})$ and $\mathrm{LEFT} = T \setminus \mathrm{SUB}$.
2. If $s(x) + \mathrm{SUM} > b$ for every $x \in \mathrm{LEFT}$, return $\mathrm{SUB}$.
3. Otherwise pick $y \in \mathrm{LEFT}$ with $s(y) + \mathrm{SUM}$ as large as possible without exceeding $b$, move it from $\mathrm{LEFT}$ to $\mathrm{SUB}$, add $s(y)$ to $\mathrm{SUM}$, and return to step 2.

Steps 1 and 3 may have ties. Following the paper, a set $T_1$ is choosable by $A_k$ if some resolution of all ties produces it, and the performance $A_k(u)$ on input $u$ is the smallest measure of a choosable output. The ratio is $r(A_k, u) = u^*/A_k(u) \ge 1$, and $R[A_k](n)$ is its maximum over inputs of size at most $n$.

Formalization targets

Goal: Theorem 1 (p. 260)

For $k \ge 1$ and $n > 0$,

$$R[A_k](n) \le \frac{k+1}{k}, \qquad \lim_{n \to \infty} R[A_k](n) = \frac{k+1}{k}.$$

Formally, for every $k \ge 1$: every choosable output $T_1$ of every input satisfies $k\,\langle T,s,b\rangle^* \le (k+1)\,m(T_1)$; and for every $\delta > 0$ some input has a choosable output $T_1$ with $m(T_1) > 0$ and $\langle T,s,b\rangle^* > \big(\tfrac{k+1}{k} - \delta\big)\,m(T_1)$.

Milestones

1. For $T_1$ choosable and $T_0$ any approximate solution, $m(T_1^{\mathrm{BIG}}) \ge m(T_0^{\mathrm{BIG}})$ (p. 260).
2. If a small $x \in T$ is not in a choosable $T_1$, then $s(x) + m(T_1) > b$, hence $m(T_1) > kb/(k+1) \ge \tfrac{k}{k+1}\langle T,s,b\rangle^*$ (p. 261).
3. The stronger dichotomy: $m(T_1) = \langle T,s,b\rangle^*$ or $m(T_1) \ge \tfrac{k}{k+1}\,b$ (p. 260).
4. The lower-bound input $T = \{a_1,\dots,a_{k+2}\}$, $s(a_1) = 1+\varepsilon$, $s(a_i) = 1$ otherwise, $b = k+1$: its optimum is $k+1$, some output is choosable, and every choosable output has measure $k + \varepsilon$ (p. 261).

Significance

Theorem 1 shows that SUBSET-SUM admits polynomial-time algorithms with any worst-case ratio above $1$, in contrast with the other problems of the paper (set covering, graph colouring, maximum clique), whose best known ratios grow with the input. The algorithms $A_k$ are an early instance of the partial-enumeration schemes later used for knapsack-type problems. The tightness half shows that the analysis of $A_k$ itself cannot be sharpened.

The theorem has a short published proof, but no machine-checked version is known; there is no subset-sum or knapsack approximation result on the platform. The mission produces a reusable model of SUBSET-SUM, a model of nondeterministic algorithms through a run relation that captures every tie-break, and a checked proof that the worst case is exactly $(k+1)/k$. The same modelling pattern (choosable outputs, worst-case ratio taken over them) is used in the sibling missions of this series for MAX-SAT, set covering and exact covering.

Difficulty

The arithmetic of the upper bound is short; the difficulty is in reasoning about the algorithm as a nondeterministic process. The natural first attempt, implementing $A_k$ as a function with a fixed tie-breaking rule, proves a weaker statement: the guarantee must hold for every output the algorithm may return, including adversarial ties in step 1 (several maximum-measure sets of big elements) and step 3. Facts that are obvious for a single run, such as $\mathrm{SUM}$ always equalling $m(\mathrm{SUB})$ or which elements can enter $\mathrm{SUB}$ after step 1, have to be established for the run relation as a whole. The lower bound requires tracing the run on the explicit input for general $k$: exactly $k-1$ unit elements are added after $a_1$, and this must be shown for every choosable run, not only for one.

Formalization scope

• Numbers. Sizes and the bound are rationals (ℚ), as in the paper; sizes are required to be positive on $T$ and $b > 0$. The index $k$ is a natural number with $1 \le k$ as a hypothesis; $b/(k+1)$ is rational division, and "big" is the strict inequality $s(x) > b/(k+1)$.
• Optimum. opt u is Finset.sup' of the measure over the finite set of approximate solutions, which always contains $\emptyset$; it is $0$ when no element fits.
• Run relation. Choosable k u T₁ states that some admissible step 1 choice, followed by a finite chain of admissible iterations (Relation.ReflTransGen), reaches a halting state returning $T_1$. Every "closest to, without exceeding" is an existential choice among all maximizers.
• Size-free restatement. The paper's input size $|u|$ ("in some standard notation") is never fixed, so the goal quantifies over all inputs instead of over sizes. The upper bound for all choosable outputs is equivalent to $R[A_k](n) \le (k+1)/k$ for all $n$; since $R[A_k]$ is nondecreasing, the limit claim is equivalent to the supremum of the ratio over all inputs being $(k+1)/k$, which is the second part.
• Multiplicative ratios. No ratio is written as a division, so an output of measure $0$ cannot satisfy a bound vacuously; the lower-bound part requires $m(T_1) > 0$. The value $(k+1)/k$ is not claimed to be attained: the paper's family has ratio $(k+1)/(k+\varepsilon)$.
• Lower-bound input. A def on Fin (k + 2) exactly as on the page, with $0 < \varepsilon < 1$ (the page leaves the range implicit; $\varepsilon < 1$ keeps $a_1$ the only big element that fits when $k = 1$).
• Ruled out. A formalization with a deterministic tie-break, with a bound of the form $\mathrm{opt}/m \le c$ in a field where $x/0 = 0$, or with tightness for a single fixed $k$ would be trivial or weaker; none of these is the target.

Contributions welcome: proofs of the milestones and the goal, invariant lemmas for the run relation, and further sanity checks on small inputs. The running-time remark ($O(n^k)$ for step 1) and Sahni's knapsack extension are not part of the mission.

Selected references

• D. S. Johnson, Approximation algorithms for combinatorial problems, Journal of Computer and System Sciences 9 (1974) 256–278. https://doi.org/10.1016/S0022-0000(74)80044-9
• S. Sahni, Approximate algorithms for the 0/1 knapsack problem, Journal of the ACM 22 (1975) 115–124. https://doi.org/10.1145/321864.321873
• O. H. Ibarra, C. E. Kim, Fast approximation algorithms for the knapsack and sum of subset problems, Journal of the ACM 22 (1975) 463–468. https://doi.org/10.1145/321906.321909
• R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum (1972) 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9

Motivation

A single machine must process a set of jobs, each with a processing time and a due-date, and a job that finishes after its due-date is late. Counting late jobs is the natural objective when a late order is simply lost, whatever its lateness. In the three-field notation of scheduling theory this is the problem $1\,\|\,\sum U_j$, and it is one of the few single-machine problems with a due-date objective that a simple greedy rule solves exactly.

J. Michael Moore gave that rule in 1968 (Management Science 15(1):102–109). The only exact method previously available was the Held–Karp dynamic program, which is exponential in the number of jobs. Moore's algorithm is two sorts plus at most $n(n+1)/2$ additions and comparisons. The rule, and the variant from the paper's Author's Supplement (credited to T. J. Hodgson and today called the Moore–Hodgson algorithm), is in every scheduling textbook, for example Brucker, Scheduling Algorithms, Ch. 4, and is the base case of later work on weighted and release-date variants.

Timeline:

• 1955: J. R. Jackson shows that a job set can be scheduled with no late job if and only if the earliest-due-date order has none (Management Science Research Project report 43, UCLA).
• 1968: Moore publishes the algorithm and its proof of optimality, with Hodgson's variant stated without proof.
• 1970s onward: the weighted version $1\,\|\,\sum w_jU_j$ is shown NP-hard (Karp 1972, via knapsack), and $1\,|\,r_j\,|\,\sum U_j$ likewise (Lenstra, Rinnooy Kan and Brucker 1977), so Moore's greedy rule does not extend to them.

Setting

A finite set $J$ of jobs is given. Job $j$ has a processing time $t_j \ge 0$ and a due-date $D_j$, and the paper assumes $t_j \le D_j$ for every job (a job that cannot finish on time even if started at time $0$ is removed beforehand). The machine starts at time $0$ and processes the jobs one after another, without idle time or preemption.

A schedule $S$ of $J$ is an ordering $(J_{i_1},\dots,J_{i_n})$ of all jobs of $J$. The job in position $k$ completes at $C_{i_k} = t_{i_1} + \dots + t_{i_k}$. The late set is $L = \{J_i : C_i > D_i\}$ and the early set is $E = \{J_i : C_i \le D_i\}$. A schedule is optimal if no schedule of $J$ has fewer late jobs. $A$ and $R$ denote the early and late jobs of $S$, each kept in their order in $S$.

Moore's algorithm works on a current sequence and a list of rejected jobs.

• Step 1: order the jobs by non-decreasing processing time (the shortest processing time rule).
• Step 2: find the first late job $J_{i_q}$ of the current sequence. If there is none, stop.
• Step 3: re-order $J_{i_1},\dots,J_{i_q}$ by non-decreasing due-date. If all of them are then early, keep the re-ordered sequence. Otherwise reject $J_{i_q}$ and remove it. Return to Step 2.

The output is the final current sequence sorted by due-dates, followed by the rejected jobs in any order.

In Lean, a schedule is IsSchedule J l, the late set is lateSet t D l, optimality is IsOptimal t D J l, $A$ and $R$ are earlyPart/latePart, and one pass of Steps 2–3 is the relation MooreStep t D, all in the namespace MooreLateJobs.NumLate.

Formalization targets

Goal: Moore's algorithm is optimal (The Algorithm, Step 2, p. 103)

Let $l_0$ be a shortest-processing-time schedule of $J$, and let a run of MooreStep from $(l_0,[\,])$ reach a state $(\mathrm{cur},\mathrm{rej})$ in which $\mathrm{cur}$ has no late job. Then for every due-date ordering $A_D$ of $\mathrm{cur}$ and every ordering $P$ of $\mathrm{rej}$,

$$(A_D,\,P)\ \text{is an optimal schedule for } J.$$

All tie-breaks in both sorts are covered.

Milestones

In attack order:

1. Lemma 1 (p. 105): every optimal schedule has the same number of late jobs as $(A,R)$ and as every $(A,P)$.
2. Jackson's lemma (p. 105).
3. Lemma 2 (p. 105): re-ordering $A$ by due-dates keeps an optimal $(A,R)$ schedule optimal.
4. Lemma 3 (p. 105): a job that is late in some optimal schedule can be removed and appended.
5. The repeated-elimination claim (p. 106): after removing jobs late in successive optimal schedules until the rest is feasible, $(A_D,P)$ is optimal.
6. Cases 2) and 3) of the Selection Algorithm (p. 107): in either case the job $J_q$ is late in some optimal schedule.
7. Progress and termination of the algorithm (p. 108).

A companion item states the p. 104 remark that the final current sequence need not be re-sorted: $(\mathrm{cur},P)$ is already optimal.

Significance

The theorem shows that the minimum number of late jobs on one machine can be found in $O(n\log n)$ time, by a rule that also produces an optimal schedule of a very particular shape: due-date ordered early jobs first, then the late jobs in any order. Lemma 3's decomposition, that jobs late in some optimal schedule may be discarded one at a time, is the template reused for many related greedy results in scheduling.

The result is classical and fully proved on paper. To our knowledge no machine-checked proof of Moore's algorithm, of the Moore–Hodgson variant, or of Jackson's rule exists in Mathlib. This mission produces a checked proof of the algorithm as stated in the paper, with every tie-break allowed, together with reusable single-machine objects (schedules as lists, completion times, late sets) and Jackson's earliest-due-date feasibility lemma.

Difficulty

Neither ordering rule works alone. Sorting by due-dates alone gives a schedule with no late job whenever one exists, but it can make many jobs late once any must be. Keeping the shortest jobs first does not respect the due-dates at all. The step that fails in a direct greedy argument is the claim that the specific job $J_{i_q}$, the one just found late, belongs to the late set of some optimal schedule. That job is not in general the longest job of the prefix, and the paper has to treat separately the two cases in which it is rejected. On top of this, the algorithm re-sorts prefixes on the fly, so the claim has to be tied to the invariants of the run: the prefix is early and due-date sorted, and the jobs after it are at least as long as $J_{i_q}$.

Formalization scope

• Jobs and times. Jobs form a type ι with decidable equality; $J$ is a Finset ι; $t, D : ι \to \mathbb{R}$.
• Standing hypotheses. Every statement that involves schedules assumes $t_j \ge 0$ and $t_j \le D_j$ on $J$. The first is added: processing times are durations, and Jackson's lemma fails for negative times. The second is the paper's assumption on p. 102.
• Schedules and completion times. A schedule is a duplicate-free list with exactly the jobs of $J$. Positions are 0-based, and the job in position $k$ completes at the sum of the first $k+1$ processing times. Lateness is strict ($C_j > D_j$).
• Optimality compares against every schedule of the same job set.
• Ties. Orderings "by due-dates" and "by processing times" are List.Pairwise with ≤. Ties are arbitrary, and every statement quantifies over all such orderings.
• The algorithm. Steps 2–3 are the relation MooreStep. The re-ordered prefix is any due-date sorted permutation of the first $q+1$ jobs, and case 2) rejects the first late job $J_{i_q}$ itself, not the longest job of the prefix (that is Hodgson's variant). A run is Relation.ReflTransGen.

The goal must concern runs of this step relation from a shortest-processing-time schedule of $J$. Replacing the run by an arbitrary set of rejected jobs satisfying invariants would state a different theorem. The goal is not vacuous: the progress and termination milestones show that a terminal state is always reached.

Contributions are welcome at every level. Useful ones include general lemmas on completion times under permutation and filtering of lists, a proof of Jackson's lemma, proofs of the Selection Algorithm cases, and a proof of Hodgson's variant.

Selected references

• J. M. Moore, An n Job, One Machine Sequencing Algorithm for Minimizing the Number of Late Jobs, Management Science 15(1):102–109, 1968. https://doi.org/10.1287/mnsc.15.1.102
• J. R. Jackson, Scheduling a Production Line to Minimize Maximum Tardiness, Research Report 43, Management Science Research Project, UCLA, 1955.
• M. Held and R. M. Karp, A Dynamic Programming Approach to Sequencing Problems, J. SIAM 10(1):196–210, 1962. https://doi.org/10.1137/0110015
• R. M. Karp, Reducibility among Combinatorial Problems, in Complexity of Computer Computations, 1972. https://doi.org/10.1007/978-1-4684-2001-2_9
• J. K. Lenstra, A. H. G. Rinnooy Kan and P. Brucker, Complexity of Machine Scheduling Problems, Annals of Discrete Mathematics 1:343–362, 1977. https://doi.org/10.1016/S0167-5060(08)70743-X
• P. Brucker, Scheduling Algorithms, 5th ed., Springer, 2007. https://doi.org/10.1007/978-3-540-69516-5

Motivation

The nearest common ancestor problem asks, for a rooted tree and two of its vertices $v$ and $w$, for the deepest vertex that is an ancestor of both, written $\operatorname{nca}(v,w)$. It is a subroutine in string and graph algorithms.

Harel and Tarjan (Fast Algorithms for Finding Nearest Common Ancestors, SIAM J. Comput. 13, 1984) preprocess a static tree of $n$ vertices in linear time on a random-access machine so that each query takes constant time. For a complete binary tree the queries reduce to bit arithmetic on vertex numbers (§3). An arbitrary tree is first reduced, in §4, to a compressed tree $C$ whose sizes double along every edge, and $C$ is cut by rank into three plies. Lemma 9 bounds the size of each ply, and those bounds are what make the tables of the method fit in linear space. This mission formalizes the structural lemmas of §4 about $C$ and Lemma 9.

Timeline.

• 1976: Aho, Hopcroft and Ullman give an $O(\log\log n)$-per-query random-access algorithm for static trees.
• 1979: Tarjan (Applications of path compression on balanced trees, J. ACM 26) uses the decomposition of a tree by the doubling rule on subtree sizes to compute functions on paths; Lemmas 5–7 of Harel–Tarjan are cited from there without proof.
• 1983: Sleator and Tarjan (A data structure for dynamic trees, J. Comput. System Sci. 26) use the same heavy/light split of edges for dynamic trees.
• 1984: Harel and Tarjan give the $O(n)$-preprocessing, $O(1)$-query algorithm, with the compressed tree and its plies (§4).

Setting

A rooted tree $T$ (Appendix, p. 354) consists of a finite vertex set $V$ with $n = |V|$, a root $r \in V$ and a parent map $p_T$, defined for $v \ne r$, such that every vertex reaches $r$ by iterating $p_T$. The edges of $T$ are the pairs $v \to p_T(v)$ for $v \ne r$. If $p_T^i(v) = w$ for some $i \ge 0$, then $v$ is a descendant of $w$ and $w$ an ancestor of $v$. Every vertex is its own ancestor and descendant. The depth of $v$ is the number of edges from $v$ to $r$. $\mathrm{size}_T(v)$ is the number of descendants of $v$, including $v$.

An edge $v \to p_T(v)$ is light if $2\cdot\mathrm{size}_T(v) \le \mathrm{size}_T(p_T(v))$ and heavy otherwise. At most one heavy edge enters each vertex, so the heavy edges partition $V$ into heavy paths. A vertex with no heavy edge entering or leaving it forms a heavy path by itself. The apex of a heavy path is its vertex of smallest depth, and $\mathrm{apex}(v)$ denotes the apex of the heavy path containing $v$.

The compressed tree $C$ has the same vertices and root as $T$, and its edges are

$$\{\, v \to \mathrm{apex}(p_T(v)) : v \ne r \,\}.$$

Write $p_C(v) = \mathrm{apex}(p_T(v))$, and let $\mathrm{size}_C(v)$ be the number of descendants of $v$ in $C$. The rank of $v$ is $\mathrm{rank}(v) = \lfloor \lg \mathrm{size}_C(v)\rfloor$, where $\lg = \log_2$. Let $\lg^{(i)}$ denote the $i$-fold iterate of $\lg$. Ply three is the set of vertices of rank at least $\lfloor\lg^{(2)} n\rfloor$. Ply two is the set of vertices whose rank lies between $\lfloor\lg^{(3)} n\rfloor$ and $\lfloor\lg^{(2)} n\rfloor - 1$, inclusive. Ply one is the set of vertices of rank below $\lfloor\lg^{(3)} n\rfloor$.

Formalization targets

Goal: Lemma 9 in the explicit form of its proof

For every rooted tree on $n \ge 4$ vertices:

$$|\text{ply three}| \le \frac{4n}{\lg n}, \qquad |\text{ply two}| \le \frac{4n}{\lg^{(2)} n},$$

and for every vertex $v$ in ply one, every $C$-descendant of $v$ lies in ply one and $\mathrm{size}_C(v) \le \lg^{(2)} n$.

The paper states the first two bounds as $O(n/\log n)$ and $O(n/\log^{(2)} n)$. The constants $4$ and $4$ are the ones its proof on p. 345 establishes. The third clause is the paper's "each connected component of ply one is a subtree of $C$ containing at most $\log^{(2)} n$ vertices", read vertex by vertex. Ply one is closed under $C$-descendants, so the component of a ply-one vertex is the $C$-subtree of its shallowest ply-one ancestor.

Milestones

1. Lemma 5 (p. 344): $\mathrm{size}_C(v) = \mathrm{size}_T(v)$ if $v$ is an apex, and $\mathrm{size}_C(v) = 1$ otherwise.
2. Lemma 6 (p. 344): $2\cdot\mathrm{size}_C(v) \le \mathrm{size}_C(p_C(v))$ for every $v \ne r$.
3. Lemma 8 (p. 344): for every $i$, at most $n/2^i$ vertices have rank $i$.
4. Proof of Lemma 9, first sentence (p. 345): at most $n/2^{k-1}$ vertices have rank $k$ or greater.

A further item states Lemma 7 (p. 344): $C$ has depth at most $\lfloor\lg n\rfloor$. The paper uses it to bound the tables of ply three, not in the proof of Lemma 9.

Significance

Lemma 9 is the counting step of the linear-time preprocessing. Ply three has $O(n/\log n)$ vertices, each with $O(\log n)$ ancestors in $C$ by Lemma 7, so storing every vertex's ply-three ancestors takes $O(n)$ space. Ply two has $O(n/\log^{(2)} n)$ vertices, each with $O(\log^{(2)} n)$ ply-two ancestors, which again gives $O(n)$. Ply one splits into subtrees of at most $\lg^{(2)} n$ vertices, and these are small enough to be embedded in complete binary trees and answered by the bit arithmetic of §3.

Lemmas 5–8 and the proof of Lemma 9 are proved or cited in the paper, and none of them is open. As far as a search of the platform shows, none has a machine-checked proof, and Mathlib has no parent-map rooted trees, subtree sizes or heavy-path decompositions. The mission produces a reusable formal account of heavy paths and of the size-doubling compressed tree, with the paper's explicit constants.

Difficulty

The paper states Lemmas 5–7 without proof, citing Tarjan (1979). Lemma 5 requires identifying the $C$-descendants of an apex with its $T$-descendants. That identification needs a clean description of heavy paths: at most one heavy edge enters each vertex, a vertex's heavy path runs up to its apex, and the heavy paths do not overlap. Lemma 8 needs the observation that two vertices of equal rank are unrelated in $C$, so that their descendant sets are disjoint and the sizes add up to at most $n$. Lemma 9 turns floors of iterated real logarithms into bounds on powers of two. The step $2^{\lfloor \lg^{(2)} n\rfloor} > \tfrac12 \lg n$ loses a factor $2$, and this is where the constant $4$ comes from; a proof that expects the constant $2$ fails at this step.

Formalization scope

• Trees. A rooted tree is a structure over a Fintype vertex type $V$ with a root, a total parent map and the axiom that every vertex reaches the root. The paper's partial map is made total by $p_T(r) = r$. Every statement about an edge $v \to p(v)$ assumes $v \ne r$, since for $v = r$ Lemma 6 would read $2n \le n$. The Appendix's printed "$p^0(v) = 0$" is read as $p^0(v) = v$.
• Heavy edges and apex. A heavy edge is $v \ne r$ with $\mathrm{size}_T(p_T(v)) < 2\,\mathrm{size}_T(v)$, the strict negation of light. $\mathrm{apex}(v)$ is computed by climbing heavy edges from $v$ until the first edge that is not heavy, which is the apex of the heavy path containing $v$. The root is always an apex.
• Compressed tree. $p_C(v) = \mathrm{apex}(p_T(v))$ for $v \ne r$ and $p_C(r) = r$. Ancestors and sizes in $C$ are defined through iterates of $p_C$.
• Logarithms. The rank is Nat.log 2 of $\mathrm{size}_C$, which is exactly $\lfloor\lg\mathrm{size}_C\rfloor$. The ply thresholds are iterated Nat.log 2, which equal the real floors $\lfloor\lg^{(2)} n\rfloor$ and $\lfloor\lg^{(3)} n\rfloor$ for $n \ge 4$. The bounds of the goal use Real.logb 2.
• Added hypothesis $n \ge 4$ in the goal. It makes $\lg n \ge 2$ and $\lg^{(2)} n \ge 1$, so the divisions are honest (Lean's $x/0 = 0$), and it makes $\lg^{(3)} n \ge 0$. On the page it is hidden in the $O(\cdot)$.
• Division-free milestones. Lemma 8 is stated as $\#\{\mathrm{rank} = i\}\cdot 2^i \le n$, and the rank-$\ge k$ count as $\#\{\mathrm{rank} \ge k\}\cdot 2^k \le 2n$.
• Ruled out. The goal is not an $\exists C$ statement. Replacing the paper's $4$ by an existential constant, or bounding ply three by $n$, would discard the content of the lemma.
• Welcome contributions. A library of facts about heavy paths is welcome: uniqueness of the entering heavy edge, apex characterizations, and the descendants of an apex in $C$. So are proofs of Lemmas 5–8 and proofs that the iterated Nat.log thresholds agree with the real ones. It is reusable for heavy-light decompositions generally.

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
• R. E. Tarjan, Applications of path compression on balanced trees, J. ACM 26(4):690–715, 1979. https://doi.org/10.1145/322154.322161
• 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
• D. D. Sleator, R. E. Tarjan, A data structure for dynamic trees, J. Comput. System Sci. 26(3):362–391, 1983. https://doi.org/10.1016/0022-0000(83)90006-5