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{Constructed graph schedules, support, and preconditioning}\label{supp5:section:001}
2 This appendix develops support bounds, graph schedules, block discovery and preconditioning certificates. Classical algorithmic inputs remain separate from the finite certificates proved here.\par
3 
4 \subsection{Constructing the optimal level schedule}\label{supp5:subsection:001}\textit{Source items 6.6 and 10.3; module GraphSchedules}\par
5 Let $V$ be finite and let $u\to v$ mean that task $v$ depends on task $u$. Assume there is no nonempty directed cycle. A topological order or valid level function is \emph{not} supplied as an additional hypothesis.
6 
7 For each vertex, define its strict ancestor set
8 \[
9 \operatorname{Anc}(v)=\{u:\text{there is a positive-length path }u\leadsto v\}.
10 \]
11 For every edge $u\to v$, the proof establishes
12 \[
13 \operatorname{Anc}(u)\subsetneq\operatorname{Anc}(v).
14 \]
15 The inclusion follows by appending the edge. It is strict because $u$ is an ancestor of $v$ but cannot be its own strict ancestor in an acyclic graph. Cardinality therefore decreases when following predecessors. This constructs a well-founded relation on which the level recursion is defined:
16 \[
17 \boxed{\ell(v)=1+\max_{u\to v}\ell(u),\qquad \max\varnothing=0.}
18 \]
19 
20 \textbf{Validity and attainment.} Lean proves $\ell(v)>0$ and $\ell(u)<\ell(v)$ on every edge. A path of $n$ edges from $a$ to $b$ satisfies
21 \[
22 \ell(a)+n\leq\ell(b).
23 \]
24 Conversely, predecessor-max attainment and induction produce an actual path with $\ell(v)-1$ edges ending at each vertex $v$. The result is an equality with a longest path, not merely an upper bound.
25 
26 A valid schedule $s:V\to\mathbb N$ assigns positive stages and strictly increases on each edge. Induction proves the stronger pointwise statement
27 \[
28 \ell(v)\leq s(v)\quad\text{for every }v.
29 \]
30 Consequently the constructed schedule achieves the least possible makespan,
31 \[
32 \boxed{d=\max_{v\in V}\ell(v).}
33 \]
34 For a nonempty graph, $d$ equals the number of vertices on an attained longest path. Vertices of the same level have no dependency edge in either direction.
35 
36 \textbf{Empty graph and interpretation.} When $V=\varnothing$, the checked depth is zero. The phrase ``one plus the longest edge-path length'' applies to nonempty graphs. These are ideal discrete scheduling statements. Weighted task costs, a finite processor budget, launch latency and communication are not part of this model. The definitions are mathematical constructions, not a certified hardware scheduler.
37 
38 
39 
40 \subsection{Forward substitution with an actual stage evaluator}\label{supp5:subsection:002}\textit{Source item 6.5; module TriangularSolve}\par
41 Use the graph and levels constructed on the previous page. A vertex $v$ carries an arbitrary vector space $X_v$ over a field. The spaces may have different dimensions. Let
42 \[
43 D_v:X_v\overset{\sim}{\longrightarrow}X_v,
44 \qquad T_{vu}:X_u\longrightarrow X_v
45 \]
46 be an invertible diagonal map and linear transfer maps. The operator being solved is defined by its actual block action:
47 \[
48 (Ax)_v=D_vx_v+\sum_{u\to v}T_{vu}x_u.
49 \]
50 No solution, solve equation or precomputed topological certificate is assumed.
51 
52 \textbf{Constructed solution.} Well-founded recursion defines
53 \[
54 \boxed{x_v=D_v^{-1}\!\left(b_v-\sum_{u\to v}T_{vu}x_u\right).}
55 \]
56 Applying $D_v$ proves the original equation at $v$. If another vector satisfies all equations, induction over predecessors makes each previously used coordinate identical, and invertibility of $D_v$ forces agreement at $v$. Thus the construction gives existence and uniqueness, and the block operator is bijective.
57 
58 \textbf{Parallel stages.} A second, independent definition is an explicit staged evaluator. Set $x^{(0)}=0$ and
59 \[
60 x^{(k+1)}_v=
61 \begin{cases}
62 D_v^{-1}\!\left(b_v-\displaystyle\sum_{u\to v}T_{vu}x^{(k)}_u\right),
63   &\ell(v)=k+1,\\[5pt]
64 x^{(k)}_v,&\ell(v)\ne k+1.
65 \end{cases}
66 \]
67 It reads the previous-stage vector, not partially updated coordinates. The invariant is
68 \[
69 \ell(v)\leq k\quad\Longrightarrow\quad x^{(k)}_v=x_v.
70 \]
71 Every predecessor of a level-$k+1$ vertex has level at most $k$, so the recurrence uses only coordinates already proved correct. At the canonical depth $d$ this yields
72 \[
73 \boxed{Ax^{(d)}=b.}
74 \]
75 The local independence theorem separately proves that changing coordinates outside the strict earlier levels cannot change a vertex's local solve.
76 
77 \textbf{Scope.} Diagonal invertibility is expressed by genuine linear equivalences. The task graph may include declared transfers whose values happen to be zero. Optimality refers to that declared dependency graph. Exact field arithmetic and exact local inverses are used. No floating-point stability or implementation-specific parallel speed is inferred.
78 
79 
80 
81 \subsection{Support of inverses and Schur elimination}\label{supp5:subsection:003}\textit{Source items 6.7 and 6.8; modules InverseSupport and SchurSupport}\par
82 Let $(P_a)$ be a complete idempotent packet family in a finite-dimensional algebra. Define $a\leadsto b$ by an actual finite path through nonzero blocks $P_bAP_a$. \textbf{Zero-length paths are included}, so every packet reaches itself.
83 
84 Fix the source packet $a$. In the regular representation, define the submodule
85 \[
86 W_a=\{x:P_bx=0\ \text{whenever }a\not\leadsto b\}.
87 \]
88 It contains $P_a$. Completeness of the projectors expands each component of $Ax$ into packet transfers. If a transfer into an unreachable packet were nonzero from a reachable packet, it would extend a path, a contradiction. Thus $AW_a\subseteq W_a$.
89 
90 Suppose $BA=I$. Left multiplication by $A$ is injective, including on $W_a$. Finite dimensionality makes that restricted map surjective. Given $x\in W_a$, choose $y\in W_a$ with $Ay=x$. Then $Bx=BAy=y\in W_a$. Applying this to $P_a$ proves
91 \[
92 \boxed{a\not\leadsto b\quad\Longrightarrow\quad P_bBP_a=0.}
93 \]
94 The matrix specialization takes $B$ to Mathlib's actual nonsingular matrix inverse, with an invertible determinant. No inverse-sparsity hypothesis is inserted.
95 
96 \textbf{Hidden elimination.} For the actual Schur complement
97 \[
98 S=A_{RR}-A_{RH}A_{HH}^{-1}A_{HR},
99 \]
100 the hidden inverse is expanded through the hidden projectors. A nonzero retained correction block requires indices $j,k$ with nonzero entrance and exit blocks and a hidden path $j\leadsto k$. Therefore a nonzero block $S_{ba}$ requires either a direct retained block, or
101 \[
102 a\longrightarrow j\ \leadsto_{H}\ k\longrightarrow b.
103 \]
104 The entrance and exit matrices may be rectangular. Retained and hidden coordinate sizes and packet systems are independently typed. The hidden matrix must be invertible. A zero-length hidden path permits entrance and exit through the same hidden packet.
105 
106 \textbf{Inclusion is not equality.} Cancellation can remove a block permitted by a graph route. For example,
107 \[
108 A=\begin{pmatrix}1&1&1\\0&1&1\\0&0&1\end{pmatrix}
109 \quad\text{has}\quad (A^{-1})_{13}=0
110 \]
111 despite a direct nonzero $(1,3)$ block. The implementation proves support inclusion and the corresponding no-route zero certificate, not a converse.
112 
113 
114 
115 \subsection{Exact banded addresses and modeled work}\label{supp5:subsection:004}\textit{Source item 4.1; module BandedCount}\par
116 For $p$ packets and half-bandwidth $w$, the actual address set is
117 \[
118 \mathcal B_{p,w}
119 =\{(i,j)\in\{0,\ldots,p-1\}^2:
120  i\leq j+w\ \text{and}\ j\leq i+w\}.
121 \]
122 The predicate is the integer version of $|i-j|\leq w$. The count is first defined as a double sum of indicators, then identified with the cardinality of this subtype. It is not defined by the target closed form.
123 
124 Under $0\leq w<p$, the formal proof establishes
125 \[
126 \boxed{N_{p,w}=|\mathcal B_{p,w}|=p(2w+1)-w(w+1).}
127 \]
128 The proof uses finite prefix counting, the newly exposed boundary row and column when $p$ increases, and the saturated initial band. An intermediate subtraction-free identity avoids relying on natural-number subtraction without the required inequality. The diagonal case $w=0$ gives exactly $p$ blocks, and the saturated case $w=p-1$ gives $p^2$.
129 
130 \textbf{Stored scalars.} With equal block width $b$, the storage-address type is
131 \[
132 \mathcal S=\mathcal B_{p,w}\times\{0,\ldots,b-1\}^2.
133 \]
134 Its cardinality is the actual number of represented scalar entries:
135 \[
136 \boxed{|\mathcal S|=b^2N_{p,w}.}
137 \]
138 
139 \textbf{Arithmetic events.} For $q$ right-hand sides, the declared event type adds a right-hand-side index and one of two operation roles, multiplication or accumulation:
140 \[
141 \mathcal O=\{0,1\}\times\{0,\ldots,q-1\}\times\mathcal S.
142 \]
143 Hence
144 \[
145 \boxed{|\mathcal O|=2qb^2N_{p,w}.}
146 \]
147 These identities include zero right-hand-side count. The abstract storage formula also admits zero block width. To use the manuscript's substitution $p=n/b$, one must separately require $b>0$ and $n=pb$.
148 
149 \textbf{Boundary.} Two events per coefficient and right-hand side are a declared arithmetic convention. These counts do not identify the number of CUDA instructions, account for fused multiply-add lowering, price complex arithmetic in real operations, or include allocation, indexing, communication and launch overhead. They are also not a performance comparison with dense multiplication.
150 
151 
152 
153 \subsection{Exact residual certificates for supplied packets}\label{supp5:subsection:005}\textit{Source item 9.2; module DiscoveryCertificate}\par
154 Let $(P_a)$ be a complete orthogonal projector system on a finite complex coordinate space. The projectors need not be coordinate masks. For an actual matrix $A$, define
155 \[
156 \Pi(A)=\sum_aP_aAP_a,
157 \qquad E=A-\Pi(A).
158 \]
159 Reconstruction gives the exact off-diagonal residual
160 \[
161 E=\sum_{b\ne a}P_bAP_a.
162 \]
163 
164 \textbf{Hilbert--Schmidt orthogonality.} For distinct ordered packet pairs $(b,a)\ne(d,c)$, adjoint multiplication and projector orthogonality give
165 \[
166 \operatorname{tr}\bigl((P_bAP_a)^*P_dBP_c\bigr)=0.
167 \]
168 If $b\ne d$, the central projector product vanishes. Otherwise $a\ne c$, and cyclicity of trace brings $P_cP_a$ together. This is proved for arbitrary input matrices $A,B$.
169 
170 Lean identifies the actual Frobenius norm with its trace expression,
171 \[
172 \norm{M}_{\rm F}^2=\operatorname{Re}\operatorname{tr}(M^*M),
173 \]
174 then expands the finite sum and removes each cross term. The result is
175 \[
176 \boxed{\norm{A-\Pi(A)}_{\rm F}^2
177 =\sum_{b\ne a}\norm{P_bAP_a}_{\rm F}^2.}
178 \]
179 No Pythagorean equality for the target residual is assumed.
180 
181 \textbf{Operator norm.} In a separate scoped matrix norm, the triangle inequality gives
182 \[
183 \boxed{\norm{A-\Pi(A)}_2
184 \leq\sum_{b\ne a}\norm{P_bAP_a}_2.}
185 \]
186 Here $\norm{\cdot}_2$ is the Euclidean induced operator norm, not the Frobenius norm. The formal declarations use distinct norm instances, preventing the two certificates from being conflated. Self-adjointness is used for Frobenius orthogonality. The sum estimate itself requires only the complete packet decomposition.
187 
188 \textbf{Discovery boundary.} This result certifies the residual of a \emph{supplied} decomposition. It does not construct useful projectors from an arbitrary matrix, prove that a searched decomposition is optimal, or guarantee that its application is profitable on a GPU. The simultaneous spectral-decomposition input remains separately recorded as classical.
189 
190 
191 
192 \subsection{Block-Jacobi normalization and the CG factor}\label{supp5:subsection:006}\textit{Source items 7.4 and 7.6; module BlockJacobi}\par
193 Work on a nonempty finite complex coordinate space with Euclidean operator norms. Assume $D$ and $A=D+K$ are positive definite. Define
194 \[
195 S=(\sqrt D)^{-1},\qquad B=SAS,\qquad E=SKS.
196 \]
197 The square root is the actual positive matrix square root supplied by continuous functional calculus, and the inverse is the actual matrix inverse. Positive definiteness makes $\sqrt D$ a unit. Its square identity and inverse identities prove
198 \[
199 SDS=I,\qquad B=I+E.
200 \]
201 
202 \textbf{A direct inverse bound.} If $C=(I+E)^{-1}$ and $\norm E_2\leq\eta<1$, then $C=I-EC$. Consequently
203 \[
204 (1-\eta)\norm C_2\leq 1,
205 \qquad \norm{I+E}_2\leq 1+\eta.
206 \]
207 The constructed normalization is invertible because $S$ and $A$ are. Combining the estimates gives the actual condition number bound
208 \[
209 \boxed{\kappa_2(B):=\norm B_2\norm{B^{-1}}_2
210 \leq\frac{1+\eta}{1-\eta}.}
211 \]
212 This norm argument does not require a separately assumed Hermitian perturbation. Nonnegative $\eta$ follows from the norm bound. Nonemptiness is explicit because the condition-number and norm-of-identity convention uses a nonzero coordinate space.
213 
214 \textbf{The preconditioning corollary.} Define
215 \[
216 q(\kappa)=\frac{\sqrt\kappa-1}{\sqrt\kappa+1}.
217 \]
218 Monotonicity of square root and positive denominators prove that $q$ is monotone. Lean also proves $\kappa_2(B)\geq1$, $q(\kappa)\geq0$ for $\kappa\geq1$, and $q(\kappa)<1$. Thus
219 \[
220 \boxed{q(\kappa_2(B))\leq q\!\left(\frac{1+\eta}{1-\eta}\right).}
221 \]
222 For $1\leq\kappa$ and $e_0\geq0$, an explicit classical premise $e_m\leq2q(\kappa)^m e_0$ and a certified upper bound $\kappa\leq\bar\kappa$ yield $e_m\leq2q(\bar\kappa)^m e_0$.
223 
224 \textbf{What is not claimed.} The classical conjugate-gradient convergence theorem, item 7.5, is not newly formalized. The new corollary proves its factor comparison and bound substitution. It does not replace the original theorem's algorithm hypotheses with a new axiom or claim a floating-point CG convergence proof.
225 
226 
227 
228 \subsection{Place in the finite development}\label{supp5:subsection:007}
229 The global small-core recompression theorem is proved in Appendix F. The classical conjugate-gradient algorithm theorem, floating-point product model and simultaneous spectral decomposition remain separately supplied inputs.
230 
231 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