TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

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.

The SVD threshold solver gives the unique minimum-norm fit to its truncated model

Statement

Let $A \in F^{m \times n}$ , $b \in F^{m}$ , and $τ \geq 0$ , where $F = R$ or $C$ . Let $A = U Σ V^{*}$ be an exact SVD. Define $Σ_{τ}$ by retaining $σ_{i}$ when $σ_{i} > τ$ and replacing each $σ_{i} \leq τ$ by zero, and set $A_{τ} = U Σ_{τ} V^{*}$ . Put $q = # {i : σ_{i} > τ}$ , the spectral numerical rank of $A$ at threshold $τ$ . The vector $x_{τ} = A_{τ}^{+} b$ is the unique minimum-Euclidean-norm least-squares solution for the truncated model $A_{τ} x \approx b$ . An exact-arithmetic run of Rank-thresholded least squares by the singular value decomposition that converges within its supplied finite sweep budget and supplies this SVD record returns $x_{τ}$ ; a failure or exhausted budget returns inconclusive. No convergence within an arbitrary budget is asserted. Moreover, $∥ A - A_{τ} ∥_{2} = σ_{q + 1} \leq τ, ∥ A x_{τ} - b ∥_{2} \leq ∥ A_{τ} x_{τ} - b ∥_{2} + τ ∥ x_{τ} ∥_{2},$ with $σ_{p + 1} = 0$ when $q = p = \min (m, n)$ . If every discarded singular value is zero, then $A_{τ} = A$ and $x_{τ}$ is the unique minimum-norm least-squares solution for the original matrix. If a positive singular value is discarded, no original-matrix least-squares optimality is asserted.

Facts & Assumptions

Given: An exact SVD, threshold $τ$ , right-hand side $b$ , and the associated truncated matrix and pseudoinverse.

[F1]

Every linear map between finite-dimensional real or complex inner product spaces admits a singular value decomposition: $A = U Σ V^{*}$ with orthonormal singular vectors and nonnegative diagonal singular values.

[F2]

The truncated singular-value pseudoinverse obtained by discarding singular values below a declared numerical-rank threshold: $A_{τ}^{+} = V Σ_{τ}^{+} U^{*}$ , where diagonal entries are $1 / σ_{i}$ for $σ_{i} > τ$ and zero otherwise.

[F3]

For every right-hand side $b$ , $A^{+} b$ is the unique least-squares solution of minimum Euclidean norm: for any matrix $M$ and right-hand side $b$ , $M^{+} b$ is the unique least-squares solution of minimum Euclidean norm.

[F4]

The best rank-at-most-k approximation in operator norm is the rank-k truncation of a singular value decomposition: for $0 \leq q < n$ , the SVD truncation to rank at most $q$ has spectral residual $σ_{q + 1}$ , including the stated zero-tail convention.

[F5]

Spectral numerical rank counts singular values above threshold over R or C: for $m, n \geq 1$ , the spectral numerical rank at threshold $τ$ counts precisely the singular values strictly greater than $τ$ .

[F6]

The Moore--Penrose pseudoinverse $A^{+}$ as the solution of the four Penrose equations and Every finite real or complex matrix has a unique Moore--Penrose pseudoinverse: the four Penrose equations define the Moore--Penrose pseudoinverse, and every finite real or complex matrix has a unique matrix satisfying them.

[F7]

The operator norm is zero on the zero domain and otherwise is max_{||v||=1} ||Tv||: the matrix operator norm is zero on a zero domain and is the maximum of $∥ M x ∥_{2}$ over unit vectors otherwise. Thus $∥ M x ∥_{2} \leq ∥ M ∥_{2} ∥ x ∥_{2}$ for every vector $x$ by scaling when $x \neq 0$ , and directly when $x = 0$ .

[F8]

The inner-product norm is definite, homogeneous, and satisfies the triangle inequality: the Euclidean vector norm satisfies $∥ u + v ∥_{2} \leq ∥ u ∥_{2} + ∥ v ∥_{2}$ .

[F9]

Numerical rank relative to a declared norm, scale, and tolerance defines numerical rank as the least rank of a matrix within the declared norm tolerance, for all finite matrix dimensions, including zero.

[F10]

Rank-thresholded least squares by the singular value decomposition: on exact-arithmetic convergence with the returned SVD record the procedure computes $x_{τ} = A_{τ}^{+} b$ ; a failure or exhausted sweep budget returns inconclusive.

Proof

1.1F1F2F6algebra

Let $I = {i \leq p : σ_{i} > τ}$ . By [F1]–[F2], $A_{τ} = \sum_{i \in I} σ_{i} u_{i} v_{i}^{*}$ and $A_{τ}^{+} = \sum_{i \in I} σ_{i}^{- 1} v_{i} u_{i}^{*}$ . Orthonormality gives $A_{τ} A_{τ}^{+} = \sum_{i \in I} u_{i} u_{i}^{*}$ and $A_{τ}^{+} A_{τ} = \sum_{i \in I} v_{i} v_{i}^{*}$ , which are self-adjoint. Using $u_{i}^{*} u_{j} = v_{i}^{*} v_{j} = δ_{i j}$ in those sums verifies the two Penrose product equations. Together with self-adjointness, these are the four equations; by [F6], $A_{τ}^{+}$ is the unique Moore--Penrose pseudoinverse of $A_{τ}$ . The calculation includes $I = \emptyset$ , when both matrices and sums are zero.

1.2F1F4F5F7F9algebra

If $p = 0$ , the matrix has no singular-value terms, so $A_{τ} = A$ , $q = 0$ , and its spectral numerical rank is zero because $A$ has rank zero and distance zero from itself by [F9]. If $p > 0$ , [F5] identifies $q$ with the spectral numerical rank retained by the strict threshold. When $q < p$ , one has $q < p \leq n$ , so [F4] applies with $k = q$ and gives $∥ A - A_{τ} ∥_{2} = σ_{q + 1} \leq τ$ . When $q = p$ , [F1] shows directly that all positive singular terms are retained, hence $A_{τ} = A$ and the residual norm is zero, equal to the stated convention $σ_{p + 1} = 0$ . This last branch also covers $p = 0$ without applying [F4] or [F5] outside their dimension hypotheses.

2.1step 1.1F3F10

Apply [F3] to $M = A_{τ}$ . Its unique minimum-norm least-squares solution is $A_{τ}^{+} b = x_{τ}$ , proving the truncated-model claim independently of any iteration budget. For an exact-arithmetic run converging within its supplied budget and returning the stated SVD record, [F10] identifies this vector as the returned solution; the failure branches return inconclusive.

2.2step 1.2F7F8algebra

By [F7], $∥ (A - A_{τ}) x_{τ} ∥_{2} \leq ∥ A - A_{τ} ∥_{2} ∥ x_{τ} ∥_{2}$ ; [F8] gives $∥ A x_{τ} - b ∥_{2} \leq ∥ A_{τ} x_{τ} - b ∥_{2} + ∥ (A - A_{τ}) x_{τ} ∥_{2}$ . Combining with step 1.2 proves the stated residual bound.

3.1step 2.1step 1.2algebra

If every discarded singular value is zero, the SVD formula gives $A = A_{τ}$ , so step 2.1 is the original-matrix solution. If any positive singular value is discarded, the proof has established optimality only for $A_{τ}$ ; it supplies no normal-equation or minimum-residual claim for $A$ .

4.1step 1.1step 1.2step 2.1step 2.2step 3.1∎

Steps 1.1, 1.2, 2.1, 2.2, and 3.1 prove all stated claims and the limitation.

Depends on

Used by

A converged exact sketch-and-solve run returns a sketch minimizer Theorem

Dependency tree · two levels

35 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

Wen-Wei Lin, Lecture Notes of Matrix Computations, §3.2.2 (standard reference, not scraped)