F Global small-core recompression from ordered thin SVD data
On this page · Visual guide: Compute the representation first · Permalink · Source line 1
This chapter retains the substantive mathematical pages of verification block 6 (v0.6.0). Its dated audit and pending-status passages describe that historical checkpoint; the final status is 56 of 56 registered finite items under the recorded hypotheses. Later chapters supersede earlier pending statements. All compiler and regression counts in this chapter are inherited records, not fresh runs for this edition.
F.1 Compact factors from actual column spaces
On this page · Visual guide: Stored width is not intrinsic rank · Visual guide: A complex range needs an adjoint · Permalink · Source line 4
Modules CompactRangeFactors and SmallCoreTransfer Let
Use the ordinary Euclidean inner products on the coordinate spaces. Define
The implementation constructs an orthonormal basis of each actual range subspace. Let \(Q_L\) and \(Q_R\) be the matrices of the corresponding isometric inclusions. Express the range-restricted input maps in these bases to obtain \(R_L,R_R\).
The checked identities are
with the analogous identities on the right. The dimension theorem is not an input:
The coordinate factors have full row rank. The construction therefore handles rank-deficient input factors without retaining artificial column directions.
Define the small core by actual multiplication,
Finite matrix associativity and adjoint identities give
The rank identity follows from both multiplication inequalities and the left inverse obtained by compression. It is not inferred from agreeing dimensions.
Zero factors and empty spaces. No positive-rank or nonempty-coordinate hypothesis is imposed. If a range is zero, its orthonormal basis has an empty index type. The factorization uses the resulting rectangular empty matrices. A separate theorem proves that the compact dimension is zero exactly when the original factor is zero.
Relation to QR. The argument only needs orthonormal columns and exact reconstruction. A compact QR factorization supplies these properties, but triangularity of its coordinate factor is irrelevant to the recompression theorem. The formal construction uses an exact orthonormal range basis; it does not claim Householder steps, pivot selection or floating-point stability. A supplied noncompact orthonormal factorization is also covered by the general transfer theorem, including extra zero singular directions.
F.2 Why a small-core optimum is a global optimum
On this page · Visual guide: Why a core optimum is global · Visual guide: A complex range needs an adjoint · Permalink · Source line 42
Module SmallCoreNorms; arbitrary ambient competitors For rectangular isometries \(Q,V\) define
The following statements are proved for the actual matrix rank and actual matrix norms:
For the spectral norm, the proof uses the Gram matrix identity
and the \(C^*\)-norm square identity, together with right-side adjoint symmetry. Compression follows from submultiplicativity and the isometry norm bound, including empty spaces.
For the Frobenius norm, trace cyclicity proves left and right isometric invariance. The proof also establishes the projection identity
Nonnegativity of the left side gives left compression contractivity; the right version follows by adjoints. No norm-preservation or contractivity hypothesis is inserted.
Suppose \(G_k\) is a best rank-at-most-\(k\) approximation to \(G\) in either norm. Take an arbitrary ambient matrix \(B\) with \({\operatorname{rank}} B\leq k\). Compression is an admissible small-core competitor and
This is the key global bridge: \(B\) is not required to lie in the supplied row and column spaces. The next two pages discharge the intermediate small-core optimality obligation, rather than leaving it as a hypothesis in the final theorem.
F.3 Spectral optimality from a kernel witness
On this page · Visual guide: Why a core optimum is global · Permalink · Source line 86
Modules DiagonalTruncation and SpectralOptimality Let \(\sigma_1\geq\cdots\geq\sigma_d\geq0\) and
Lean uses indices beginning at zero; the formulas on this page use the conventional one-based notation. The rank of \(D_k\) is proved to be at most \(k\), even when retained singular values are zero.
For \(k<d\), take any \(d\times d\) matrix \(B\) of rank at most \(k\). Restrict its domain to the first \(k+1\) coordinates using the actual coordinate inclusion \(J\). Since
rank-nullity supplies a nonzero vector \(z\) with \(BJz=0\). The vector \(y=Jz\) is nonzero, satisfies \(By=0\) and is supported in the first \(k+1\) coordinates. The injection and the support property are checked separately.
Monotonicity of the diagonal entries gives
Because \((D-B)y=Dy\), the operator-norm inequality implies
Cancellation of the strictly positive norm of \(y\) proves
The norm of the actual diagonal residual \(D-D_k\) equals \(\sigma_{k+1}\), so \(D_k\) attains the lower bound. If \(k\geq d\), the residual is zero and optimality follows from norm nonnegativity.
No optimality oracle. The nonzero kernel vector, its coordinate support and the diagonal norm bound are all derived. No Eckart–Young inequality, best-rank property or singular-tail formula is assumed. The final rectangular SVD result follows by the isometric transfer proved on the preceding page.
F.4 Frobenius optimality from kernel weights
On this page · Visual guide: Why a core optimum is global · Permalink · Source line 122
Modules KernelFrame and FrobeniusOptimality For an arbitrary competitor \(B\) with \({\operatorname{rank}} B\leq k\), construct an orthonormal matrix \(Q\) spanning its actual kernel. Then
Define the row weights
The proof derives
The upper bound uses contraction of \(Q^*\) on a coordinate vector. The weight sum follows from the trace of \(Q^*Q\) and rank-nullity.
For any nonnegative decreasing sequence \(a_i\), weights with these properties satisfy
This finite weighted inequality is itself proved. For \(k<d\), use \(\mu=a_{k+1}\) and compare the summands to tail weights \(v_i=0\) for \(i\leq k\) and \(v_i=1\) otherwise:
For a retained coordinate the inequality uses \(a_i\geq\mu\) and \(w_i\geq0\). For a tail coordinate it uses \(a_i\leq\mu\) and \(w_i\leq1\). Summation and \(\sum w_i\geq\sum v_i\) give the result.
Set \(a_i=\sigma_i^2\). Right compression cannot increase the Frobenius norm, and \(BQ=0\), hence
Direct calculation of \(D-D_k\) attains equality. Thus the best-rank Frobenius assertion is proved from kernel geometry and finite sums, independently of the spectral lower-bound proof. Repeated and zero singular values require no uniqueness claim.
F.5 Thin output factors and the final theorem
On this page · Permalink · Source line 161
Modules CompactTruncation and SmallCoreRecompression For the actual core \(G=R_LR_R^*\), supply ordered thin SVD data
These are precisely the fields of the formal SVD structure. It contains no rank-optimality or tail-error field. A derived theorem checks the Gram eigenvector equation
Let \(h=\min(d,k)\) and retain exactly the first \(h\) column indices. The rectangular square-root mask has entries
Lean proves its index cardinality and \(MM^*=D_k\). Define
The product equals \(Q_LWD_kZ^*Q_R^*\) and has rank at most \(k\). The principal theorem proves, for every ambient \(B\) with \({\operatorname{rank}} B\leq k\),
It also gives the exact errors
Both the squared and square-root Frobenius formulas are checked. All these statements are combined in KomorebiPaperVIII.SmallCore.small_core_optimal_recompression.
Endpoints. Rank zero produces the zero output; \(k\geq d\) reconstructs the original product. An empty SVD certificate is constructed for a zero core, and diagonal SVD certificates are constructed explicitly. Zero singular values are never inverted. At repeated singular values the result asserts optimality, not uniqueness of the minimizer.
F.6 Source map and verification
On this page · Visual guide: What this edition certifies · Permalink · Source line 200
One completed manuscript item; 79 supporting declarations
| Module | Main purpose | Theorems |
|---|---|---|
| SmallCoreNorms | Isometric norms, compression, rank | 19 |
| CompactRangeFactors | Actual compact column factors | 7 |
| SmallCoreTransfer | Global best-rank transfer | 7 |
| KernelFrame | Actual kernel and row weights | 8 |
| DiagonalTruncation | Rank and exact diagonal errors | 9 |
| FrobeniusOptimality | Weighted-tail lower bound | 5 |
| SpectralOptimality | Prefix-kernel lower bound | 7 |
| CompactTruncation | Thin square-root factors | 5 |
| SmallCoreRecompression | Main theorem and Gram relation | 6 |
| RecompressionEndpoints | Zero and full-retention cases | 6 |
| Total | Theorem 5.6 and its support | 79 |
Cumulative Lean run. All 40 local modules were compiled in a newly created output directory under Lean 4.34.0-rc2. Each exited with code zero and warnings were fatal. The 392 named theorem reports and 66 separately counted construction reports match the inventory exactly. Dependencies are confined to propext, Classical.choice and Quot.sound, or subsets thereof. False equality and admitted-proof controls were both rejected.
Pinned dependency. The actual Mathlib Git revision and manifest revision both match aeb72f1e9981b6d35b426b16dca7759be3e7ba06. The supplied compiled Mathlib cache was reused. It was not independently rebuilt or rechecked. Recovery verified all seven offline archive parts and the combined archive hash.
Infrastructure. Forty-three unit tests passed: 17 verifier tests, 12 fifth-block compatibility tests updated to the current totals, and 14 sixth-block tests. The original fifth-block fixed-count test file and metadata are preserved. Exact audit coverage, dependency order, no-bypass scans, classical-input boundaries and absence of optimality fields in the SVD structure are tested.
Failures retained. Of 31 captured development checks, 21 failed before correction and ten accepted drafts supplied the new modules. Failures concerned proof elaboration, finite-index/cardinality APIs, dependent rewrites, norm scopes, and warning diagnostics. Their inactive source snapshots and logs are retained separately from the successful fresh cumulative run. An initial interactive runtime launch was unsupported; noninteractive assembly succeeded.
F.7 Regressions, reproduction, and claim boundary
On this page · Visual guide: What this edition certifies · Permalink · Source line 235
Exact mathematical guarantees versus numerical implementations Independent numerical checks. A deterministic NumPy complex128 mirror tested 182 input-factor pairs at 638 truncation cases. The cases include rectangular matrices, rank-deficient and zero factors, empty spaces, repeated singular values, rank zero, and ranks beyond the core width. Comparison used both the small core and an independently computed ambient SVD reference. There were 3,190 arbitrary rank-bounded competitors, nine invalid-input rejection controls and two checks demonstrating failure when essential assumptions are removed.
The largest relative tail/reconstruction discrepancy was below \(3.7\times10^{-15}\), against a declared \(2\times10^{-9}\) tolerance. The mirror uses numerical rank thresholds and a numerical SVD to construct column bases. It is not compiled or extracted Lean code, a proof for all inputs, or a GPU benchmark. The formal result uses exact ranks and exact factorization equations.
Reproduce from the extracted source root.
python3 scripts/verify_integrity.py
python3 -m unittest discover -s scripts -p 'test_*.py' -v
python3 scripts/verify.py --kit /path/to/portable-kit \
--out verification/recheck --timeout 240
python3 scripts/run_sixth_regressions.py \
--out verification/recheck_numerical.jsonThe unit tests and numerical mirror require NumPy. The Lean verification path needs Python 3.10 or later and the separately supplied pinned Linux x86-64 kit. Local compiled interfaces are regenerated. The runner also supports bounded batches with --max-checks and hash-checked --resume. A partial checkpoint is not a pass.
What is complete. The 56-item manuscript-proved register is covered under the recorded hypotheses. The original theorem says to take orthonormal factors and a core SVD. The new construction and proof discharge the recompression conclusion from those exact factorization equations. In particular, no best-approximation assertion or error formula is hidden in an input certificate.
What is not claimed. General SVD existence or a numerical SVD implementation is not newly formalized. The four classical entries remain separately tracked; the ordered-SVD-data optimality argument now has checked support, while the CG algorithm theorem, floating-point product model and simultaneous-decomposition input are not newly proved in full. No new generic matrix-multiplication exponent, floating-point stability theorem or hardware speedup follows from this release.
The original manuscript, bibliography, source package and all five earlier supplements are preserved. Historical CPU/GPU measurements, earlier compiler execution suites and Papers I–VII in full were not rerun. Prose-to-formal correspondence is an explicit mathematical review, not an automated theorem equating a sentence with a Lean type.