TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Core-SVD recompression is best at the declared Frobenius tolerance

Statement

Let $M = \sum_{s} U_{s} V_{s}^{*}$ be the finite matrix input to Core-SVD recompression with rank and error tolerances, and let $k$ and $δ \geq 0$ be its rank cap and Frobenius tolerance. If the algorithm returns success with rank $q$ , its returned matrix $\hat{M}$ has rank $q$ and satisfies $∥ M - \hat{M} ∥_{F} = (\sum_{j > q} s_{j} (M)^{2})^{1 / 2} \leq δ$ . No lower-rank matrix meets the same tolerance. If the algorithm returns tolerance-not-met, no matrix of rank at most $k$ meets the tolerance.

Facts & Assumptions

Given: Finite real or complex factor matrices $U_{s}, V_{s}$ , their represented matrix $M$ , an integer rank cap $k$ , a tolerance $δ \geq 0$ , and the procedure and status returned by Core-SVD recompression with rank and error tolerances.

[F1]

Core-SVD recompression with rank and error tolerances: the procedure forms $C = R_{U} R_{V}^{*}$ from compact SVDs of the concatenated factors, takes an SVD of $C$ , selects the smallest $q \leq k$ whose discarded singular-value tail is at most $δ$ , and reports that tail as $e_{q}$ .

[F2]

Every linear map between finite-dimensional real or complex inner product spaces admits a singular value decomposition: every finite real or complex matrix has an SVD with orthonormal left and right singular vectors and nonnegative singular values.

[F3]

Finite tensor arrays and the Frobenius inner product: matrix rank is the dimension of the column image, the Frobenius norm is the square root of the sum of squared entry moduli, and $M^{*}$ is the conjugate transpose.

[F4]

Best rank-k matrix approximation in Frobenius norm: the rank-at-most- $r$ truncated SVD has Frobenius error equal to the square root of the discarded squared singular values, and every rank-at-most- $r$ matrix has at least that error.

Proof

1.1F1F2F3algebra

The compact SVDs in [F1] give $U = Q_{U} R_{U}$ and $V = Q_{V} R_{V}$ with orthonormal columns in $Q_{U}, Q_{V}$ . Hence $M = Q_{U} (R_{U} R_{V}^{*}) Q_{V}^{*} = Q_{U} C Q_{V}^{*}$ . If $C = P Σ Q^{*}$ is its SVD, then $M = (Q_{U} P) Σ (Q_{V} Q)^{*}$ ; both outer factors have orthonormal columns, so completing them by orthonormal bases gives an SVD of $M$ . Thus the core and $M$ have the same positive singular values.

2.1F1F2F3F4step 1.1algebra∎

On success, the output factors in [F1] form the rank- $q$ truncation of the lifted SVD in step 1.1. Its retained singular values are positive and their singular vectors are orthonormal, so its rank is exactly $q$ . Applying [F4] gives $∥ M - \hat{M} ∥_{F} = (\sum_{j > q} s_{j} (M)^{2})^{1 / 2} \leq δ$ . By the minimal choice in [F1], every smaller $r < q$ has discarded tail greater than $δ$ ; [F4] then rules out every rank-at-most- $r$ approximation meeting the tolerance. If the algorithm fails, then $k < t$ and the tail at $k$ is greater than $δ$ (otherwise $q = k$ would pass); [F4] rules out every rank-at-most- $k$ approximation. This includes $q = 0$ , $k = 0$ , zero factors, and repeated singular values.

Depends on

Used by

Dependency tree · two levels

9 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

Steffen Börm, Lars Grasedyck, and Wolfgang Hackbusch, Hierarchical Matrices, MiS Lecture Note 21 (2003; revised June 2006), §§7.1–7.2 (standard reference, not scraped)
Ralf Hiptmair, AdvNumCSE Lecture Document, Chapter 2, “Local Low-Rank Compression of Non-Local Operators” (ETH Zürich, AT’23), §2.4.2, Theorem 2.4.2.6 (standard reference, not scraped)