Linear algebra

Motivation

Linear recurrences with constant coefficients are among the first tools of enumerative combinatorics and the analysis of algorithms: the Fibonacci numbers, the number of binary strings avoiding a pattern, the running time of a divide-and-conquer loop and the number of tilings of a strip all satisfy relations of the form $c_0 a_{n+k} + c_1 a_{n+k-1} + \cdots + c_k a_n = 0$. Chapter 9 of Keller and Trotter's Applied Combinatorics (appliedcombinatorics.org) treats such relations as linear equations in an operator, the advancement operator, in direct analogy with linear differential equations with constant coefficients. The chapter's Principal Theorem says that the solution set of such an equation is a vector space whose dimension equals the order of the recurrence; everything else in the chapter (general solutions for distinct and repeated roots, and the reduction of nonhomogeneous equations to homogeneous ones) is organised around it.

This mission formalizes that theorem, in the book's model of functions on all of $\mathbb{Z}$, together with the numbered lemmas of Section 9.5 on which its outline rests.

Setting

Let $V$ be the real vector space of all functions $f : \mathbb{Z} \to \mathbb{R}$, with pointwise addition and scalar multiplication. The advancement operator $A : V \to V$ is

$$A f(n) = f(n+1) \qquad (n \in \mathbb{Z}),$$

a linear operator with $A^p f(n) = f(n+p)$ for $p \ge 0$. For a nonnegative integer $k$ and real constants $c_0, c_1, \dots, c_k$, the advancement operator polynomial is

$$p(A) = c_0 A^k + c_1 A^{k-1} + c_2 A^{k-2} + \cdots + c_k,$$

so that $p(A) f(n) = c_0 f(n+k) + c_1 f(n+k-1) + \cdots + c_k f(n)$. The solution space of the homogeneous equation $p(A) f = 0$ is

$$W = \{ f \in V : p(A) f = 0 \},$$

the kernel of $p(A)$, a linear subspace of $V$. In Lean, $A$ is AppliedComb.Recurrence.advance : Module.End ℝ (ℤ → ℝ), $p(A)$ is opPoly k c for a coefficient vector c : Fin (k + 1) → ℝ with c i multiplying $A^{k-i}$, and $W$ is solutionSpace k c := LinearMap.ker (opPoly k c). A factor $A - r$ is advance - r • 1.

Formalization targets

Goal: Theorem 9.18 (the Principal Theorem)

For a positive integer $k$ and real constants $c_0, \dots, c_k$ with $c_0 \neq 0$ and $c_k \neq 0$,

$$\dim_{\mathbb{R}} \{ f : \mathbb{Z} \to \mathbb{R} \;:\; (c_0 A^k + c_1 A^{k-1} + \cdots + c_k) f = 0 \} = k.$$

Milestones

1. Lemma 9.19. If $r \neq 0$ and $(A - r) f = 0$, then $f(n) = f(0)\, r^n$ for every $n \in \mathbb{Z}$.
2. Lemma 9.20. If $c_0, c_k \neq 0$, $g \in V$ is arbitrary and $p(A) f_0 = g$, then every solution of $p(A) f = g$ is $f = f_0 + f_1$ with $f_1 \in W$.
3. Theorem 9.21. If $r_1, \dots, r_k$ are distinct nonzero reals, every solution of $(A - r_1)(A - r_2)\cdots(A - r_k) f = 0$ has the form

$$f(n) = c_1 r_1^n + c_2 r_2^n + \cdots + c_k r_k^n \qquad (n \in \mathbb{Z}).$$

4. Lemma 9.22. If $k \ge 1$ and $r \neq 0$, then $(A - r)^k f = 0$ holds exactly when

$$f(n) = c_1 r^n + c_2 n r^n + c_3 n^2 r^n + \cdots + c_k n^{k-1} r^n \qquad (n \in \mathbb{Z})$$

for some real constants $c_1, \dots, c_k$.

Significance

The result itself. Theorem 9.18 is what justifies the standard recipe for solving a recurrence: once $k$ linearly independent solutions are found, every solution is a linear combination of them, and $k$ initial values pin down a unique solution. Theorems 9.21 and 9.22 name those $k$ solutions when the characteristic polynomial splits over $\mathbb{R}$, and Lemma 9.20 reduces nonhomogeneous recurrences, the ones arising from counting problems with a forcing term, to one particular solution plus the homogeneous space.

Formalizing it. The book states Theorem 9.18 without a full proof ("we won't prove the full result") and leaves Lemma 9.22 as an exercise, so a formalization supplies arguments the source omits. Mathlib's LinearRecurrence develops the $\mathbb{N}$-indexed, monic version (LinearRecurrence.solSpace_rank); the bi-infinite, two-sided setting of the book, in which the constant term $c_k$ must be nonzero, is not in Mathlib or on the platform as of this mission.

Difficulty

The subspace part of Theorem 9.18 is immediate; the content is the dimension count, in both directions. On $\mathbb{Z}$ a solution must extend to negative indices as well as positive ones, so an argument that works for sequences indexed by $\mathbb{N}$ does not transfer: there the constant term plays no role and the dimension is $k$ whatever the constant term, while on $\mathbb{Z}$ a vanishing $c_k$ changes the answer. The outline in the book proceeds through factorisations of $p(A)$, which over $\mathbb{R}$ need not exist (complex roots), so the goal cannot be obtained by combining Theorems 9.21 and 9.22 alone. Lemma 9.22 requires showing that the functions $n^j r^n$ solve $(A - r)^k f = 0$ and that they exhaust its solutions, for $n$ ranging over all integers.

Formalization scope

• Functions are $\mathbb{Z} \to \mathbb{R}$ (the real space $V$ of Section 9.5, p. 199), not $\mathbb{N} \to \mathbb{R}$ and not $\mathbb{Z} \to \mathbb{C}$. Powers $r^n$ with $n$ negative are integer powers (zpow), always of a nonzero base.
• Dimension in the goal is Module.rank ℝ (solutionSpace k c) = k, a cardinal equality, so it also asserts finite-dimensionality.
• The coefficient vector is c : Fin (k + 1) → ℝ; c 0 is the leading coefficient $c_0$ and c (Fin.last k) the constant term $c_k$.
• Theorem 9.21 asserts one inclusion, as on the page ("every solution has the form"); Lemma 9.22 asserts both ("the general solution"), as an iff.
• Lemma 9.22 carries the hypothesis $r \neq 0$, the standing assumption of Section 9.5.2 (p. 200), which the lemma's own sentence does not repeat.
• No O(·), "≈" or unspecified threshold occurs in these statements, so no explicit constant is instantiated.
• Ruling out the trivial reading: $W$ is defined as the kernel of the operator polynomial $p(A)$, never as the span of $k$ chosen functions, so the goal is not a statement about the rank of a spanning family.

Needed infrastructure: linear operators on the function space ℤ → ℝ, powers and products in Module.End, Module.rank/Module.finrank, and finite sums; Mathlib's LinearRecurrence may be adapted for the forward half. The definitions advance, opPoly and solutionSpace are reusable for any later mission on recurrences or on generating functions for bi-infinite sequences. Contributions of the milestone lemmas, of a proof of the goal that avoids factorisation over $\mathbb{C}$, and of a complex-valued variant are welcome.

Selected references

• Mitchel T. Keller and William T. Trotter, Applied Combinatorics, 2017 Edition, Chapter 9 (Recurrence Equations), CC BY-SA 4.0. appliedcombinatorics.org
• Mathlib, Mathlib/Algebra/LinearRecurrence.lean (ℕ-indexed linear recurrences, LinearRecurrence.solSpace_rank). Mathlib docs
• Ronald L. Graham, Donald E. Knuth and Oren Patashnik, Concrete Mathematics, 2nd ed., Addison-Wesley, 1994, Section 7.3 (solving recurrences). ISBN 978-0-201-55802-9.

Motivation

Many computations need the trace of a matrix $A$ that is never formed explicitly and can only be applied to vectors: the trace of a matrix function such as $\mathrm{trace}(A^{-1})$ or $\log\det A = \mathrm{trace}(\log A)$ in statistics and lattice QCD, the Frobenius norm $\|B\|_F^2 = \mathrm{trace}(B^TB)$ of an operator, or the number of triangles of a graph. The standard tool is Monte-Carlo estimation, introduced by M. F. Hutchinson (Hutchinson 1989): average $M$ quadratic forms $z_i^TAz_i$ over random sign vectors $z_i$. Each sample costs one matrix–vector product, uses one random bit per entry, and needs only additions and subtractions.

Before Avron and Toledo (2011), only the variance of such estimators had been analysed. A small variance does not say how many samples guarantee a given relative error with a given probability. Avron and Toledo gave the first bounds of this kind for several estimators. This mission covers the bound for Hutchinson's estimator, their Theorem 7.1.

Setting

A Rademacher random variable takes the values $+1$ and $-1$, each with probability $1/2$. Let $A \in \mathbb{R}^{n\times n}$ be symmetric positive semi-definite. Draw $M \ge 1$ independent random vectors $z_1, \ldots, z_M \in \mathbb{R}^n$ whose $Mn$ entries are independent Rademacher variables. Hutchinson's trace estimator is

$$H_M = \frac{1}{M}\sum_{i=1}^{M} z_i^TAz_i .$$

A single sample $z^TAz$ is an unbiased estimator of $\mathrm{trace}(A)$ (Lemma 2.1 of the paper, due to Hutchinson). For symmetric $A$ its variance is $2\bigl(\|A\|_F^2 - \sum_i A_{ii}^2\bigr)$, twice the squared Frobenius mass of $A$ off the diagonal.

Given $\epsilon > 0$ and $\delta \in (0,1)$, a random estimator $T$ is an $(\epsilon,\delta)$-approximator of $\mathrm{trace}(A)$ if

$$\Pr\bigl(|T - \mathrm{trace}(A)| \le \epsilon\,\mathrm{trace}(A)\bigr) \ge 1 - \delta .$$

The rank $\mathrm{rank}(A)$ is the number of nonzero eigenvalues $\lambda_j$ of $A$, counted with multiplicity.

Formalization targets

Goal: Theorem 7.1, sample bound for $H_M$

For every symmetric positive semi-definite $A$, every $0 < \epsilon \le 1/2$ and every $0 < \delta < 1$,

$$M \ge 6\epsilon^{-2}\ln\!\left(\frac{2\,\mathrm{rank}(A)}{\delta}\right) \quad\Longrightarrow\quad H_M \text{ is an } (\epsilon,\delta)\text{-approximator of } \mathrm{trace}(A).$$

The bound depends on $A$ only through its rank. It does not depend on the dimension $n$, on the condition number, or on how the trace is spread over the diagonal.

Milestones

1. Lemma 7.2 (Achlioptas 2001, Lemma 5). For a unit vector $\alpha \in \mathbb{R}^n$ and $S = \frac1M\sum_{i=1}^M(\alpha^Tz_i)^2$, for every $\epsilon > 0$,

$$\Pr(|S - 1| \ge \epsilon) \le 2\exp\!\left(-\frac{M}{2}\left(\frac{\epsilon^2}{2} - \frac{\epsilon^3}{3}\right)\right).$$

2. Per-direction bound (proof of Theorem 7.1, p. 8:11). Let $r \ge 1$ and $0 < \epsilon \le 1/2$. If $M \ge 6\epsilon^{-2}\ln(2r/\delta)$, then $\Pr(|S - 1| \ge \epsilon) \le \delta/r$.
3. From directions to the trace (proof of Theorem 7.1, p. 8:11). Write $A = U\Lambda U^T$ and $y_i = U^Tz_i$. If $|\frac1M\sum_i y_{ij}^2 - 1| \le \epsilon$ for every $j$ with $\lambda_j \ne 0$, then $|H_M - \mathrm{trace}(A)| \le \epsilon\,\mathrm{trace}(A)$. This step is deterministic.
4. Lemma 2.1 (Hutchinson). $\mathrm{E}(z^TAz) = \mathrm{trace}(A)$, and for symmetric $A$, $\mathrm{Var}(z^TAz) = 2(\|A\|_F^2 - \sum_i A_{ii}^2)$.

Significance

Theorem 7.1 gives a practitioner an explicit number of matrix–vector products after which Hutchinson's method is guaranteed to reach relative accuracy $\epsilon$ with confidence $1-\delta$. No bound was available before, although the method had been in wide use for two decades. The bound exceeds the one the same paper proves for Gaussian test vectors ($20\epsilon^{-2}\ln(2/\delta)$) by a $\ln(\mathrm{rank}(A))$ factor. The authors conjecture that this factor is not needed. Later work removed it: Roosta-Khorasani and Ascher (2015) proved a rank-free bound for the Rademacher case, and Cortinovis and Kressner (2022) extended sample bounds to indefinite matrices. Sample bounds of this type underlie variance-reduced estimators such as Hutch++ (Meyer et al. 2021).

The theorem is proved in the literature. To the platform's knowledge it has no machine-checked proof. Formalizing it produces a checked Rademacher concentration inequality for averages of squared linear forms (Achlioptas' lemma, which is also a core lemma of database-friendly Johnson–Lindenstrauss projections), and a checked spectral reduction from a quadratic-form estimator to its eigen-directions. Neither is currently in Mathlib.

Difficulty

The estimator is not an average of independent copies of a bounded variable with a small range: a single sample $z^TAz$ can deviate from $\mathrm{trace}(A)$ by an amount comparable to $\|A\|_F\sqrt n$. Chebyshev's inequality with the variance of Lemma 2.1 only gives a polynomial dependence on $1/\delta$. Hoeffding's inequality applied to $z^TAz$ directly gives a dependence on $n$ and on the size of the entries of $A$. Unlike the Gaussian case, the estimator cannot be written as a weighted sum of independent chi-squared variables, because rotating a Rademacher vector does not give another Rademacher vector. The central difficulty is Lemma 7.2: a tail bound for $(\alpha^Tz)^2$ that holds uniformly over every unit direction $\alpha$, including directions in which $\alpha^Tz$ is far from Gaussian (for $\alpha = e_1$ it is a constant).

Formalization scope

Matrices are Matrix (Fin n) (Fin n) ℝ, and positive semi-definiteness is Matrix.PosSemidef. The Rademacher law is $\tfrac12(\delta_1 + \delta_{-1})$ on ℝ. The sample space is Fin M → Fin n → ℝ with the product of $Mn$ copies of this law (hutchinsonSampleMeasure), so the law of the estimator is constructed, not assumed. $H_M(\omega) = (M:\mathbb{R})^{-1}\sum_i \omega_i\cdot(A\omega_i)$. Probabilities are Measure.real, and the $(\epsilon,\delta)$-approximator is Definition 4.1 verbatim. $\mathrm{rank}(A)$ is Matrix.rank. In Lemma 7.2 the i.i.d. copies $Q_i$ are the functions $(\alpha\cdot z_i)^2$ on this product space.

Corrections of printed statements, each recorded in the item's Formalization Note:

• Theorem 7.1 is printed without a range on $\epsilon$. Its proof needs $\frac{M}{2}(\frac{\epsilon^2}{2} - \frac{\epsilon^3}{3}) \ge \frac{M\epsilon^2}{6}$, which holds exactly when $\epsilon \le 1/2$. Without a range the printed statement is false: take $A = \frac1n\mathbf 1\mathbf 1^T$, $n = 10^4$, $\epsilon = 10$ and $\delta = 10^{-4}$. The condition admits $M = 1$, while $\Pr(H_1 > 11) \approx 9\cdot10^{-4} > \delta$. The goal and milestone 2 are therefore stated for $0 < \epsilon \le 1/2$.
• Lemma 2.1 is printed for an arbitrary $n\times n$ matrix. The variance formula fails for non-symmetric $A$: for $A = \begin{pmatrix}0&1\\0&0\end{pmatrix}$ the variance is $1$, not $2$. Symmetry is assumed for the variance part only.
• Proof of Theorem 7.1. The proof writes $\Lambda = UAU^T$ together with $y_i = U^Tz_i$. These fit together only for $A = U\Lambda U^T$, which is the convention of milestone 3.

For $A = 0$ the threshold involves $\ln 0$. Lean's Real.log 0 = 0 turns the condition into $M \ge 0$, which agrees with the paper's reading $\ln 0 = -\infty$. The conclusion then holds because $H_M = \mathrm{trace}(A) = 0$, so no extra hypothesis is added. A formalization that took the law of the samples as a hypothesis could make that hypothesis unsatisfiable and the theorem vacuous; the constructed product space rules this out.

A complete development needs:

• the product Rademacher measure and moment generating functions of Rademacher sums;
• a Chernoff bound for averages of i.i.d. bounded variables on a product space;
• the spectral theorem for real symmetric matrices, with rank equal to the number of nonzero eigenvalues;
• a finite union bound.

The Rademacher concentration results are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative proofs of Lemma 7.2.

Selected references

• H. Avron and S. Toledo, Randomized algorithms for estimating the trace of an implicit symmetric positive semi-definite matrix, Journal of the ACM 58(2), Article 8, 2011. https://doi.org/10.1145/1944345.1944349
• M. F. Hutchinson, A stochastic estimator of the trace of the influence matrix for Laplacian smoothing splines, Communications in Statistics – Simulation and Computation 18(3), 1059–1076, 1989. https://doi.org/10.1080/03610918908812806
• D. Achlioptas, Database-friendly random projections, Proceedings of PODS 2001, 274–281. https://doi.org/10.1145/375551.375608
• F. Roosta-Khorasani and U. Ascher, Improved bounds on sample size for implicit matrix trace estimators, Foundations of Computational Mathematics 15, 1187–1212, 2015. https://doi.org/10.1007/s10208-014-9220-1
• A. Cortinovis and D. Kressner, On randomized trace estimates for indefinite matrices with an application to determinants, Foundations of Computational Mathematics 22, 875–903, 2022. https://doi.org/10.1007/s10208-021-09525-9
• R. A. Meyer, C. Musco, C. Musco and D. P. Woodruff, Hutch++: Optimal stochastic trace estimation, SOSA 2021, 142–155. https://doi.org/10.1137/1.9781611976496.16

Motivation

Many matrices in scientific computing are available only implicitly: one can multiply a vector by $A$, for instance by solving a linear system or applying a matrix function, but the entries of $A$ are never formed. Quantities such as the trace must then be estimated from a small number of matrix–vector products. Randomized trace estimators do exactly this: draw random vectors $z$, compute the quadratic forms $z^TAz$, and average.

Avron and Toledo (J. ACM 58(2), 2011) gave the first sample bounds of the form "$M$ samples suffice for relative error $\epsilon$ with probability $1-\delta$" for the standard estimators. Among their results is a case in which the estimate is not merely approximate but exact: when $A$ is a projection matrix, its trace equals its rank, an integer, and rounding a Gaussian trace estimate recovers that integer with high probability. Computing the rank of a projection arises, for example, when charge densities are computed in electronic structure calculations without diagonalization (Bekas, Kokiopoulou and Saad 2007).

Setting

Let $n \ge 1$ and $A \in \mathbb{R}^{n\times n}$. A projection matrix here is an orthogonal projection: $A$ is symmetric and $A^2 = A$. Equivalently, $A$ is symmetric and every eigenvalue of $A$ is $0$ or $1$; its rank $\mathrm{rank}(A)$ is the number of eigenvalues equal to $1$.

Fix a number of samples $M \ge 1$. Let $z_1,\ldots,z_M \in \mathbb{R}^n$ be random vectors whose $Mn$ entries are independent standard normal random variables. The Gaussian trace estimator (Definition 3.1 of the paper) is

$$G_M = \frac{1}{M}\sum_{i=1}^{M} z_i^T A z_i .$$

Its expectation is $\mathrm{trace}(A)$. For $x \in \mathbb{R}$, $\mathrm{round}(x)$ denotes the nearest integer to $x$. For $k \ge 1$, a random variable $X$ has the $\chi^2$ distribution with $k$ degrees of freedom, $X \sim \chi^2(k)$, if it has the law of $g_1^2 + \cdots + g_k^2$ for independent standard normal $g_1, \ldots, g_k$.

Formalization targets

Goal: Lemma 5.3 (p. 8:9)

For a projection matrix $A$, a failure probability $\delta > 0$, and every integer $M \ge 1$ with $M \ge 24\,\mathrm{rank}(A)\ln(2/\delta)$,

$$\Pr\bigl(\mathrm{round}(G_M) \ne \mathrm{rank}(A)\bigr) \le \delta .$$

The number of samples depends on the rank and on $\delta$ only; there is no accuracy parameter, and none on $n$.

Milestones, in the order the proof uses them

1. Law of $MG_M$. $MG_M \sim \chi^2(M\,\mathrm{rank}(A))$.
2. $\chi^2$ tail bound (cited by the paper from Li, Hastie and Church 2007). For $X \sim \chi^2(k)$, $k\ge1$ and $0 < \epsilon \le \tfrac12$,

$$\Pr(|X - k| \ge \epsilon k) \le 2\exp(-k\epsilon^2/6).$$

3. Tail of $G_M$. For $\mathrm{rank}(A) \ge 1$ and $0 < \epsilon \le \tfrac12$,

$$\Pr(|G_M - \mathrm{rank}(A)| \ge \mathrm{rank}(A)\epsilon) \le 2\exp(-M\,\mathrm{rank}(A)\epsilon^2/6).$$

4. Eq. (2). If moreover $M \ge 6\,\mathrm{rank}(A)^{-1}\epsilon^{-2}\ln(2/\delta)$, then $\Pr(|G_M - \mathrm{rank}(A)| \ge \mathrm{rank}(A)\epsilon) \le \delta$.
5. Trace of a projection. $\mathrm{trace}(A) = \mathrm{rank}(A)$.

Significance

The lemma turns a randomized estimator into an exact algorithm with a controlled failure probability: the rank of an implicitly given projection is obtained from $O(\mathrm{rank}(A)\log(1/\delta))$ matrix–vector products, independently of the dimension $n$. It is also an instance where the paper's general relative-error bound for the Gaussian estimator (Theorem 5.2, whose sample count grows like $\epsilon^{-2}$) is improved by exploiting the spectrum of $A$: an absolute error below $\tfrac12$ is a relative error $\epsilon = 1/(2\,\mathrm{rank}(A))$, for which the general bound would require a number of samples quadratic in the rank, whereas Lemma 5.3 needs only a linear number.

The result is proved in the paper. The mission produces a machine-checked version of it, together with two pieces of reusable substrate: the exact $\chi^2$ law of a Gaussian quadratic form in an orthogonal projection, and a two-sided $\chi^2$ tail bound with explicit constant $1/6$ on the range $0<\epsilon\le 1/2$. To the best of available knowledge, none of these statements is formalized in Mathlib; a platform mission on the Johnson–Lindenstrauss lemma states a $\chi^2$ concentration bound with a different exponent, $(\epsilon^2-\epsilon^3)/4$, on the open range $0<\epsilon<1/2$, which does not cover the value $\epsilon = 1/2$ needed here when $\mathrm{rank}(A)=1$.

Difficulty

The deterministic part is short; the probabilistic part is not. The step "$y = Uz$ has independent standard normal entries because $U$ is orthogonal" is the rotation invariance of the standard Gaussian measure on $\mathbb{R}^n$, and it must be combined with the independence of the $M$ samples to identify the law of a sum of $M\,\mathrm{rank}(A)$ squares; this is a statement about product measures and pushforwards, not about moments. The $\chi^2$ tail bound is quoted by the paper without proof. Its constant $1/6$ is not the constant of the usual textbook $\chi^2$ estimates, and the bound is false outside a restricted range of $\epsilon$ (see below), so a generic sub-exponential concentration inequality with unspecified constants does not deliver it. Finally, the rounding step requires matching Mathlib's round with the event $|G_M - \mathrm{rank}(A)| < \tfrac12$.

Formalization scope

All declarations live in the namespace TraceEstimation.ProjectionRank. Matrices are Matrix (Fin n) (Fin n) ℝ. The sample space of $G_M$ is Fin M → Fin n → ℝ with the product measure Measure.pi (fun _ => Measure.pi (fun _ => gaussianReal 0 1)), so the law of the estimator is constructed, not assumed. Probabilities are Measure.real of events. "Projection matrix" is A.IsHermitian ∧ A * A = A (orthogonal projection); a non-symmetric idempotent also has eigenvalues $0$ and $1$, but the paper's proof diagonalizes $A$ by a unitary matrix, which requires symmetry. round is Mathlib's round : ℝ → ℤ; the rank is Matrix.rank. The $\chi^2$ distribution is not defined: its role is played by the pushforward of a product of standard normals under $g \mapsto \sum_l g_l^2$.

Corrections of the printed text, both in the $\chi^2$ tail bound (milestone 2):

• The paper prints $\Pr(|X - k| \le \epsilon k) \le 2\exp(-k\epsilon^2/6)$. The inner $\le$ is a misprint for $\ge$; the next display applies the bound with $\ge$.
• The paper gives no range for $\epsilon$. The bound fails for $\epsilon = 1$ and large $k$, since $\Pr(X \ge 2k)$ decays like $e^{-k(1-\ln 2)/2}$, slower than $e^{-k/6}$. The mission states it for $0<\epsilon\le 1/2$, and milestones 3 and 4 inherit that range; the proof uses only $\epsilon = 1/(2\,\mathrm{rank}(A)) \le 1/2$.

The goal keeps the paper's hypotheses: $\delta > 0$ with no upper bound, and $\mathrm{rank}(A) = 0$ allowed (both are true cases). A statement about the event $|G_M - \mathrm{rank}(A)| < \tfrac12$, or Eq. (2) alone, is not the goal; the goal is about $\mathrm{round}(G_M)$. The sample measure is a probability measure, so the bound $\le \delta$ is not vacuous.

Contributions welcome beyond the milestones: rotation invariance of the standard Gaussian vector under orthogonal matrices, the moment generating function of $\chi^2(k)$, and the spectral fact $\mathrm{trace}(A) = \mathrm{rank}(A)$ for idempotents, each reusable well outside this mission.

Selected references

• H. Avron and S. Toledo, Randomized algorithms for estimating the trace of an implicit symmetric positive semi-definite matrix, Journal of the ACM 58(2), Article 8, 2011. https://doi.org/10.1145/1944345.1944349
• P. Li, T. Hastie and K. Church, Nonlinear estimators and tail bounds for dimension reduction in $l_1$ using Cauchy random projections, in Learning Theory (COLT 2007), Lecture Notes in Computer Science 4539, Springer, 514–529, 2007 (the version the paper cites); journal version in Journal of Machine Learning Research 8, 2497–2532, 2007, https://jmlr.org/papers/v8/li07b.html
• C. Bekas, E. Kokiopoulou and Y. Saad, An estimator for the diagonal of a matrix, Applied Numerical Mathematics 57(11–12), 1214–1229, 2007. https://doi.org/10.1016/j.apnum.2007.01.003
• M. F. Hutchinson, A stochastic estimator of the trace of the influence matrix for Laplacian smoothing splines, Communications in Statistics – Simulation and Computation 19(2), 433–450, 1990. https://doi.org/10.1080/03610919008812866

Motivation

Boolean networks model gene regulatory networks by giving each gene an on/off value and updating all values synchronously by logical rules (Kauffman, 1969). Adding external Boolean inputs gives Boolean control networks (BCNs), in which a designer (a drug, an intervention) chooses the inputs over time. The basic control-theoretic question is controllability: can the inputs drive the network from any configuration to any other? Cheng and Qi (Automatica 2009) answered it for BCNs using the semi-tensor product of matrices, which rewrites a BCN as a linear recursion on canonical basis vectors.

Biological regulation is not instantaneous: transcription and translation introduce delays, so the next value of a gene can depend on several past values. Lu, Zhong, Ho, Tang and Cao (SIAM J. Control Optim. 2016) study delayed BCNs, in which the update reads the last $\mu$ states, and give criteria for two kinds of controllability, including the case where some configurations are dangerous and must be avoided (in biology, states corresponding to disease). The mission formalizes their criteria.

Setting

Write $\mathcal D=\{0,1\}$. A state is $x=(x_1,\dots,x_n)\in\mathcal D^n$ and an input value is $u\in\mathcal D^m$. Fix $\mu\ge1$. The delayed BCN (2.2) is

$$x_i(t+1)=f_i\big(u(t),x(t-\mu+1),\dots,x(t)\big),\qquad i=1,\dots,n,$$

with arbitrary Boolean functions $f_i:\mathcal D^{m+\mu n}\to\mathcal D$, collected into one map $F$ with $x(t+1)=F(u(t),X(t))$. A trajectory is the window $X(t)=(x(t-\mu+1),\dots,x(t))$ of the last $\mu$ states; its last entry is the current state. One step maps $X(t)$ under the input $u(t)$ to $X(t+1)=(x(t-\mu+2),\dots,x(t+1))$. A control sequence of length $k$ is $U=(u(0),\dots,u(k-1))$, with inputs chosen freely; $y(i)=X(i)$ denotes the trajectory after $i$ steps from an initial trajectory $y(0)$.

The transition-count matrix $Q$ has rows and columns indexed by trajectories: $Q_{b,a}$ is the number of input values $u$ taking trajectory $a$ to trajectory $b$ in one step. For a set $C_t$ of forbidden trajectories, $Q_{C_t}$ is $Q$ with the rows and columns of $C_t$ replaced by zeros, and $\mathbb Q_{C_t}$ is $Q$ with those rows and columns deleted.

The notions of controllability are:

• Trajectory controllable (Definition 3.1): from every initial trajectory, every trajectory $X_d$ equals $X(k)$ for some $k\ge1$ and some control sequence.
• Trajectory controllable under $C_t$ (Definition 3.11): for all trajectories $a,b\notin C_t$ there are $k\ge0$ and a control sequence steering $y(0)=a$ to $y(k)=b$ with $y(i)\notin C_t$ for $i=0,\dots,k$.
• State controllable (Definition 4.1): from every initial trajectory, every state equals $x(k)$ for some $k>0$ and some control sequence.

A real square matrix $A$ of size $N\ge2$ is reducible (Definition 3.7) if a simultaneous permutation of rows and columns brings it to block upper-triangular form $\begin{pmatrix}A_{11}&A_{12}\\0&A_{22}\end{pmatrix}$ with square diagonal blocks; it is irreducible otherwise, so every $1\times1$ matrix is irreducible.

$\mathbb N_1(k;y_a,y_b,C_t)$ counts the control sequences of length $k$ steering $y_a$ to $y_b$ while avoiding $C_t$; $\mathbb N_2(k;a,b_s)$ counts those steering the initial trajectory $a$ to $x(k)=b_s$; $\Xi^{p}_\mu$ is the set of trajectories with current state $p$.

Formalization targets

Goal: Theorem 3.12

$$\text{the delayed BCN is trajectory controllable under } C_t\iff \mathbb Q_{C_t}\ \text{is irreducible},$$

for every $\mu\ge1$, $n$, $m$, every update map and every forbidden set $C_t$. It is the most general criterion of the paper.

Milestones

• Proposition 3.5: for $k>0$, $\mathbb N_1(k;y_a,y_b,C_t)=y_b^{\mathsf T}(Q_{C_t})^ky_a$.
• Remark 3: $\mathbb N_1(k;y_a,y_b)=y_b^{\mathsf T}Q^ky_a$.
• Theorem 3.10: trajectory controllable $\iff$ $Q$ irreducible.
• Theorem 4.3: $\mathbb N_2(k;a,b_s)=\sum_{b\in\Xi^{b_s}_\mu}b^{\mathsf T}Q^ka$.
• Theorem 5.1: the same count while avoiding forbidden states $C_s$, with $Q$ zeroed on the trajectories containing a state of $C_s$.
• Corollary 5.3: trajectory controllability implies state controllability.

A supporting item, Lemma 3.9 (corrected form), relates Definition 3.7 to positivity of entries of powers for nonnegative matrices of size at least 2.

Significance

The criteria replace a question about control sequences of unbounded length by a finite test on one nonnegative integer matrix of size $2^{\mu n}$. The counting identities give more than a yes/no answer: they enumerate the control sequences achieving a transfer, which is what a designer choosing among interventions needs, and they handle forbidden states by passing to forbidden trajectories.

The results are proved in the paper; none of them has a machine-checked proof. Formalizing them yields a reusable Lean model of delayed (and, for $\mu=1$, ordinary) Boolean control networks defined directly through their dynamics, together with a checked bridge from dynamic reachability to the combinatorics of nonnegative matrices. A formal version also pins down points the printed text leaves loose: Lemma 3.9 as printed is false (it characterizes primitive, not irreducible, matrices), and the two different matrices $Q_{C_t}$ (zeroed) and $\mathbb Q_{C_t}$ (deleted) must not be confused.

Difficulty

The central step is the passage between three objects: reachability under the dynamics, positivity of entries of powers of $Q$, and the block-triangular definition of irreducibility. The counting identity for powers of $Q$ is a statement about sequences of inputs, not about paths in a graph, so the bijection between control sequences and weighted walks has to be established with the avoidance constraint carried at every intermediate time, including the endpoints. The equivalence between Definition 3.7 and strong connectivity is the classical graph-theoretic characterization, but it has edge cases the obvious argument misses: a $1\times1$ zero matrix is irreducible by Definition 3.7 yet has no positive power, which is exactly why Definition 3.11 allows $k=0$ while Definition 3.1 does not. A proof that routes through "some power of $\mathbb Q_{C_t}$ is entrywise positive", following the printed Lemma 3.9, proves a false intermediate statement.

Formalization scope

Conventions committed to in Lean:

• A state is Fin n → Bool (true is the paper's 1); a trajectory is Fin μ → State n with index 0 the oldest state and index $\mu-1$ the current state; $\mu\ge1$ is a standing assumption (NeZero μ); $n,m\ge0$ are arbitrary and no assumption is placed on the update functions.
• Matrices are indexed by trajectories rather than by the paper's index $j$ of $\delta^j_{2^{\mu n}}$. The paper's $Q=L\ltimes\mathbf 1_{2^m}$ is obtained by the simultaneous relabelling of Lemma 2.6, and every statement (entries of powers, sums over sets of trajectories, Definition 3.7) is invariant under it. $\mathbb Q_{C_t}$ is indexed by the subtype of allowed trajectories.
• Irreducibility is Definition 3.7 applied to the matrix with entries cast to $\mathbb R$; it is not Mathlib's Matrix.IsIrreducible, which differs on $1\times1$ matrices.
• Pinned readings: Definition 3.1 and Definition 4.1 use $k\ge1$; Definition 3.11 uses $k\ge0$; Proposition 3.5, Theorem 4.3 and Theorem 5.1 are stated for $k>0$ (Proposition 3.5 is false at $k=0$ when $y_a=y_b\in C_t$); Remark 3 holds for all $k\ge0$. "Avoiding $C_s$" in Theorem 5.1 means that no state $x(i)$, $i=1-\mu,\dots,k$, lies in $C_s$, which is the theorem's own middle term $\mathbb N_1(k;a,b,\Xi^{C_s})$. $\Xi^p_\mu$ is defined semantically by eq. (4.3), since the printed index range in (4.4) is a misprint. Lemma 3.9 is included in corrected form with $N\ge2$.

Controllability is defined through the dynamics and control sequences, never as positivity of entries of powers of $Q$; a formalization that defines reachability by $(Q^k)_{b,a}>0$ would reduce Theorems 3.10 and 3.12 to library facts and is ruled out.

Needed infrastructure: the correspondence between control sequences and products of entries of $Q$ (the core of Proposition 3.5), and the equivalence of Definition 3.7 with strong connectivity of the support graph for nonnegative matrices (Mathlib's Matrix.IsIrreducible, Matrix.isIrreducible_iff_exists_pow_pos and Matrix.pow_apply_pos_iff_nonempty_path cover much of the second part for sizes at least 2). Both are reusable beyond this mission, for ordinary BCNs, probabilistic BCNs and finite automata. Contributions of either piece, or of the semi-tensor-product bridge identifying $Q$ with $L\ltimes\mathbf 1_{2^m}$, are welcome.

Selected references

• J. Lu, J. Zhong, D. W. C. Ho, Y. Tang, J. Cao, On Controllability of Delayed Boolean Control Networks, SIAM J. Control Optim. 54(2):475–494, 2016. https://doi.org/10.1137/140991820
• D. Cheng, H. Qi, Controllability and observability of Boolean control networks, Automatica 45(7):1659–1667, 2009. https://doi.org/10.1016/j.automatica.2009.03.006
• S. A. Kauffman, Metabolic stability and epigenesis in randomly constructed genetic nets, J. Theoret. Biol. 22(3):437–467, 1969. https://doi.org/10.1016/0022-5193(69)90015-0
• A. Berman, R. J. Plemmons, Nonnegative Matrices in the Mathematical Sciences, SIAM Classics in Applied Mathematics 9, 1994. https://doi.org/10.1137/1.9781611971262

Motivation

Clique-width is a graph parameter introduced by Courcelle and Olariu (Discrete Appl. Math. 101 (2000)) that measures how far a graph is from being built by a few labelled operations. Every problem expressible in monadic second-order logic with quantification over vertices and vertex sets (MSO$_1$) can be solved in linear time on graphs given together with a decomposition of bounded clique-width (Courcelle, Makowsky and Rotics, Theory Comput. Syst. 33 (2000)). Bounded clique-width is more general than bounded tree-width: complete graphs have unbounded tree-width but clique-width $2$.

For fixed $k$ there was, before this paper, no polynomial-time algorithm that either decides that a graph has clique-width at least $k+1$ or outputs a decomposition of clique-width bounded by a function of $k$; the best known algorithm, by Johansson (2001), gave width $2k\log n$. Oum and Seymour (J. Combin. Theory Ser. B 96 (2006)) closed this gap with approximation $2^{3k+2}-1$, through rank-width and a factor-3 approximation for the branch-width of symmetric submodular functions.

Timeline:

• 1991: Robertson and Seymour introduce branch-width of graphs and hypergraphs (J. Combin. Theory Ser. B 52).
• 2000: Courcelle and Olariu define clique-width; Courcelle, Makowsky and Rotics solve MSO$_1$ problems on graphs given with a $k$-expression.
• 2001: Johansson gives a $2k\log n$ approximation.
• 2006: Oum and Seymour define rank-width, prove $\mathrm{rwd}(G) \le \mathrm{cwd}(G) \le 2^{\mathrm{rwd}(G)+1}-1$, and give an $O(n^9 \log n)$ algorithm that outputs a $(2^{3k+2}-1)$-expression or certifies clique-width above $k$.

Setting

All graphs are finite and simple. For a finite set $V$, a function $f : 2^V \to \mathbb{Z}$ is submodular if $f(X)+f(Y) \ge f(X\cap Y)+f(X\cup Y)$ and symmetric if $f(X) = f(V\setminus X)$.

A branch-decomposition of $f$ is a pair $(T, L)$ where $T$ is a tree with at least two vertices and all degrees at most $3$, and $L$ is a bijection from $V$ onto the leaves of $T$. Removing an edge $e$ of $T$ splits the leaves in two; the width of $e$ is $f$ of the set of elements of $V$ on one side. The width of $(T, L)$ is the largest edge width, and the branch-width $\mathrm{bw}(f)$ is the least width of a branch-decomposition, with $\mathrm{bw}(f) = f(\emptyset)$ when $|V| \le 1$.

A set $W \subseteq V$ is well-linked with respect to $f$ if for every partition $(X, Y)$ of $W$ and every $Z$ with $X \subseteq Z \subseteq V\setminus Y$, $f(Z) \ge \min(|X|, |Y|)$.

Let $A(G)$ be the adjacency matrix of $G$ over $\mathrm{GF}(2)$. For disjoint $X, Y \subseteq V(G)$, $\mathrm{cutrk}^*_G(X, Y)$ is the rank of the submatrix of $A(G)$ with rows $X$ and columns $Y$, and the cut-rank function is $\mathrm{cutrk}_G(X) = \mathrm{cutrk}^*_G(X, V(G)\setminus X)$. The rank-width $\mathrm{rwd}(G)$ is $\mathrm{bw}(\mathrm{cutrk}_G)$.

A $k$-expression is a term built from constants $\cdot_i$ (a vertex with label $i \in \{1,\dots,k\}$), the operators $\eta_{i,j}$ ($i \ne j$; add all edges between labels $i$ and $j$), $\rho_{i\to j}$ (relabel $i$ into $j$) and disjoint union $\oplus$. Its value is the labelled graph it produces; $G$ has clique-width $\mathrm{cwd}(G) \le k$ if some $k$-expression has value isomorphic to $G$.

An interpolation of $f$ is a function $f^*$ on disjoint pairs $(X, Y)$ that agrees with $f$ on $(X, V\setminus X)$, is monotone, submodular in the sense $f^*(A,B)+f^*(C,D) \ge f^*(A\cap C, B\cup D) + f^*(A\cup C, B\cap D)$, and has $f^*(\emptyset,\emptyset)=f(\emptyset)$.

Formalization targets

Goal: Theorem 1.1, certificate form

For a graph $G$ with at least one vertex and an integer $k \ge 1$:

$$\exists\, W,\ |W| = 3k+1,\ W \text{ well-linked for } \mathrm{cutrk}_G \;\Longrightarrow\; \mathrm{cwd}(G) \ge k+1,$$ $$\nexists\, W,\ |W| = 3k+1,\ W \text{ well-linked for } \mathrm{cutrk}_G \;\Longrightarrow\; \mathrm{cwd}(G) \le 2^{3k+2}-1.$$

The same explicit condition decides which side of the approximation holds; this is what the paper's algorithm certifies.

Milestones

1. Proposition 4.1: properties of an interpolation, including that $X \mapsto f^*(X, B) - f(\emptyset)$ is a matroid rank function on $V\setminus B$ when $f(\{v\}) - f(\emptyset) \le 1$.
2. Proposition 4.2: $f_{\min}(X,Y) = \min_{X\subseteq Z\subseteq V\setminus Y} f(Z)$ is an interpolation.
3. Theorem 5.1: a well-linked set of size $k$ forces $\mathrm{bw}(f) \ge k/3$ (for $k \ne 1$).
4. Theorem 5.2: no well-linked set of size $k$ implies $\mathrm{bw}(f) \le k$, when $f(\{v\}) \le 1$.
5. Proposition 6.1: $\mathrm{rk}\,M[X_1,Y_1] + \mathrm{rk}\,M[X_2,Y_2] \ge \mathrm{rk}\,M[X_1\cup X_2, Y_1\cap Y_2] + \mathrm{rk}\,M[X_1\cap X_2, Y_1\cup Y_2]$.
6. Corollary 6.2: submodularity of $\mathrm{cutrk}^*_G$ and $\mathrm{cutrk}_G$.
7. Section 6 claim: $\mathrm{cutrk}_G$ is symmetric submodular and $\mathrm{cutrk}^*_G$ interpolates it.
8. Proposition 6.3: $\mathrm{rwd}(G) \le \mathrm{cwd}(G) \le 2^{\mathrm{rwd}(G)+1}-1$.

Significance

The dichotomy turns clique-width, for which no exact polynomial algorithm is known even for fixed $k$, into a parameter that can be approximated with an explicit witness in each direction. Downstream, every algorithm for graphs of bounded clique-width that needs a $k$-expression as input becomes applicable to graphs given without one, at the cost of an exponential blow-up of the width.

The result is proved in the literature; this mission formalizes it. To our knowledge none of the objects involved — branch-width of set functions, rank-width, cut-rank, $k$-expressions, clique-width — has been formalized in Mathlib, and the submodularity of submatrix rank (Proposition 6.1) is absent from Mathlib's Matrix.rank API. The formal development would give reusable definitions of branch-decompositions of arbitrary integer set functions, of cut-rank, and of clique-width, and a machine-checked link between the combinatorial and the linear-algebraic width parameters.

Difficulty

The upper bound in Theorem 5.2 is the core. The natural approach, growing a branch-decomposition one leaf split at a time while keeping the width at most $k$, gets stuck at a leaf carrying a set $B$ with $f(B) = k$: a split of $B$ into two parts of $f$-value below $k$ has to be found, and it must be found from the failure of well-linkedness of a set that is not obviously related to $B$. The paper's device is the interpolation $f^*$, which attaches a matroid to $B$ whose base has exactly $f(B)$ elements. Formalizing this requires handling partial branch-decompositions, their extensions, and a maximality argument over trees, none of which exists in Mathlib.

Proposition 6.3's upper bound is a second, independent difficulty: a rank-decomposition must be converted into a $k$-expression by an induction over a rooted binary tree, with a relabelling argument bounding the number of labels by the number of distinct nonzero rows of a $\mathrm{GF}(2)$ matrix of rank $k$. Its lower bound needs the tree structure of a $k$-expression to be read as a branch-decomposition.

Formalization scope

The ground set is a Fintype V with DecidableEq V; subsets are Finset V; set functions are Finset V → ℤ, as in the paper. A branch-decomposition is a tree T : SimpleGraph (Fin n) with $n \ge 2$, all neighbour sets of size at most $3$, and an injective map $L$ from $V$ onto the vertices of degree $1$; the side of an edge $uw$ is found by reachability from $u$ after deleting $uw$. Branch-width, rank-width and clique-width are never computed as minima: "$\mathrm{bw}(f) \le k$" is the predicate "$|V| \le 1$ and $f(\emptyset) \le k$, or a branch-decomposition of width at most $k$ exists", lower bounds say that every branch-decomposition has a wide edge, and "$\mathrm{cwd}(G) \le k$" is "$G$ has a $k$-expression". Labels $\{1,\dots,k\}$ are Fin k. The value of a $k$-expression has as vertex type the occurrences of constants (a nested sum type), and $\eta_{i,j}$ requires $i \ne j$. Cut-rank uses Matrix.rank over ZMod 2 of submatrices of SimpleGraph.adjMatrix. An interpolation is a function on all pairs of subsets whose axioms are imposed on disjoint pairs only.

Running time is not formalized. The paper's Theorem 1.1 asserts an $O(n^9\log n)$ algorithm; there is no cost model on the page, and the goal states the certificate the algorithm returns instead. Without the running time, "$\mathrm{cwd}(G) \ge k+1$ or $\mathrm{cwd}(G) \le 2^{3k+2}-1$" holds for every graph, so that reading is ruled out as a formalization of the goal; so are well-linkedness with respect to anything other than $\mathrm{cutrk}_G$, widths defined by an unguarded infimum (which is $0$ on an empty family), $k$-expressions whose value is not the graph up to isomorphism or whose $\eta$ may join equal labels, and Theorem 5.1 stated for $k = 1$.

Correction of Theorem 5.1. As printed, Theorem 5.1 fails for $k = 1$: a singleton is always well-linked, but the edgeless graph on two vertices has cut-rank identically $0$ and branch-width $0 < 1/3$. The milestone carries the hypothesis $k \ne 1$; the goal uses the theorem only at size $3k+1 \ge 4$.

The graph with no vertex is excluded from the goal and from the upper bound of Proposition 6.3, since it has no $k$-expression for any $k$. Contributions welcome: proofs of the milestones, lemmas on branch-decompositions (suppressing degree-2 vertices, extending partial decompositions), and submatrix-rank submodularity, which is reusable beyond this mission.

Selected references

• S. Oum and P. Seymour, Approximating clique-width and branch-width, J. Combin. Theory Ser. B 96 (2006) 514–528. https://doi.org/10.1016/j.jctb.2005.10.006
• B. Courcelle and S. Olariu, Upper bounds to the clique width of graphs, Discrete Appl. Math. 101 (2000) 77–114. https://doi.org/10.1016/S0166-218X(99)00184-5
• B. Courcelle, J. A. Makowsky and U. Rotics, Linear time solvable optimization problems on graphs of bounded clique-width, Theory Comput. Syst. 33 (2000) 125–150. https://doi.org/10.1007/s002249910009
• N. Robertson and P. D. Seymour, Graph minors. X. Obstructions to tree-decomposition, J. Combin. Theory Ser. B 52 (1991) 153–190. https://doi.org/10.1016/0095-8956(91)90061-N

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