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{Exact semantics, support, and low-rank identities}\label{supp1:section:001}
2 This chapter retains the substantive mathematical pages of verification block 1 (v0.1.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{Exact packet semantics}\label{supp1:subsection:001}\textit{Source items 2.3, 2.5, and 2.6}\par
5 Let $R$ be a ring, $I$ a finite index type, and $(P_a)_{a\in I}$ a family satisfying
6 \[
7 P_bP_a=\begin{cases}P_a&b=a,\\0&b\ne a,\end{cases}
8 \qquad \sum_aP_a=1.
9 \]
10 Write $A_{ba}=P_bAP_a$ and let $E_A=\{(b,a):A_{ba}\ne0\}$. These are exact algebraic zeros, not values discarded by a floating-point threshold.
11 
12 \textbf{Reconstruction and action.} The checked finite sum is
13 \[
14 \boxed{A=\sum_{(b,a)\in E_A} A_{ba}.}
15 \]
16 The proof inserts the complete projector sum on both sides and removes only zero summands. Applying this identity to an arbitrary module gives exact action. A separate finite-matrix theorem establishes
17 \[
18 AZ=\sum_{(b,a)\in E_A}A_{ba}Z
19 \]
20 for every rectangular batch of right-hand sides $Z$.
21 
22 \textbf{Composition.} Inserting the projector identity between factors yields
23 \[
24 \boxed{(AB)_{ba}=\sum_c A_{bc}B_{ca}.}
25 \]
26 If the left side is nonzero, at least one intermediate $c$ has both $A_{bc}\ne0$ and $B_{ca}\ne0$. Consequently $\supp(AB)\subseteq\supp(A)\circ\supp(B)$. No equality of supports is asserted.
27 
28 \textbf{Adjoint and tensor products.} With an involution and self-adjoint projectors, the formalization proves
29 \[
30 (A_{ba})^*=(A^*)_{ab}.
31 \]
32 For actual finite matrices and actual Kronecker products, it proves
33 \[
34 (P_b\otimes Q_d)(A\otimes B)(P_a\otimes Q_c)
35 =A_{ba}\otimes B_{dc}.
36 \]
37 The self-adjointness hypothesis is explicit in the adjoint theorem. The tensor theorem is not a statement about an uninterpreted tensor symbol.
38 
39 \textbf{Concrete coordinates.} Given any tag map from finite scalar coordinates to packet addresses, \code{coordinatePackets} constructs diagonal zero-one matrices. Their orthogonality and completeness are proved. The construction allows unequal packet sizes and unused packet addresses. Its action is checked entrywise: it retains exactly the coordinates carrying the selected tag.
40 
41 The underlying ring-valued projector calculus is imported from the unchanged, freshly recompiled Paper VII foundation. Reuse is recorded separately from the new Paper VIII declarations.
42 
43 
44 
45 \subsection{Support propagation and nilpotence}\label{supp1:subsection:002}\textit{Source items 6.1, 6.2, and 6.3}\par
46 A path of length $n$ in the Lean predicate \code{TransferPath} is a directed walk: vertices may repeat. This is the notion required by matrix powers. At length zero the endpoints coincide. At length $n+1$, a nonzero last block is appended to a length-$n$ walk.
47 
48 Define the active contribution sum recursively by
49 \begin{align*}
50 F_0(b,a)&=\begin{cases}P_a&b=a,\\0&b\ne a,\end{cases}\\
51 F_{n+1}(b,a)&=\sum_{c:\,A_{bc}\ne0}A_{bc}F_n(c,a).
52 \end{align*}
53 The checked identity is
54 \[
55 \boxed{P_bA^nP_a=F_n(b,a)\qquad(n\ge0).}
56 \]
57 Its proof is induction using the exact composition theorem, not an assumed support recurrence. When no active walk exists, the corresponding contribution sum is zero, and hence the actual block of $A^n$ vanishes.
58 
59 \textbf{Nilpotence certificate.} If no walk of length $h+1$ exists between any pair of packets, then
60 \[
61 \boxed{A^{h+1}=0.}
62 \]
63 Every block vanishes, and reconstruction forces the whole operator to vanish. A second theorem derives the required absence of walks from a supplied level map
64 \[
65 \ell:I\longrightarrow\{0,\ldots,h\},\qquad
66 A_{bc}\ne0\ \Longrightarrow\ \ell(c)<\ell(b).
67 \]
68 It proves that a length-$n$ walk increases the level by at least $n$. This certifies the acyclic case with a bounded height. This block does not implement or verify an algorithm that constructs a topological ordering or computes the longest path.
69 
70 \textbf{Polynomial support.} For the actual finite sum
71 \[
72 p(A)=\sum_{j=0}^{d}c_jA^j,
73 \]
74 the checked support lies in the union of the support relations of the powers. The formalization treats the $j=0$ contribution explicitly, so the constant term is not accidentally omitted.
75 
76 \textbf{Cancellation control.} Lean verifies the rational example
77 \[
78 A=\begin{bmatrix}1&1\\-1&-1\end{bmatrix},\qquad A^2=0.
79 \]
80 The coordinate block $A_{00}$ is nonzero, and a length-two active walk from zero to zero exists. Nevertheless the corresponding block of $A^2$ is zero. This is an exact counterexample to replacing support inclusion by equality.
81 
82 
83 
84 \subsection{Low-rank algebra and inversion}\label{supp1:subsection:003}\textit{Source items 5.1, 5.3, and 5.4}\par
85 Let $A=D_A+U_AV_A^*$ and $B=D_B+U_BV_B^*$ have rectangular factor widths $r_A$ and $r_B$. The formalization constructs
86 \begin{align*}
87 U_C&=\begin{bmatrix}D_AU_B+U_A(V_A^*U_B)&U_A\end{bmatrix},\\
88 V_C&=\begin{bmatrix}V_B&D_B^*V_A\end{bmatrix}
89 \end{align*}
90 and proves
91 \[
92 \boxed{AB=D_AD_B+U_CV_C^*.}
93 \]
94 These are actual concatenated matrices with $r_B+r_A$ columns. Expanding the product and grouping the terms with common right factors proves the identity. The separate rank theorem establishes
95 \[
96 \rank(AB-D_AD_B)\le r_A+r_B.
97 \]
98 It bounds actual matrix rank, not just the number of stored columns. Packet diagonality of $D_AD_B$ follows from diagonality of both factors and the checked block-composition formula.
99 
100 \textbf{Woodbury.} For $D$ and
101 \[
102 S=I+V^*D^{-1}U
103 \]
104 both invertible, Lean checks the ordinary matrix inverse formula
105 \[
106 \boxed{(D+UV^*)^{-1}
107 =D^{-1}-D^{-1}US^{-1}V^*D^{-1}.}
108 \]
109 The proof specializes Mathlib's classical Woodbury identity. A separate theorem derives invertibility of $D+UV^*$ from the two stated assumptions. A further theorem verifies that multiplying the proposed inverse by any batch $Z$ solves the updated system. Invertibility of the update is not inserted as an extra premise.
110 
111 \textbf{Norm bound.} Over the real or complex scalars, all matrix norms in the following theorem are Hilbert-space operator norms, including the rectangular factors:
112 \[
113 \boxed{
114 \norm{(D+UV^*)^{-1}}
115 \le\norm{D^{-1}}+
116 \norm{D^{-1}U}\,\norm{S^{-1}}\,\norm{V^*D^{-1}}.
117 }
118 \]
119 After the checked inverse identity, the proof uses the triangle inequality and two rectangular operator-norm product bounds.
120 
121 \textbf{Not covered here.} The arbitrary product-chain rank corollary, optimal small-core recompression, singular-value approximation theorem, chain perturbation bounds, and numerical stability of a particular solve implementation are not marked complete by these results. Algebraic representability is not a GPU execution-time guarantee.
122 
123 
124 
125 \subsection{Packet perturbation certificates}\label{supp1:subsection:004}\textit{Source item 8.1 and two uniform consequences}\par
126 Let $X$ be a normed space over a nontrivially normed field. The formal objects are actual continuous linear maps $X\to X$, with their operator norm. Let $a(e)$ identify the source packet of edge $e$, and suppose
127 \[
128 \Delta_e=\Delta_e P_{a(e)}.
129 \]
130 Set
131 \[
132 A=\sum_e A_e,\qquad \widehat A=\sum_e(A_e+\Delta_e).
133 \]
134 The exact operator and vector identities are proved first:
135 \[
136 \widehat A-A=\sum_e\Delta_e P_{a(e)},\qquad
137 (\widehat A-A)x=\sum_e\Delta_e(P_{a(e)}x).
138 \]
139 Applying the finite triangle inequality and the defining operator-norm estimate gives
140 \[
141 \boxed{
142 \norm{(\widehat A-A)x}
143 \le\sum_e\norm{\Delta_e}\,\norm{P_{a(e)}x}.
144 }
145 \]
146 If $\norm{\Delta_e}\le\varepsilon_e\norm{A_e}$, then the formal relative certificate is
147 \[
148 \boxed{
149 \norm{(\widehat A-A)x}
150 \le\sum_e\varepsilon_e\norm{A_e}\,\norm{P_{a(e)}x}.
151 }
152 \]
153 The source additionally assumes that each exact block is source supported. The proof of this bound does not need that assumption. The checked statement therefore uses weaker sufficient hypotheses without weakening the conclusion.
154 
155 \textbf{Uniform operator estimates.} Two additional checked consequences are
156 \[
157 \norm{\widehat A-A}
158 \le\sum_e\norm{\Delta_e}\,\norm{P_{a(e)}}
159 \]
160 and, when $\norm{P_a}\le1$ for every packet,
161 \[
162 \boxed{\norm{\widehat A-A}\le\sum_e\norm{\Delta_e}.}
163 \]
164 These estimates are uniform in the input vector and can be used as inputs to later chain analyses. The chain results themselves are not included in this block's completed inventory.
165 
166 \textbf{Implementation boundary.} The maps $\Delta_e$ and their bounds must be supplied or justified for a numerical implementation. This formalization does not establish IEEE rounding behavior, prevent overflow or underflow, model a CUDA kernel, or certify the recorded device speedups. Those are distinct claims and require separate evidence.
167 
168 
169 
170 \subsection{Statement correction and verification}\label{supp1:subsection:005}\textit{Boundary audit for item 8.4; evidence for this release}\par
171 \textbf{Positive budget is necessary.} The source minimizes
172 \[
173 \sum_e c_e\log\frac1{\varepsilon_e},\qquad
174 \varepsilon_e>0,\qquad \sum_e s_e\varepsilon_e=\tau,
175 \]
176 with positive sensitivities and costs, but it does not explicitly impose $\tau>0$. For a nonempty edge set, Lean proves
177 \[
178 s_e>0\ \text{and}\ \varepsilon_e>0\ \text{for all }e
179 \quad\Longrightarrow\quad
180 \sum_e s_e\varepsilon_e>0.
181 \]
182 It follows that every nonpositive budget is infeasible. A one-edge, unit-sensitivity, zero-budget instance is checked as an exact boundary example.
183 
184 The amended nonempty-index statement should require $\tau>0$. Nonemptiness also makes the sum of positive costs in the displayed optimizer's denominator positive. The empty edge set should be treated separately. \textbf{Existence, optimality, and uniqueness of the corrected optimizer are not proved in this release.} Item 8.4 remains boundary-audit-only.
185 
186 \textbf{Fresh Lean run.} All six modules completed with exit code zero under Lean 4.34.0-rc2 and Mathlib revision
187 \begin{center}\code{aeb72f1e9981b6d35b426b16dca7759be3e7ba06}.
188 \end{center}
189 All 60 theorem-level audits and the separate coordinate-projector construction audit use only \code{propext}, \code{Classical.choice}, and \code{Quot.sound}. Warnings were treated as errors. The deliberately false equality and the deliberate admitted-proof placeholder were both rejected. All 17 verifier regression tests passed.
190 
191 \textbf{Failures are retained.} Nine of the 15 captured development checks failed before correction. Their snapshots and compiler logs remain separate from the active modules and the successful final run. The initial long runtime-extraction command was also interrupted by the host limit. A second extraction completed, and the final run verified the restored runtime and dependency pins.
192 
193 \textbf{Reproducibility.} The release includes exact sources, module-level commands, source and compiled-artifact hashes, axiom logs, the complete source-result coverage ledger, and a checkpointed verifier. The original CPU suite passed 37,392 checks. It does not reproduce GPU timings.
194 
195 \textbf{Remaining scope.} Forty-six manuscript-proved items remain not fully covered, plus four separately tracked classical inputs. Mathlib's imported proofs were not independently rechecked, and earlier papers were not rebuilt in full. The next work can build on these semantics to address the cost models, compiler, recompression, and numerical-analysis statements without treating empirical performance as a theorem.

Back to source controls

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