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{Exact semantics, support, and low-rank identities}\label{supp1:section:001}
2 This appendix develops exact packet semantics, support propagation, low-rank algebra and error models. Positive-budget conditions are isolated before the allocation theorem in Appendix B.\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 Chapter VII foundation, which was recompiled in the recorded formal run. Reuse is recorded separately from the new Chapter 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{Positive budget and feasibility}\label{supp1:subsection:005}\textit{Positive-budget condition for item 8.4}\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. The positive-budget condition is essential. 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 nonempty-index statement requires $\tau>0$. Nonemptiness also makes the sum of positive costs in the displayed optimizer's denominator positive. The empty edge set is treated separately. Existence, global optimality and uniqueness for the positive-budget problem are proved in Section~\ref{supp2:subsection:004}.
185 

Back to source controls

Back to Realization Calculus