Realization Calculus

Download original file

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

Read the typeset paper

1 \clearpage\FloatBarrier\section{Global small-core recompression from ordered thin SVD data}\label{supp6:section:001}
2 This appendix derives global small-core recompression from actual compact ranges and supplied ordered thin-SVD equations. Optimality is proved against arbitrary ambient competitors.\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 The competitor $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, while 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, while $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{Place in the finite development}\label{supp6:subsection:006}
201 The 56-item manuscript-proved register is covered under its stated hypotheses. General SVD existence, a numerical SVD algorithm, floating-point CG convergence and hardware speedups do not follow merely from this formal scope. The formal companion identifies the exact declaration map and recorded verification evidence.
202 
203 The historical compiler, regression and development records appear in the formal companion under ``Historical proof-development records.''

Back to source controls

Back to Realization Calculus