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{Structured transforms and clipped precision}\label{supp4:section:001}
2 This chapter retains the substantive mathematical pages of verification block 4 (v0.4.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{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$; 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 logarithmic re-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; 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{Verification, regressions, and remaining work}\label{supp4:subsection:007}\textit{Cumulative release evidence}\par
242 \textbf{Lean verification.} All 23 modules were rebuilt in a fresh output directory under Lean 4.34.0-rc2 and Mathlib revision
243 \begin{center}\code{aeb72f1e9981b6d35b426b16dca7759be3e7ba06}.\end{center}
244 Every final module returned exit code zero, with warnings treated as errors. The 247 theorem audits and 22 construction audits used only \code{propext}, \code{Classical.choice}, and \code{Quot.sound}, or subsets thereof. Active proof sources contain no admitted proofs or added axioms. The false-equality and admitted-proof negative controls were rejected. All 17 verifier regression tests passed.
245 
246 \textbf{Development failures.} Of 20 captured development checks in this block, 12 failed and eight passed. Failures included incomplete development lemmas, import visibility, finite-index instance reduction, and warning diagnostics. Failed source snapshots and compiler logs are retained separately from the successful fresh cumulative run. The first request for interactive runtime recovery was unsupported; noninteractive archive assembly and extraction succeeded, with every part hash and the combined hash verified.
247 
248 \textbf{Independent regressions.} The Python mirrors passed 180 exact-rational Kronecker cases, 120 tensor cases, 96 Walsh cases, 240 Toeplitz cases, and 600 clipped-allocation cases. The latter include 60 maximal-budget cases and 1,800 rejected infeasible budgets. These are finite checks, not additional universal theorems or executions of the Lean definitions.
249 
250 A separate complex128 Fourier regression covered 96 cases at lengths 1 through 24. Maximum absolute errors were approximately $3.34\times10^{-14}$ for diagonalization, $2.98\times10^{-15}$ for unitarity, and $2.04\times10^{-13}$ for application, all below the declared $10^{-10}$ threshold. These numerical checks are not substituted for the symbolic Lean proof.
251 
252 \textbf{Ten manuscript-proved items remain:}
253 \begin{center}\small
254 \begin{tabular}{@{}lp{.79\textwidth}@{}}
255 \toprule
256 Item & Remaining result\\\midrule
257 4.1 & Equal block banded count\\
258 5.6 & Small-core optimal recompression\\
259 6.5, 6.6 & Triangular level solve and sequential depth\\
260 6.7, 6.8 & Inverse and Schur support inclusion\\
261 7.4, 7.6 & Block-Jacobi condition bound and certified preconditioning\\
262 9.2 & Exact block-discovery certificate\\
263 10.3 & Acyclic schedule depth\\\bottomrule
264 \end{tabular}
265 \end{center}
266 Four classical inputs remain separately recorded. This release does not rerun the original numerical corpus or GPU benchmarks, rebuild Papers I--VII in full, or independently recheck every imported Mathlib proof.
267 

Back to source controls

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