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{Product chains, Krylov spaces, and integer budgets}\label{supp3:section:001}
2 This chapter retains the substantive mathematical pages of verification block 3 (v0.3.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{Low-rank factors through a product chain}\label{supp3:subsection:001}\textit{Source item 5.2}\par
5 Let
6 \[
7 A_j=D_j+U_jV_j^*,\qquad U_j,V_j\in\mathbb C^{n\times r_j},
8 \]
9 with all $D_j$ diagonal in one packet layout. Set
10 \[
11 P_m=A_m\cdots A_1,\qquad D^{(m)}=D_m\cdots D_1.
12 \]
13 The formalization constructs thin matrices $L_m,R_m$ such that
14 \[
15 \boxed{P_m=D^{(m)}+L_mR_m^*.}
16 \]
17 Their column index type is a recursively constructed disjoint sum. Its cardinality is proved to equal $\sum_{j=1}^m r_j$.
18 
19 \textbf{Construction.} Suppose $P_{m-1}=D^{(m-1)}+L_{m-1}R_{m-1}^*$. The new factors are
20 \begin{align*}
21 L_m&=\bigl[D_mL_{m-1}+U_m(V_m^*L_{m-1})\quad U_m\bigr],\\
22 R_m&=\bigl[R_{m-1}\quad (D^{(m-1)})^*V_m\bigr].
23 \end{align*}
24 Substitution into the already checked two-factor product identity proves exactness. This is not a rank-only existence argument. The recursively defined factors are themselves audited.
25 
26 Applying the ordinary matrix-rank inequality gives
27 \[
28 \boxed{\operatorname{rank}(P_m-D^{(m)})\leq\sum_{j=1}^m r_j.}
29 \]
30 The bound concerns the actual correction matrix, not just the number of allocated columns. The proof also shows that $D^{(m)}$ stays packet diagonal. The empty chain has identity base, empty column type, and zero correction. Individual $r_j=0$ are permitted.
31 
32 \textbf{What is not completed here.} This is an unrecompressed representation. Optimal small-core singular-value recompression, item 5.6, remains separate. The construction can accumulate redundant columns and is not a claim of minimal factor width.
33 
34 \subsubsection{Actual noncommutative products}
35 The error module defines the left-accumulated product recursively, with $P_0=I$ and $P_{j+1}=A_{j+1}P_j$. For a perturbed sequence $\widehat A_j$, it derives the discrepancy recursion
36 \[
37 \widehat P_{j+1}-P_{j+1}
38 =\widehat A_{j+1}(\widehat P_j-P_j)
39  +(\widehat A_{j+1}-A_{j+1})P_j.
40 \]
41 The identity follows from the actual products. It is not supplied as an assumption to a norm estimate, and it does not commute the operators. Lean uses zero-based indices internally, so index $j$ in source code corresponds to manuscript factor $j+1$.
42 
43 
44 
45 \subsection{Error propagation and recompression}\label{supp3:subsection:002}\textit{Source items 5.8, 5.9, and 8.3}\par
46 For $\widehat A_j=A_j+E_j$, the checked product-chain bound is
47 \[
48 \boxed{
49 \norm{\widehat A_m\cdots\widehat A_1-A_m\cdots A_1}
50 \leq\sum_{j=1}^m
51  \left(\prod_{i=j+1}^m\norm{\widehat A_i}\right)
52  \norm{E_j}
53  \left(\prod_{i=1}^{j-1}\norm{A_i}\right).}
54 \]
55 Empty products are one. The proof first solves a scalar gain recurrence as a finite sum, then bounds the actual discrepancy recursion by it. A version with certified upper bounds $\delta_j\geq\norm{E_j}$ is included. The product-norm argument uses a norm-one identity, as in operators on a nonzero normed space.
56 
57 \textbf{Post-product recompression is different.} Define the implemented iterates by
58 \[
59 \widetilde P_0=I,\qquad
60 \widetilde P_j=A_j\widetilde P_{j-1}+E_j.
61 \]
62 Here $E_j$ is a residual introduced after multiplication. Lean derives
63 \[
64 \widetilde P_j-P_j=A_j(\widetilde P_{j-1}-P_{j-1})+E_j
65 \]
66 and proves
67 \[
68 \boxed{\norm{\widetilde P_m-P_m}
69 \leq\sum_{j=1}^m\left(\prod_{i=j+1}^m\norm{A_i}\right)\delta_j,
70 \quad \norm{E_j}\leq\delta_j.}
71 \]
72 This theorem works in a normed ring without the extra norm-one condition. It includes the empty iteration. There is no exact-prefix factor in the local residual term, because the residual is already measured at the post-product output.
73 
74 \textbf{Packetwise mixed precision.} At each stage let
75 \[
76 A_j=\sum_e A_{j,e},\qquad
77 \widehat A_j=\sum_e(A_{j,e}+\Delta_{j,e}),\qquad
78 \Delta_{j,e}=\Delta_{j,e}P_{j,a(e)}.
79 \]
80 The previous packet certificate supplies the uniform operator bound
81 \[
82 \norm{\widehat A_j-A_j}\leq
83 \delta_j:=\sum_e\norm{\Delta_{j,e}}\norm{P_{j,a(e)}}.
84 \]
85 The new theorem substitutes these $\delta_j$ into the actual product-chain estimate. The resulting vector error is at most the operator certificate times $\norm{x}$. A vector-specific packet bound is not silently reused as an operator norm.
86 
87 These are deterministic implications from stated residual bounds. They do not establish the rounding behavior of a floating-point kernel. The floating-point matrix-product model remains one of the separately tracked classical inputs.
88 
89 
90 
91 \subsection{Exact and approximate packet Krylov spaces}\label{supp3:subsection:003}\textit{Source items 7.2 and 7.3}\par
92 Write
93 \[
94 \mathcal K_m(A,v)=\operatorname{span}\{v,Av,\ldots,A^{m-1}v\}.
95 \]
96 For a complete finite projector family $P_i$, suppose $A$ commutes with every $P_i$. Let $A_i=P_iAP_i$. Lean proves the actual orbit identity
97 \[
98 A^jv=\sum_i A_i^jP_iv
99 \]
100 and therefore
101 \[
102 \boxed{\mathcal K_m(A,v)\subseteq
103 \bigoplus_i\mathcal K_m(A_i,P_iv).}
104 \]
105 The case $j=0$ uses $\sum_iP_i=I$. The zeroth local power is the ambient identity, applied to $P_iv$, rather than an incorrectly substituted local projector power.
106 
107 \textbf{The direct sum is justified.} Each local space is proved to lie in the actual range of $P_i$. Projecting a finite sum of local vectors selects its $i$th summand. Consequently a zero sum of local vectors has every summand zero. The proof does not assert equality between the global Krylov space and the full sum of local Krylov spaces.
108 
109 For approximate invariance let $A=D+K$, where $D$ is packet diagonal, and set
110 \[
111 M=\max\{\norm{A},\norm{D}\}.
112 \]
113 For every positive integer $j$, the operator estimate is
114 \[
115 \boxed{\norm{A^j-D^j}\leq jM^{j-1}\norm{K}.}
116 \]
117 The proof is noncommutative and uses actual powers. Its positive-index version works even in a trivial normed ring. No division by $M$ is used, so $M=0$ causes no exception.
118 
119 Define the comparison space
120 \[
121 \mathcal L_{j+1}=\bigoplus_i\mathcal K_{j+1}(P_iDP_i,P_iv).
122 \]
123 Packet diagonality is first shown to imply commutation. The exact theorem then proves $D^jv\in\mathcal L_{j+1}$. Using that vector as a witness in the infimum distance gives
124 \[
125 \boxed{\operatorname{dist}(A^jv,\mathcal L_{j+1})
126 \leq jM^{j-1}\norm{K}\norm{v}.}
127 \]
128 This statement uses Lean's actual metric infimum distance to the subspace. It does not assume that the comparison vector lies there. The block-Jacobi condition bound and the preconditioned conjugate-gradient corollary are not completed by these Krylov results.
129 
130 
131 
132 \subsection{Integer error budgets and discrete precision}\label{supp3:subsection:004}\textit{Source item 8.7 and common minimum machinery}\par
133 The finite budget programs use integer weights and exact ordered-field costs. They apply to rational costs for execution and to real costs for mathematical statements. Unreachable states are represented by \code{none}, not by a large finite sentinel.
134 
135 For a predicate $S$ on costs, the common minimum specification means:
136 \[
137 \begin{array}{ll}
138 \code{none}: & \text{no cost satisfies }S,\\
139 \code{some}(v): & S(v)\text{ and }v\leq z\text{ whenever }S(z).
140 \end{array}
141 \]
142 Both attainment and minimality are included. Optional minimum and optional addition are proved to implement union and independent sum of feasible sets.
143 
144 For exact-weight tables $F,G$, min-plus convolution is
145 \[
146 (F\star G)(b)=\min_{0\leq k\leq b}\{F(k)+G(b-k)\},
147 \]
148 with an infeasible sum whenever either operand is infeasible. Its correctness theorem identifies every finite answer with an actual feasible pair of component weights and costs. Repeated convolution handles arbitrary finite lists of components.
149 
150 \textbf{Independent precision assignments.} For every edge, a finite list contains its permitted pairs $(w,c)$ of quantized error and cost. The legal assignment type chooses exactly one listed pair per edge. It is defined independently of the dynamic program. Costs and weights are then summed over that assignment.
151 
152 If $D$ is the already-solved tail table, the next edge has exact-weight recurrence
153 \[
154 F(b)=\min_{(w,c)\text{ allowed},\;w\leq b}\{D(b-w)+c\}.
155 \]
156 The final answer is $\min_{0\leq b\leq B}F(b)$. Lean proves that this is the exact minimum over legal assignments with total error at most $B$, or \code{none} exactly when no such assignment exists.
157 
158 \textbf{The subtraction guard matters.} Natural subtraction truncates at zero. Without the condition $w\leq b$, an option of weight one could be accepted at budget zero. The implemented program checks the condition before subtraction. Dedicated regressions also cover a zero-weight option, an empty option set, and the empty collection of edges. The last case has cost and error zero.
159 
160 This result does not prove that an unquantized physical error model is accurately represented by integer weights. The formal optimum concerns the declared quantized model. Clipped continuous allocation, item 8.5, remains separate.
161 
162 
163 
164 \subsection{The quantized packet-tree compiler}\label{supp3:subsection:005}\textit{Source item 9.8}\par
165 The new program uses the previous block's actual finite \code{CandidateTree} and independent legal \code{Cut} type. An internal node has any nonempty finite family of children. A cut either keeps its node or chooses a legal cut in every child. A terminal node can only be kept.
166 
167 Keeping node $v$ costs $\kappa_v$ and incurs integer error $w_v$. Splitting costs overhead $\sigma_v$ in addition to the selected child cuts. The exact-weight recurrence is
168 \[
169 F_v(b)=\min\left\{
170 \begin{array}{l}
171 \kappa_v\quad\text{if }b=w_v,\\[2pt]
172 \displaystyle\sigma_v+
173 \min_{\sum_i b_i=b}\sum_iF_{v_i}(b_i)\quad\text{if }v\text{ is internal}.
174 \end{array}\right.
175 \]
176 Nonexistent alternatives are infeasible. The child sum is implemented by the proved finite min-plus convolution, not by assuming an optimal allocation.
177 
178 \textbf{Exact semantics.} For every tree and every integer weight $b$, Lean proves that $F_v(b)$ is a minimum of costs of independent legal cuts of exact weight $b$. Thus each finite answer has an attaining cut and is a lower bound for every other legal cut at that weight. Infeasibility is equivalent to the absence of such a cut.
179 
180 The root scan
181 \[
182 \boxed{\min_{0\leq b\leq B}F_{\mathrm{root}}(b)}
183 \]
184 is therefore the exact budget-constrained optimum. Increasing the budget cannot increase a finite optimum. The theorem retains feasibility hypotheses where necessary rather than treating \code{none} as an ordinary real cost.
185 
186 \textbf{Why the budget program adds something.} Consider the three admissible cost/error pairs
187 \[
188 (0,4),\qquad(3,2),\qquad(4,0).
189 \]
190 At budget two the answer is cost three. The middle pair cannot minimize cost plus $\lambda$ times error: comparison with the first pair would require $\lambda\geq3/2$, while comparison with the third would require $\lambda\leq1/2$. The executable suite checks the budget answer on an actual unary candidate tree with these cuts. It is not obtained merely by varying the previous Lagrangian compiler's multiplier.
191 
192 \textbf{Output boundary.} This budget implementation returns the minimum cost or \code{none}. Attainment is proved, but executable backtracking metadata for a selected cut is not yet returned. Universal packet discovery, overlapping decompositions, nonadditive cache costs, and arbitrary device scheduling remain outside the theorem.
193 
194 
195 
196 \subsection{Cached arrays and a work certificate}\label{supp3:subsection:006}\textit{Source item 9.9 and implemented forms of 8.7 and 9.8}\par
197 A recursive value equation alone need not be an efficient program. Repeated calls can recompute the same subtree table. The new implementation therefore stores each table as an array-backed \code{Vector} with exactly $B+1$ optional entries.
198 
199 Each child table is evaluated and cached before the parent merges it. A merge reads two existing tables and tabulates their convolution. The discrete precision program likewise computes its tail table once before filling the next edge's table. The final scan reads the stored root or final-edge table.
200 
201 \textbf{Entrywise implementation theorem.} For every $b\leq B$, Lean proves
202 \[
203 \operatorname{lookup}(\operatorname{storedTree}(B,t),b)=F_t(b).
204 \]
205 There is a parallel theorem for stored discrete precision. The proof establishes first that an output entry at $b$ depends only on input entries at most $b$, then proceeds through cached convolution and the tree recursion. Consequently the optimality, attainment, and infeasibility specification applies to the actual stored result.
206 
207 \textbf{Counted candidates.} One full convolution table examines indices
208 \[
209 (b,k),\qquad 0\leq b\leq B,\quad0\leq k\leq b.
210 \]
211 These form a concrete finite dependent-sum type. Its cardinality is proved to be
212 \[
213 \sum_{b=0}^B(b+1)\leq(B+1)^2.
214 \]
215 For a nonempty finite tree, the number of child merges plus one equals the node count $N$. This identity is proved for arbitrary finite branching.
216 
217 Let $W_B(t)$ be the declared unit-cost count of table-cell constructions and tested min-plus candidates. The model charges the empty child-combination table as well as the output cells and merge candidates. Lean proves
218 \[
219 W_B(t)\leq2(B+1)N+\bigl((B+1)+(B+1)^2\bigr)(N-1)
220 \]
221 and hence
222 \[
223 \boxed{W_B(t)\leq N\bigl(3(B+1)+(B+1)^2\bigr).}
224 \]
225 The root minimum scan adds a linear pass. Thus the declared tabulation model is pseudo-polynomial in $N$ and the numeric budget $B$.
226 
227 \textbf{Scope of this certificate.} These are table and candidate counts, not a measured execution trace or a theorem about every instruction emitted by the compiler. Rational bit complexity, allocation overhead, memory traffic, and hardware timing are not included. The certificate is not polynomial in the binary input length of $B$.
228 
229 
230 
231 \subsection{Verification, executable checks, and remaining work}\label{supp3:subsection:007}\textit{Release evidence and precise completion boundary}\par
232 The fresh cumulative run used \textbf{Lean 4.34.0-rc2} and pinned Mathlib revision
233 \begin{center}\code{aeb72f1e9981b6d35b426b16dca7759be3e7ba06}.\end{center}
234 All 18 modules returned exit code zero with warnings treated as errors. Every one of the 197 theorem audits used only \code{propext}, \code{Classical.choice}, and \code{Quot.sound}, or subsets thereof. Twelve constructions were separately audited. The active proof files contain no admitted proofs or added axiom declarations. The deliberately false equality and admitted-proof control were both rejected.
235 
236 \textbf{Exact-rational executable suite.} Independent enumeration, rather than the DP recurrence, produces the candidate costs used for comparison.
237 \begin{center}\small
238 \renewcommand{\arraystretch}{1.18}
239 \begin{tabular}{@{}p{.70\textwidth}r@{}}
240 \toprule
241 New test category & Count\\
242 \midrule
243 Tree instances with unary, binary, ternary, and mixed branching & 384\\
244 Exact-weight table comparisons for trees & 4,992\\
245 Budget-minimum comparisons for trees & 4,992\\
246 Independently enumerated legal cuts & 19,152\\
247 Additional functional-specification comparisons & 1,440\\
248 Discrete precision instances & 288\\
249 Exact-weight / budget comparisons for precision & 3,744 each\\
250 Independently enumerated legal assignments & 1,453\\
251 Explicit boundary regressions & 5\\
252 \bottomrule
253 \end{tabular}
254 \end{center}
255 All passed. The preceding block's 600 compiler cases, 85,320 enumerated pruning scores, and 600 cached-update comparisons were also rerun and passed. These counts describe executable tests, not additional theorem declarations.
256 
257 \textbf{Failures retained.} Eleven of 18 captured development compilation checks failed before correction. Their source snapshots and diagnostics are retained separately from the successful final run. They principally concern type elaboration, module visibility, finite indices, and simplification. An unsupported interactive runtime-recovery request failed before assembly started. The later noninteractive restoration succeeded.
258 
259 \textbf{Sixteen manuscript-proved items remain:} 4.1, 4.3--4.7, 5.6, 6.5--6.8, 7.4, 7.6, 8.5, 9.2, and 10.3. These concern structured spectral and tensor primitives, optimal recompression, graph scheduling and inverse support, preconditioning, clipped allocation, and block-discovery certificates. Four classical inputs are still separate.
260 
261 No GPU timings, original CPU numerical suite, full Papers I--VII rebuild, or independent recheck of imported Mathlib proofs was performed in this block. The JSON verification report, execution reports, preservation report, source ledger, logs, and scripts provide the auditable release record.

Back to source controls

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