Paper VIII: Packet Operator Algorithms, Exact Compilation, and GPU Realization

Download original file

This is the original TeX manuscript source. Use the paper’s PDF for typeset equations.

Read the typeset paper

Read this chapter with formatted equations

1 \clearpage\FloatBarrier\section{Global small-core recompression from ordered thin SVD data}\label{supp6:section:001}
2 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.\par
3 
4 \subsection{Compact factors from actual column spaces}\label{supp6:subsection:001}\textit{Modules CompactRangeFactors and SmallCoreTransfer}\par
5 Let
6 \[
7 L\in\C^{m\times t},\qquad R\in\C^{n\times t},\qquad A=LR^*.
8 \]
9 Use the ordinary Euclidean inner products on the coordinate spaces. Define
10 \[
11 S_L=\operatorname{range}(L),\quad r_L=\dim S_L,
12 \qquad S_R=\operatorname{range}(R),\quad r_R=\dim S_R.
13 \]
14 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$.
15 
16 The checked identities are
17 \[
18 \boxed{Q_L^*Q_L=I,\quad L=Q_LR_L,\quad R_L=Q_L^*L,}
19 \]
20 with the analogous identities on the right. The dimension theorem is not an input:
21 \[
22 \boxed{r_L=\rank L,\qquad r_R=\rank R.}
23 \]
24 The coordinate factors have full row rank. The construction therefore handles rank-deficient input factors without retaining artificial column directions.
25 
26 Define the small core by actual multiplication,
27 \[
28 G=R_LR_R^*\in\C^{r_L\times r_R}.
29 \]
30 Finite matrix associativity and adjoint identities give
31 \[
32 \boxed{A=Q_LGQ_R^*,\qquad \rank G=\rank A.}
33 \]
34 The rank identity follows from both multiplication inequalities and the left inverse obtained by compression. It is not inferred from agreeing dimensions.
35 
36 \textbf{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.
37 
38 \textbf{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.
39 
40 
41 
42 \subsection{Why a small-core optimum is a global optimum}\label{supp6:subsection:002}\textit{Module SmallCoreNorms; arbitrary ambient competitors}\par
43 For rectangular isometries $Q,V$ define
44 \[
45 \mathcal L(G)=QGV^*,\qquad \mathcal C(B)=Q^*BV,
46 \qquad Q^*Q=I,\quad V^*V=I.
47 \]
48 The following statements are proved for the actual matrix rank and actual matrix norms:
49 \[
50 \mathcal C(\mathcal L(G))=G,
51 \qquad \rank\mathcal L(G)=\rank G,
52 \qquad \rank\mathcal C(B)\leq\rank B,
53 \]
54 \[
55 \boxed{\norm{\mathcal L(G)}_\nu=\norm{G}_\nu,
56 \qquad \norm{\mathcal C(B)}_\nu\leq\norm B_\nu,
57 \quad \nu\in\{2,\mathrm F\}.}
58 \]
59 For the spectral norm, the proof uses the Gram matrix identity
60 \[
61 (QG)^*(QG)=G^*G
62 \]
63 and the $C^*$-norm square identity, together with right-side adjoint symmetry. Compression follows from submultiplicativity and the isometry norm bound, including empty spaces.
64 
65 For the Frobenius norm, trace cyclicity proves left and right isometric invariance. The proof also establishes the projection identity
66 \[
67 \norm{B-QQ^*B}_{\mathrm F}^{2}
68 =\norm B_{\mathrm F}^{2}-\norm{Q^*B}_{\mathrm F}^{2}.
69 \]
70 Nonnegativity of the left side gives left compression contractivity; the right version follows by adjoints. No norm-preservation or contractivity hypothesis is inserted.
71 
72 Suppose $G_k$ is a best rank-at-most-$k$ approximation to $G$ in either norm. Take an \emph{arbitrary} ambient matrix $B$ with $\rank B\leq k$. Compression is an admissible small-core competitor and
73 \[
74 \begin{aligned}
75 \norm{\mathcal L(G)-\mathcal L(G_k)}_\nu
76 &=\norm{G-G_k}_\nu\\
77 &\leq\norm{G-\mathcal C(B)}_\nu\\
78 &=\norm{\mathcal C(\mathcal L(G)-B)}_\nu\\
79 &\leq\norm{\mathcal L(G)-B}_\nu.
80 \end{aligned}
81 \]
82 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.
83 
84 
85 
86 \subsection{Spectral optimality from a kernel witness}\label{supp6:subsection:003}\textit{Modules DiagonalTruncation and SpectralOptimality}\par
87 Let $\sigma_1\geq\cdots\geq\sigma_d\geq0$ and
88 \[
89 D=\diag(\sigma_1,\ldots,\sigma_d),\qquad
90 D_k=\diag(\sigma_1,\ldots,\sigma_{\min(k,d)},0,\ldots,0).
91 \]
92 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.
93 
94 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
95 \[
96 \rank(BJ)\leq\rank B\leq k<k+1,
97 \]
98 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.
99 
100 Monotonicity of the diagonal entries gives
101 \[
102 \norm{Dy}^{2}
103 =\sum_{i=1}^{k+1}\sigma_i^{2}|y_i|^{2}
104 \geq\sigma_{k+1}^{2}\norm y^{2}.
105 \]
106 Because $(D-B)y=Dy$, the operator-norm inequality implies
107 \[
108 \sigma_{k+1}\norm y
109 \leq\norm{(D-B)y}
110 \leq\norm{D-B}_2\norm y.
111 \]
112 Cancellation of the strictly positive norm of $y$ proves
113 \[
114 \boxed{\sigma_{k+1}\leq\norm{D-B}_2.}
115 \]
116 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.
117 
118 \textbf{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.
119 
120 
121 
122 \subsection{Frobenius optimality from kernel weights}\label{supp6:subsection:004}\textit{Modules KernelFrame and FrobeniusOptimality}\par
123 For an arbitrary competitor $B$ with $\rank B\leq k$, construct an orthonormal matrix $Q$ spanning its actual kernel. Then
124 \[
125 BQ=0,\qquad Q^*Q=I,\qquad q=\dim\ker B=d-\rank B.
126 \]
127 Define the row weights
128 \[
129 w_i=\sum_{j=1}^{q}|Q_{ij}|^2.
130 \]
131 The proof derives
132 \[
133 \boxed{0\leq w_i\leq1,\qquad \sum_iw_i=q\geq\max(d-k,0).}
134 \]
135 The upper bound uses contraction of $Q^*$ on a coordinate vector. The weight sum follows from the trace of $Q^*Q$ and rank-nullity.
136 
137 For any nonnegative decreasing sequence $a_i$, weights with these properties satisfy
138 \[
139 \sum_i a_iw_i\geq\sum_{i>k}a_i.
140 \]
141 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:
142 \[
143 a_iv_i+\mu(w_i-v_i)\leq a_iw_i.
144 \]
145 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.
146 
147 Set $a_i=\sigma_i^2$. Right compression cannot increase the Frobenius norm, and $BQ=0$, hence
148 \[
149 \begin{aligned}
150 \norm{D-B}_{\mathrm F}^{2}
151 &\geq\norm{(D-B)Q}_{\mathrm F}^{2}\\
152 &=\norm{DQ}_{\mathrm F}^{2}
153 =\sum_i\sigma_i^2w_i
154 \geq\sum_{i>k}\sigma_i^2.
155 \end{aligned}
156 \]
157 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.
158 
159 
160 
161 \subsection{Thin output factors and the final theorem}\label{supp6:subsection:005}\textit{Modules CompactTruncation and SmallCoreRecompression}\par
162 For the actual core $G=R_LR_R^*$, supply ordered thin SVD data
163 \[
164 G=W\diag(\sigma)Z^*,\qquad W^*W=I,
165 \qquad Z^*Z=I,\qquad \sigma_1\geq\cdots\geq\sigma_d\geq0.
166 \]
167 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
168 \[
169 G^*GZ=Z\diag(\sigma_1^2,\ldots,\sigma_d^2).
170 \]
171 Let $h=\min(d,k)$ and retain exactly the first $h$ column indices. The rectangular square-root mask has entries
172 \[
173 M_{ij}=\begin{cases}\sqrt{\sigma_j},&i=j,\\0,&i\ne j,\end{cases}
174 \qquad 1\leq i\leq d,\quad 1\leq j\leq h.
175 \]
176 Lean proves its index cardinality and $MM^*=D_k$. Define
177 \[
178 \boxed{L_k=Q_LWM,\qquad R_k=Q_RZM.}
179 \]
180 The product equals $Q_LWD_kZ^*Q_R^*$ and has rank at most $k$. The principal theorem proves, for every ambient $B$ with $\rank B\leq k$,
181 \[
182 \boxed{\norm{LR^*-L_kR_k^*}_\nu\leq\norm{LR^*-B}_\nu,
183 \quad\nu\in\{2,\mathrm F\}.}
184 \]
185 It also gives the exact errors
186 \[
187 \norm{LR^*-L_kR_k^*}_2=
188 \begin{cases}\sigma_{k+1},&k<d,\\0,&k\geq d,\end{cases}
189 \qquad
190 \norm{LR^*-L_kR_k^*}_{\mathrm F}
191 =\left(\sum_{i>k}\sigma_i^2\right)^{1/2}.
192 \]
193 Both the squared and square-root Frobenius formulas are checked. All these statements are combined in\par
194 \path{KomorebiPaperVIII.SmallCore.small_core_optimal_recompression}.
195 
196 \textbf{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.
197 
198 
199 
200 \subsection{Source map and verification}\label{supp6:subsection:006}\textit{One completed manuscript item; 79 supporting declarations}\par
201 \begin{center}\small
202 \renewcommand{\arraystretch}{1.18}
203 \begin{tabular}{@{}p{.36\textwidth}p{.43\textwidth}r@{}}
204 \toprule
205 Module & Main purpose & Theorems\\
206 \midrule
207 SmallCoreNorms & Isometric norms, compression, rank & 19\\
208 CompactRangeFactors & Actual compact column factors & 7\\
209 SmallCoreTransfer & Global best-rank transfer & 7\\
210 KernelFrame & Actual kernel and row weights & 8\\
211 DiagonalTruncation & Rank and exact diagonal errors & 9\\
212 FrobeniusOptimality & Weighted-tail lower bound & 5\\
213 SpectralOptimality & Prefix-kernel lower bound & 7\\
214 CompactTruncation & Thin square-root factors & 5\\
215 SmallCoreRecompression & Main theorem and Gram relation & 6\\
216 RecompressionEndpoints & Zero and full-retention cases & 6\\
217 \midrule
218 Total & Theorem 5.6 and its support & 79\\
219 \bottomrule
220 \end{tabular}
221 \end{center}
222 
223 \textbf{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 \texttt{propext}, \texttt{Classical.choice} and \texttt{Quot.sound}, or subsets thereof. False equality and admitted-proof controls were both rejected.
224 
225 \textbf{Pinned dependency.} The actual Mathlib Git revision and manifest revision both match\par
226 \path{aeb72f1e9981b6d35b426b16dca7759be3e7ba06}.
227 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.
228 
229 \textbf{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.
230 
231 \textbf{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.
232 
233 
234 
235 \subsection{Regressions, reproduction and claim boundary}\label{supp6:subsection:007}\textit{Exact mathematical guarantees versus numerical implementations}\par
236 \textbf{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.
237 
238 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.
239 
240 \textbf{Reproduce from the extracted source root.}
241 \begin{verbatim}
242 python3 scripts/verify_integrity.py
243 python3 -m unittest discover -s scripts -p 'test_*.py' -v
244 python3 scripts/verify.py --kit /path/to/portable-kit \
245     --out verification/recheck --timeout 240
246 python3 scripts/run_sixth_regressions.py \
247     --out verification/recheck_numerical.json
248 \end{verbatim}
249 The 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 \texttt{--max-checks} and hash-checked \texttt{--resume}. A partial checkpoint is not a pass.
250 
251 \textbf{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.
252 
253 \textbf{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.
254 
255 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.

Back to source controls

Back to Paper VIII: Packet Operator Algorithms, Exact Compilation, and GPU Realization