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{Structured transforms and clipped precision}\label{supp4:section:001}
2 This appendix proves the structured-transform identities and the global clipped-allocation theorem, including the maximal-budget endpoint.\par
3 
4 \subsection{Circulant Fourier diagonalization}\label{supp4:subsection:001}\textit{Source item 4.3; module CirculantFourier}\par
5 Let $n>0$, with coordinates indexed by $\mathbb Z/n\mathbb Z$. Define the actual circulant by
6 \[
7 C(c)_{jk}=c_{j-k}.
8 \]
9 The formal Fourier matrix is
10 \[
11 F_{jk}=\frac{1}{\sqrt n}\,\chi(-jk),
12 \qquad
13 \chi(a)=\exp\!\left(\frac{2\pi i a}{n}\right).
14 \]
15 The standard character is not left abstract: a checked theorem identifies these entries with
16 \[
17 \frac{1}{\sqrt n}\exp\!\left(-\frac{2\pi i\,\operatorname{val}(j)\operatorname{val}(k)}n\right).
18 \]
19 The value representatives enter only this explicit exponential formula. All modular algebra uses the residue classes themselves.
20 
21 \textbf{Normalization and inversion.} The proof identifies matrix application with the ordinary counting-measure discrete Fourier transform:
22 \[
23 Fx=n^{-1/2}\operatorname{DFT}(x).
24 \]
25 It separately identifies $F^*x$ with the appropriately scaled inverse transform. Mathlib's checked Fourier inversion theorem and the proved scalar normalization yield both identities
26 \[
27 \boxed{F^*F=I,\qquad FF^*=I.}
28 \]
29 No unitarity assumption is inserted.
30 
31 \textbf{Convolution and reconstruction.} An explicit bijective change of index proves
32 \[
33 \operatorname{DFT}(C(c)x)_k
34 =\operatorname{DFT}(c)_k\operatorname{DFT}(x)_k.
35 \]
36 This gives the matrix intertwining relation $FC(c)=\operatorname{diag}(\operatorname{DFT}c)F$. Multiplication by the proved inverse reconstructs the circulant:
37 \[
38 \boxed{C(c)=F^*\operatorname{diag}(\sqrt n\,Fc)F.}
39 \]
40 The two-transform application formula is also checked for every input vector. The result includes $n=1$ and arbitrary complex coefficients. Hermiticity is not required.
41 
42 \textbf{Claim boundary.} This verifies the exact Fourier representation, not an $O(n\log n)$ implementation of the transform. The latter is an additional algorithmic factorization of the same linear map.
43 
44 
45 
46 \subsection{Toeplitz padding and column-major vectorization}\label{supp4:subsection:002}\textit{Source items 4.4 and 4.5}\par
47 \textbf{Toeplitz embedding.} For $n>0$, define
48 \[
49 T_{ij}=
50 \begin{cases}
51 c_{i-j},&j\le i,\\
52 r_{j-i},&i<j.
53 \end{cases}
54 \]
55 The diagonal is supplied by $c_0$, and the coordinate $r_0$ is unused. The constructed generator of length $2n$ is
56 \[
57 g=(c_0,\ldots,c_{n-1},0,r_{n-1},\ldots,r_1),
58 \]
59 and the padding map is the actual finite-index sum eliminator that appends $n$ zeros.
60 
61 Lean first proves the upper-left block identity
62 \[
63 C(g)_{ij}=T_{ij}\qquad(0\le i,j<n).
64 \]
65 For $j\le i$, finite modular subtraction has its ordinary value $i-j$. For $i<j$, it has wrapped value $2n+i-j$, whose reversed generator coordinate is $j-i$. Both branches are checked with the actual finite-index arithmetic.
66 
67 Splitting the product sum into the original and padded halves then gives
68 \[
69 \boxed{\bigl(C(g)(x,0)^T\bigr)_{0:n}=Tx.}
70 \]
71 The generator's first half and its middle zero are checked separately. Neither symmetry nor conjugation is involved.
72 
73 \textbf{Kronecker application.} For $A\in\C^{m\times m}$, $B\in\C^{n\times n}$ and $X\in\C^{n\times m}$, Lean proves
74 \[
75 \boxed{(A\otimes B)\operatorname{vec}(X)=\operatorname{vec}(BXA^T).}
76 \]
77 The formal vectorization is explicitly column-major: its pair coordinate $(j,i)$ stores $X_{ij}$. The right factor is the \emph{ordinary transpose}, not the conjugate transpose. This distinction is essential over $\C$.
78 
79 Finite types of multiplication/accumulation events and stored scalar addresses give
80 \[
81 \boxed{2n^2m+2nm^2\ \text{modeled operations},\qquad n^2+m^2\ \text{factor entries}.}
82 \]
83 The explicit Kronecker matrix has $n^2m^2$ entries. As in the manuscript, the operation model assigns two scalar operations to each multiply-accumulate term.
84 
85 
86 
87 \subsection{Arbitrary tensor factors}\label{supp4:subsection:003}\textit{Source item 4.6; module StructuredTensor}\par
88 Let $A_0,\ldots,A_{k-1}$ be square factors of order $d$. Tensor coordinates are represented by a nested product of $k$ copies of $\{0,\ldots,d-1\}$. The empty product is a singleton. Lean proves that the coordinate type has cardinality $d^k$.
89 
90 The represented matrix is defined recursively using the actual Kronecker product:
91 \[
92 M_0=[1],\qquad M_{k+1}=A_0\otimes M_k(A_1,\ldots,A_k).
93 \]
94 The algorithm is defined independently. On each slice with fixed first coordinate, it recursively contracts the trailing modes. It then applies $A_0$ to the resulting first-coordinate fibers:
95 \[
96 y_{i,u}=\sum_{j=0}^{d-1}(A_0)_{ij}\,
97 \operatorname{Apply}_{k}(A_1,\ldots,A_k;x_{j,\cdot})_u.
98 \]
99 Induction, the Kronecker entry formula, and finite-sum distributivity prove
100 \[
101 \boxed{\operatorname{Apply}_k(A;x)=M_k(A)x.}
102 \]
103 Thus correctness is not inferred merely from agreeing dimension or storage formulas.
104 
105 \textbf{Operation events.} The event type for $k+1$ modes is a disjoint union of $d$ copies of the trailing event type and the events for the final fiber contraction. Its cardinality obeys
106 \[
107 W_0=0,\qquad W_{k+1}=dW_k+2d^{k+2}.
108 \]
109 Lean proves the closed form
110 \[
111 \boxed{W_k=2kd^{k+1}.}
112 \]
113 The factor-address type has cardinality
114 \[
115 \boxed{k d^2.}
116 \]
117 These statements include $k=0$ and $d=0$. With no factors, the action is the identity on the singleton coordinate type and incurs zero modeled arithmetic. With $d=0$ and at least one factor, the coordinate type is empty.
118 
119 \textbf{Implementation boundary.} These are recursive mathematical contractions with exact complex arithmetic. The event model assumes each intermediate slice is computed once and reused. It is not an instrumented execution trace or a cost bound for every evaluator of the raw functional definition. The count excludes indexing, allocation, data movement, fused instruction effects, and the real-operation cost of a complex scalar operation. Those require a separately declared backend model.
120 
121 
122 
123 \subsection{Walsh butterfly and exact addition count}\label{supp4:subsection:004}\textit{Source item 4.7; module WalshTransform}\par
124 The two-point matrix is constructed as
125 \[
126 H_2=\begin{pmatrix}1&1\\1&-1\end{pmatrix},
127 \]
128 and the full family is defined by $H_1=[1]$ and
129 \[
130 H_{2N}=H_2\otimes H_N
131 =\begin{pmatrix}H_N&H_N\\H_N&-H_N\end{pmatrix}.
132 \]
133 The two-point orthogonality identity is checked explicitly. Kronecker multiplication and induction then prove
134 \[
135 \boxed{H_NH_N^T=NI,\qquad N=2^k.}
136 \]
137 The ordinary transpose is sufficient because all constructed entries are real, even though the scalar field is $\C$.
138 
139 \textbf{Actual butterfly.} For the two halves $x_0,x_1$ of the input, the independently defined procedure returns
140 \[
141 \operatorname{Walsh}_{2N}(x_0,x_1)
142 =\bigl(\operatorname{Walsh}_N(x_0+x_1),
143        \operatorname{Walsh}_N(x_0-x_1)\bigr).
144 \]
145 Lean proves that this vector equals $H_{2N}x$. The argument expands the two first-coordinate cases and applies finite-sum distributivity. It does not assume that the recursive algorithm already represents the matrix.
146 
147 \textbf{Exact arithmetic count.} Each pair of slices forms one sum and one difference at every trailing coordinate. The event type therefore gives
148 \[
149 A_0=0,\qquad A_{k+1}=2A_k+2^{k+1}.
150 \]
151 The closed form and its equivalent logarithmic expression are both checked:
152 \[
153 \boxed{A_k=k2^k=N\log_2N.}
154 \]
155 The logarithm in the formal count is the natural-number binary logarithm, with its power-of-two identity proved by Mathlib. The case $N=1$ has zero arithmetic events.
156 
157 A further action theorem gives
158 \[
159 H_N(H_N^Tx)=Nx,
160 \]
161 which identifies the inverse after division by the nonzero scalar $N$. This result concerns exact arithmetic, not floating-point error accumulation through a butterfly implementation.
162 
163 
164 
165 \subsection{Clipped precision: existence and multiplier uniqueness}\label{supp4:subsection:005}\textit{Source item 8.5; module ClippedPrecision}\par
166 Let $E$ be a finite nonempty set and suppose
167 \[
168 s_e>0,\qquad c_e>0,\qquad m_e>0,
169 \qquad 0<\tau\le\sum_e s_em_e.
170 \]
171 The feasible set is
172 \[
173 0<\varepsilon_e\le m_e,\qquad \sum_e s_e\varepsilon_e=\tau,
174 \]
175 and the objective is the same logarithmic objective used in item 8.4:
176 \[
177 J(\varepsilon)=\sum_e c_e\log(1/\varepsilon_e).
178 \]
179 Strictly positive caps are stated explicitly. A zero or negative cap cannot admit a positive tolerance at that coordinate.
180 
181 \textbf{Constructive parameterization.} Write $t=1/\lambda$ and set
182 \[
183 u_e(t)=\min\{m_e,tc_e/s_e\},\qquad
184 \Phi(t)=\sum_e s_eu_e(t).
185 \]
186 Lean proves that $\Phi$ is continuous and nondecreasing, with $\Phi(0)=0$. At the finite positive scale
187 \[
188 T=\sum_e\frac{m_es_e}{c_e},
189 \]
190 every coordinate is saturated, so $u(T)=m$ and $\Phi(T)=\sum_es_em_e$. The intermediate value theorem produces $t>0$ with $\Phi(t)=\tau$. The multiplier is not assumed to exist.
191 
192 \textbf{Strictness below saturation.} If $t<u$ and $\Phi(t)$ is below the maximum, at least one coordinate is unsaturated at $t$. That coordinate strictly increases, and every other coordinate is nondecreasing. Hence $\Phi(t)<\Phi(u)$. This proves uniqueness of the scale and, by reciprocation, the exact manuscript statement
193 \[
194 \boxed{\exists!\lambda>0:\quad
195 \sum_e s_e\min\!\left\{m_e,\frac{c_e}{\lambda s_e}\right\}=\tau}
196 \]
197 when $0<\tau<\sum_es_em_e$.
198 
199 At the maximal budget, the minimizing vector remains unique but the multiplier need not be. The one-coordinate case $s=c=m=1$ is checked: both $\lambda=1$ and $\lambda=1/2$ produce the same tolerance $1$.
200 
201 
202 
203 \subsection{Clipped precision: global optimality}\label{supp4:subsection:006}\textit{Source item 8.5, continued}\par
204 Existence of a multiplier alone does not prove optimality. The formal proof supplies a global supporting inequality, rather than invoking an assumed Karush--Kuhn--Tucker optimality oracle.
205 
206 Fix the feasible vector $u=u(t)$ obtained above and any feasible competitor $\varepsilon$. For each coordinate, Lean proves
207 \[
208 \boxed{
209  c_e\left(\frac{\varepsilon_e}{u_e}-1\right)
210  \le \frac{s_e}{t}(\varepsilon_e-u_e).
211 }
212 \]
213 When $u_e=tc_e/s_e$, this is equality. When $u_e=m_e$, the capped condition implies $s_e/t\le c_e/m_e$, while $\varepsilon_e-m_e\le0$. Multiplying by this nonpositive difference gives the required inequality in the correct direction.
214 
215 The equal-budget constraint then yields
216 \[
217 \sum_e c_e\left(\frac{\varepsilon_e}{u_e}-1\right)
218 \le\frac1t\sum_e s_e(\varepsilon_e-u_e)=0.
219 \]
220 Applying the checked inequality $\log z\le z-1$ for $z>0$ gives
221 \[
222 \sum_e c_e\log(\varepsilon_e/u_e)\le0.
223 \]
224 Since
225 \[
226 J(\varepsilon)-J(u)
227 =-\sum_e c_e\log(\varepsilon_e/u_e),
228 \]
229 we obtain $J(u)\le J(\varepsilon)$ for every feasible competitor.
230 
231 If $\varepsilon\ne u$, one coordinate has ratio different from $1$. The logarithmic inequality is strict there, and its positive weight preserves strictness in the sum. Consequently,
232 \[
233 \boxed{\varepsilon\ne u\quad\Longrightarrow\quad J(u)<J(\varepsilon).}
234 \]
235 This proves the unique global minimizing vector for every positive feasible budget, including the maximal endpoint.
236 
237 \textbf{Numerical boundary.} Existence uses real continuity and the intermediate value theorem. This is a mathematical construction, not an executable floating-point multiplier search with a certified stopping tolerance. The companion exact-rational water-filling routine is an independent regression mirror and is not itself the compiled Lean construction.
238 
239 
240 
241 \subsection{Place in the finite development}\label{supp4:subsection:007}
242 Appendix E develops the remaining graph, schedule, counting and preconditioning constructions. Appendix F proves the global small-core recompression theorem from its stated factorization data.
243 
244 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