TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedjudge pass (gpt-6-luna)verified 2026-10-22 (gpt-6.1-sol)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Exact basis-pursuit recovery under the strict nullspace property

Statement

Let $m, n, s \in N$ with $m, n \geq 1$ and $1 \leq s \leq n$ , and let $A \in R^{m \times n}$ satisfy the strict nullspace property of order $s$ . Use one-based coordinate labels $j = 1, \dots, n$ , with coordinate $j$ identified with the library's coordinate $j - 1$ . If $x^{†} \in R^{n}$ has at most $s$ nonzero coordinates, then $x^{†}$ is the unique minimizer of $\sum_{j = 1}^{n} ∣ z_{j} ∣$ over all $z \in R^{n}$ satisfying $A z = A x^{†}$ . This is a noiseless exact-data result; it makes no exact-recovery or support-recovery assertion for noisy observations.

Statement references

Strict nullspace property and coordinate conventions

Finite-dimensional one-norm

Triangle inequality for the finite-dimensional one-norm

Foucart and Rauhut, A Mathematical Introduction to Compressive Sensing, §4.1, Theorems 4.4–4.5, pp. 79–80

Bandeira, Ten Lectures and Forty-Two Open Problems in the Mathematics of Data Science, §6.3, pp. 106–107

Facts & Assumptions

Given: Integers $m, n \geq 1$ , an integer $1 \leq s \leq n$ , a matrix $A \in R^{m \times n}$ satisfying the strict nullspace property of order $s$ , and a vector $x^{†} \in R^{n}$ with at most $s$ nonzero coordinates.

[F1]

The strict nullspace property: for every nonzero $h \in \ker A$ and every $S \subseteq [n]$ with $∣ S ∣ \leq s$ , $∥ h_{S} ∥_{1} < ∥ h_{S^{c}} ∥_{1}$ .

[F2]

The $p$ -norms $∥ x ∥_{p}$ for rational $p \geq 1$ , and $∥ x ∥_{\infty}$ : $∥ u ∥_{1} = \sum_{j = 1}^{n} ∣ u_{j} ∣$ for $u \in R^{n}$ .

[F3]

Each $∥ \cdot ∥_{p}$ is a norm on $R^{n}$ , and the induced metrics are exactly $d_{1}$ , $d_{2}$ and $d_{\infty}$ of the published metric-spaces page: the p=1 formula is a norm on $R^{n}$ .

[F4]

A norm on a real vector space, the induced metric, and the dictionary with the metric axioms: every norm $N$ satisfies the triangle inequality $N (u + v) \leq N (u) + N (v)$ .

[F5]

The strict nullspace property: under its coordinate relabeling, $(A u)_{i} = \sum_{j = 1}^{n} A_{i j} u_{j}$ for each row $i$ .

[F6]

Laws of finite sums and finite products: finite sums are additive, so $\sum_{j = 1}^{n} (b_{j} - c_{j}) = \sum_{j = 1}^{n} b_{j} - \sum_{j = 1}^{n} c_{j}$ for real lists.

Proof

1.1givenF1F5F6constructalgebra

Let $S : = {j \in [n] : x_{j}^{†} \neq 0}$ , so $∣ S ∣ \leq s$ . For any feasible $z \neq x^{†}$ , put $h : = z - x^{†}$ . For each row $i$ , [F5] and [F6] give $(A h)_{i} = \sum_{j = 1}^{n} A_{i j} (z_{j} - x_{j}^{†}) = \sum_{j = 1}^{n} A_{i j} z_{j} - \sum_{j = 1}^{n} A_{i j} x_{j}^{†} = (A z)_{i} - (A x^{†})_{i} = 0$ , so $h \in \ker A$ and $h \neq 0$ . Hence [F1] gives $∥ h_{S} ∥_{1} < ∥ h_{S^{c}} ∥_{1}$ .

2.1givenF1F2F3F4step 1.1algebra∎

By [F3], $∥ \cdot ∥_{1}$ is a norm, so [F4] gives its triangle inequality. On $S$ , $z_{S} = x_{S}^{†} + h_{S}$ , hence $∥ x^{†} ∥_{1} = ∥ x_{S}^{†} ∥_{1} = ∥ z_{S} - h_{S} ∥_{1} \leq ∥ z_{S} ∥_{1} + ∥ h_{S} ∥_{1}$ . On $S^{c}$ , $x^{†}$ vanishes and $z_{S^{c}} = h_{S^{c}}$ , so $z = z_{S} + h_{S^{c}}$ with disjoint coordinate supports and $∥ z ∥_{1} = ∥ z_{S} ∥_{1} + ∥ h_{S^{c}} ∥_{1}$ . By step 1.1, this is strictly greater than $∥ z_{S} ∥_{1} + ∥ h_{S} ∥_{1} \geq ∥ x^{†} ∥_{1}$ . Thus every feasible vector distinct from $x^{†}$ has strictly larger objective, and $x^{†}$ , which is feasible, is the unique minimizer.

Depends on

Used by

Dependency tree · two levels

47 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Simon Foucart and Holger Rauhut, A Mathematical Introduction to Compressive Sensing, §4.1, Theorems 4.4–4.5 (standard reference, not scraped)
Afonso S. Bandeira, Ten Lectures and Forty-Two Open Problems in the Mathematics of Data Science, §6.3 (standard reference, not scraped)