Paper I: Typed Operator Systems, Seed Rank, and Exact Packet Coordinates

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 \section{Coordinate transport, morphisms, invariant exact sequences, and completion}
2 \begin{readerroadmap}
3 This section follows packet data through changes of coordinates, maps between systems, and passage to a quotient.  It then explains the additional assumptions needed when density, topology, or completion enters the argument.
4 \end{readerroadmap}
5 \subsection{Coordinate changes and packet compatible morphisms}
6 
Statement: Coordinate transport · Go to proof · Read statement and proof side by side7 \begin{theorem}[Coordinate transport]
8 \label{thm:coordinate-transport}
9 Let $U:X\to Y$ be a vector space isomorphism and let $\Pcal=(P_\alpha)$ be a packet system on $X$.  Define
10 \[
11 Q_\alpha:=UP_\alpha U^{-1}.
12 \]
13 Then $\Qcal=(Q_\alpha)$ is a packet system on $Y$.  For $\widetilde T=UTU^{-1}$,
14 \[
15 \boxed{
16 Q_\beta\widetilde TQ_\alpha
17 =
18 U(P_\beta TP_\alpha)U^{-1}.
19 }
20 \]
21 Hence packet dimensions, zero patterns, and support preorders are invariant under coordinate transport.  If a declared algebra generating family $\mathcal G$ is transported to $U\mathcal G U^{-1}$, then its transfer graph and reachability relation are also preserved.
22 \end{theorem}
23 \RecordID{PSC-I-T-COORDINATE-TRANSPORT}
24 \Depends{PSC-I-D-PACKET-SYSTEM and PSC-I-D-TRANSFER-BLOCK.}
25 
Proof block: Coordinate transport · Go to statement · Read statement and proof side by side26 \begin{proof}
27 Conjugation preserves products and sums, so
28 \[
29 Q_\alpha Q_\beta
30 =UP_\alpha P_\beta U^{-1}
31 =\delta_{\alpha\beta}Q_\alpha,
32 \qquad
33 \sum_\alpha Q_\alpha=I_Y.
34 \]
35 The block identity is direct multiplication:
36 \[
37 Q_\beta\widetilde TQ_\alpha
38 =UP_\beta TP_\alpha U^{-1}.
39 \]
40 All listed invariants are determined by these transported blocks.
41 \end{proof}
42 
43 \begin{interpretation}
44 An isomorphism changes the coordinates of each packet while preserving the direct sum structure.  Conjugating the projectors and the operator together preserves every block identity.  This is the linear prototype for the gauge changes used later in the series.
45 \end{interpretation}
46 
47 
Statement: Packet-compatible operator morphism48 \begin{definition}[Packet compatible operator morphism]
49 \label{def:packet-morphism}
50 Let $(X,\A,\Pcal)$ and $(Y,\B,\Qcal)$ be packet resolved operator modules with packet index sets $I$ and $J$.  A packet compatible operator morphism is a triple
51 \[
52 (\Phi,\varphi,\sigma)
53 \]
54 consisting of a unital algebra homomorphism $\varphi:\A\to\B$, a linear map $\Phi:X\to Y$ satisfying
55 \[
56 \Phi(Ax)=\varphi(A)\Phi(x),
57 \]
58 and a map $\sigma:I\to J$ satisfying
59 \[
60 Q_j\Phi
61 =
62 \Phi P_{\sigma^{-1}(j)},
63 \qquad
64 P_{\sigma^{-1}(j)}:=
65 \sum_{\sigma(\alpha)=j}P_\alpha.
66 \]
67 An empty fiber is interpreted as the zero projector.
68 \end{definition}
69 \RecordID{PSC-I-D-PACKET-MORPHISM}
70 
71 The packet index map records which source packets are grouped into each target packet.  Its compatibility equation says that projecting after transport gives the same result as first collecting those source packets.  The intertwining equation separately ensures that the declared operator actions agree with the transport.  Both conditions matter when comparing transfer blocks.
72 
Statement: Morphism of seeded systems73 \begin{definition}[Morphism of seeded systems]
74 \label{def:seed-morphism}
75 A morphism
76 \[
77 (X,\A,S,\Pcal)\longrightarrow(Y,\B,S',\Qcal)
78 \]
79 is a packet compatible operator morphism satisfying the seed condition
80 \[
81 \Phi(S)\subseteq\Hull_{\B}(S').
82 \]
83 In the topological category all maps and actions are required to be continuous and the seed condition uses the topological hull when declared.
84 \end{definition}
85 \RecordID{PSC-I-D-SEED-MORPHISM}
86 
Statement: Naturality of generated hulls and transfer blocks · Go to proof · Read statement and proof side by side87 \begin{theorem}[Naturality of generated hulls and transfer blocks]
88 \label{thm:naturality}
89 Let $(\Phi,\varphi,\sigma)$ be a packet compatible operator morphism.  For every subset $S\subseteq X$,
90 \[
91 \boxed{
92 \Phi(\Hull_{\A}(S))
93 =
94 \Hull_{\varphi(\A)}(\Phi(S))
95 \subseteq
96 \Hull_{\B}(\Phi(S)).
97 }
98 \]
99 For $T\in\A$ and $i,j\in J$,
100 \[
101 \boxed{
102 Q_j\varphi(T)Q_i\Phi
103 =
104 \sum_{\substack{\sigma(\beta)=j\\\sigma(\alpha)=i}}
105 \Phi P_\beta TP_\alpha.
106 }
107 \]
108 If $\Phi$ is surjective and $S$ generates $X$, then $\Phi(S)$ generates $Y$ under $\varphi(\A)$ and hence under $\B$.  If, in addition, the morphism is seeded, then $S'$ generates $Y$.
109 \end{theorem}
110 \RecordID{PSC-I-T-NATURALITY}
111 \Depends{PSC-I-D-PACKET-MORPHISM and PSC-I-T-BLOCK-MULTIPLICATION.}
112 \Exports{The canonical naturality theorem for every later realization.}
113 
Proof block: Naturality of generated hulls and transfer blocks · Go to statement · Read statement and proof side by side114 \begin{proof}
115 Every element of $\Phi(\Hull_{\A}(S))$ is a finite sum of vectors
116 \[
117 \Phi(As)=\varphi(A)\Phi(s),
118 \]
119 so it belongs to $\Hull_{\varphi(\A)}(\Phi(S))$.  Conversely, every generator $\varphi(A)\Phi(s)$ equals $\Phi(As)$, giving equality.
120 
121 For the block formula, use intertwining and packet compatibility twice:
122 \begin{align*}
123 Q_j\varphi(T)Q_i\Phi
124 &=Q_j\varphi(T)\Phi P_{\sigma^{-1}(i)}\\
125 &=Q_j\Phi TP_{\sigma^{-1}(i)}\\
126 &=\Phi P_{\sigma^{-1}(j)}TP_{\sigma^{-1}(i)}\\
127 &=\sum_{\substack{\sigma(\beta)=j\\\sigma(\alpha)=i}}
128 \Phi P_\beta TP_\alpha.
129 \end{align*}
130 If $\Phi$ is surjective and $\Hull_{\A}(S)=X$, the hull equality gives $Y=\Hull_{\varphi(\A)}(\Phi(S))$.  If $\Phi(S)\subseteq\Hull_{\B}(S')$, then $\Hull_{\B}(\Phi(S))\subseteq\Hull_{\B}(S')$, so $S'$ generates $Y$.
131 \end{proof}
132 
133 \begin{keyidea}
134 Naturality gives two ways to compute the same transported block.  One may apply the target operator between target projectors, or sum the source blocks whose packet indices map to those target indices and then apply the morphism.  The theorem also identifies the image of the generated hull.  These equalities make the comparison between the two systems precise.
135 \end{keyidea}
136 
137 
Statement: Category of seeded packet systems · Go to proof · Read statement and proof side by side138 \begin{proposition}[Category of seeded packet systems]
139 \label{prop:seed-category}
140 Packet compatible operator morphisms compose, seeded morphisms compose, and identity morphisms satisfy both definitions.  Thus packet resolved operator modules form a category $\mathbf{PktMod}$ and seeded packet systems form a category $\mathbf{SeedSys}$.
141 \end{proposition}
142 \RecordID{PSC-I-P-SEED-SYSTEM-CATEGORY}
143 \Depends{\nolinkurl{PSC-I-D-PACKET-MORPHISM},
144 \nolinkurl{PSC-I-D-SEED-MORPHISM}, and
145 \nolinkurl{PSC-I-T-NATURALITY}.}
146 
Proof block: Category of seeded packet systems · Go to statement · Read statement and proof side by side147 \begin{proof}
148 Let $(\Phi,\varphi,\sigma):(X,\A,\Pcal)\to(Y,\B,\Qcal)$ and $(\Psi,\psi,\tau):(Y,\B,\Qcal)\to(Z,\Ccal,\Rcal)$ be morphisms.  Intertwining is preserved because
149 \[
150 \Psi\Phi(Ax)
151 =
152 \Psi(\varphi(A)\Phi x)
153 =
154 (\psi\circ\varphi)(A)\Psi\Phi x.
155 \]
156 For $k$ in the target packet set,
157 \begin{align*}
158 R_k\Psi\Phi
159 &=\Psi Q_{\tau^{-1}(k)}\Phi\\
160 &=\Psi\Phi
161 \sum_{\tau(\sigma(\alpha))=k}P_\alpha.
162 \end{align*}
163 Thus the composite packet map is $\tau\circ\sigma$.  If the morphisms are seeded, then
164 \[
165 \Phi(S)\subseteq\Hull_{\B}(S'),
166 \qquad
167 \Psi(S')\subseteq\Hull_{\Ccal}(S'').
168 \]
169 By \cref{thm:naturality},
170 \[
171 \Psi\Phi(S)
172 \subseteq
173 \Psi(\Hull_{\B}(S'))
174 \subseteq
175 \Hull_{\Ccal}(\Psi(S'))
176 \subseteq
177 \Hull_{\Ccal}(S'').
178 \]
179 Identity maps satisfy the definitions with identity algebra and packet maps.
180 \end{proof}
181 
182 \subsection{Invariant subspaces and quotient packets}
183 Passage to a quotient uses two separate invariance assumptions.  The packet projectors must preserve the subspace for packet coordinates to descend.  An operator must also preserve that subspace for its action, and hence its transfer blocks, to descend.  The first condition is enough for the packet exact sequence.  The second enters the corollary about transfer blocks.
184 
Statement: Packet exact sequence for an invariant subspace · Go to proof · Read statement and proof side by side185 \begin{theorem}[Packet exact sequence for an invariant subspace]
186 \label{thm:packet-exact-sequence}
187 Let $K\leq X$ satisfy $P_\alpha K\subseteq K$ for every $\alpha$.  Define
188 \[
189 K_\alpha:=P_\alpha K=K\cap X_\alpha
190 \]
191 and
192 \[
193 \overline P_\alpha(x+K):=P_\alpha x+K.
194 \]
195 Then:
196 \begin{enumerate}[label=(\roman*)]
197 \item The nonzero restrictions $P_\alpha|_K$ form a packet system on $K$.
198 \item The nonzero $\overline P_\alpha$ form a packet system on $X/K$.
199 \item For every $\alpha$ there is a short exact sequence
200 \[
201 0\longrightarrow K_\alpha
202 \longrightarrow X_\alpha
203 \longrightarrow \overline P_\alpha(X/K)
204 \longrightarrow0,
205 \]
206 and
207 \[
208 \overline P_\alpha(X/K)
209 \cong
210 X_\alpha/(X_\alpha\cap K)
211 \cong
212 (X_\alpha+K)/K.
213 \]
214 \item The full exact sequence decomposes packetwise as the direct sum of these short exact sequences.
215 \end{enumerate}
216 \end{theorem}
217 \RecordID{PSC-I-T-PACKET-EXACT-SEQUENCE}
218 \Depends{PSC-I-T-EXACT-PACKET-COORDINATES.}
219 \Exports{Packetwise subobject and quotient constructions.}
220 
Proof block: Packet exact sequence for an invariant subspace · Go to statement · Read statement and proof side by side221 \begin{proof}
222 Restriction preserves idempotency, pairwise annihilation, and the identity sum on $K$.  If $x\in K\cap X_\alpha$, then $x=P_\alpha x\in P_\alpha K$, proving $K_\alpha=K\cap X_\alpha$.
223 
224 The quotient operator is well defined because replacing $x$ by $x+k$ changes $P_\alpha x$ by $P_\alpha k\in K$.  The idempotent and annihilation identities descend, and the sum is the identity on $X/K$.  The map $X_\alpha\to X/K$ has image $(X_\alpha+K)/K$ and kernel $X_\alpha\cap K$, giving the short exact sequence and the quotient isomorphisms.  Exact packet coordinates identify the original sequence with the direct sum over $\alpha$.
225 \end{proof}
226 
227 \begin{microexample}[title={Packet descent to a quotient}]
228 Let \(X=X_1\oplus X_2\) and let \(K\subseteq X_1\) be a subspace.  The quotient has packets \(X_1/K\) and \(X_2\).  Any operator preserving \(K\) descends with the same organization by source and target packets, with blocks entering or leaving the first packet replaced by their induced quotient maps.  An induced block can become zero even when its original block is nonzero, so the pattern of nonzero blocks can shrink.  Any resulting zero packet is removed from the quotient packet system.
229 \end{microexample}
230 
231 
Statement: Packet descent through an invariant quotient · Go to proof · Read statement and proof side by side232 \begin{theorem}[Packet descent through an invariant quotient]
233 \label{thm:quotient-packet-descent}
234 Under the hypotheses of \cref{thm:packet-exact-sequence}, the operators
235 \[
236 \overline P_\alpha(x+K)=P_\alpha x+K
237 \]
238 are well defined pairwise annihilating idempotents with sum $I_{X/K}$, and the quotient map satisfies
239 \[
240 \boxed{\pi P_\alpha=\overline P_\alpha\pi.}
241 \]
242 After zero packets are removed, they form the canonical quotient packet system.
243 \end{theorem}
244 \RecordID{PSC-I-T-QUOTIENT-PACKET-DESCENT}
245 \Depends{PSC-I-T-PACKET-EXACT-SEQUENCE.}
246 
Proof block: Packet descent through an invariant quotient · Go to statement · Read statement and proof side by side247 \begin{proof}
248 All assertions are the quotient part of \cref{thm:packet-exact-sequence}.  The intertwining identity follows directly from the definition:
249 \[
250 \overline P_\alpha\pi(x)=P_\alpha x+K=\pi P_\alpha(x).
251 \]
252 \end{proof}
253 
Statement: Restriction and quotient of transfer blocks · Go to proof · Read statement and proof side by side254 \begin{corollary}[Restriction and quotient of transfer blocks]
255 \label{cor:block-descent}
256 Under the hypotheses of \cref{thm:packet-exact-sequence}, let $T\in\End(X)$ preserve $K$.  Then every block $T_{\beta\alpha}$ maps $K_\alpha$ into $K_\beta$, and the induced quotient operator $\overline T$ satisfies
257 \[
258 \boxed{
259 \overline T_{\beta\alpha}\,\pi
260 =
261 \pi T_{\beta\alpha},
262 }
263 \]
264 where $\pi:X\twoheadrightarrow X/K$.
265 \end{corollary}
266 \RecordID{PSC-I-C-QUOTIENT-PACKET-DESCENT}
267 \Depends{PSC-I-T-PACKET-EXACT-SEQUENCE.}
268 
Proof block: Restriction and quotient of transfer blocks · Go to statement · Read statement and proof side by side269 \begin{proof}
270 If $x\in K_\alpha$, then $Tx\in K$, so
271 \[
272 T_{\beta\alpha}x=P_\beta Tx\in K\cap X_\beta=K_\beta.
273 \]
274 On the quotient,
275 \[
276 \overline T_{\beta\alpha}\pi
277 =
278 \overline P_\beta\overline T\overline P_\alpha\pi
279 =
280 \pi P_\beta TP_\alpha.
281 \]
282 \end{proof}
283 
Statement: Topological packet exact sequence · Go to proof · Read statement and proof side by side284 \begin{corollary}[Topological packet exact sequence]
285 \label{cor:topological-packet-exact-sequence}
286 If $X$ is Banach, the $P_\alpha$ are bounded, and $K$ is closed and packet invariant, then every packet sequence in \cref{thm:packet-exact-sequence} is a short exact sequence of Banach spaces with bounded maps, and the quotient projectors are bounded.
287 \end{corollary}
288 \RecordID{PSC-I-C-TOPOLOGICAL-PACKET-EXACT-SEQUENCE}
289 \Depends{\nolinkurl{PSC-I-T-PACKET-EXACT-SEQUENCE} and
290 \nolinkurl{PSC-I-T-BANACH-PACKET-ISOMORPHISM}.}
291 
Proof block: Topological packet exact sequence · Go to statement · Read statement and proof side by side292 \begin{proof}
293 Closedness of $K$ makes $X/K$ Banach.  The restricted projectors are bounded, and the quotient projectors are bounded because
294 \[
295 \|\overline P_\alpha(x+K)\|_{X/K}
296 \leq
297 \|P_\alpha\|\,\|x+K\|_{X/K}.
298 \]
299 The packet spaces are closed ranges of bounded idempotents.
300 \end{proof}
301 
302 \subsection{Dense images, quotient topology, and completion}
303 Algebraic generation uses finite linear combinations of operator images.  Topological generation allows limits of those combinations in the declared topology.  A continuous surjection carries this approximation property to the target, but identifying the target with a topological quotient requires a further assumption.
304 
Statement: Dense realization theorem · Go to proof · Read statement and proof side by side305 \begin{theorem}[Dense realization theorem]
306 \label{thm:dense-realization}
307 Let $X$ and $Y$ be Hausdorff topological vector spaces, let $\Phi:X\to Y$ be continuous, surjective, and intertwining with respect to $\varphi$, and let $S$ topologically generate $X$.  Then $\Phi(S)$ topologically generates $Y$.  If finite continuous packet systems satisfy
308 \[
309 Q_j\Phi=\Phi P_{\sigma^{-1}(j)},
310 \]
311 then
312 \[
313 \boxed{
314 Q_jY=\Phi(P_{\sigma^{-1}(j)}X)
315 }
316 \]
317 for every $j$.
318 \end{theorem}
319 \RecordID{PSC-I-T-DENSE-REALIZATION}
320 \Depends{PSC-I-T-NATURALITY.}
321 
Proof block: Dense realization theorem · Go to statement · Read statement and proof side by side322 \begin{proof}
323 Given $y=\Phi(x)$, choose a net $x_\lambda\in\Hull_{\A}(S)$ converging to $x$.  Then
324 \[
325 \Phi(x_\lambda)\to y,
326 \]
327 and naturality places every $\Phi(x_\lambda)$ in $\Hull_{\B}(\Phi(S))$.  Hence the latter hull is dense.  For packets, one inclusion follows from compatibility.  Conversely, if $y=Q_jy$, choose $x$ with $\Phi(x)=y$.  Then
328 \[
329 y=Q_j\Phi(x)=\Phi P_{\sigma^{-1}(j)}x.
330 \]
331 \end{proof}
332 
Statement: Quotient topology and completed realization · Go to proof · Read statement and proof side by side333 \begin{theorem}[Quotient topology and completed realization]
334 \label{thm:quotient-topology}
335 Let $\Phi:X\twoheadrightarrow Y$ be a continuous linear quotient map between Hausdorff topological vector spaces, and put $K=\Ker\Phi$.  Then the induced map
336 \[
337 \widetilde\Phi:X/K\longrightarrow Y
338 \]
339 is a topological isomorphism.  If $D\subseteq X$ is a linear subspace whose image $\Phi(D)$ is dense in a complete space $Y$, then the completion of
340 \[
341 D/(D\cap K)
342 \]
343 in the topology transported from $Y$ is canonically isomorphic to $Y$.
344 \end{theorem}
345 \RecordID{PSC-I-T-QUOTIENT-TOPOLOGY-COMPLETION}
346 \Depends{PSC-I-T-COMPLETED-PRESENTATION, the definition of quotient topology, and uniqueness of completion.}
347 
Proof block: Quotient topology and completed realization · Go to statement · Read statement and proof side by side348 \begin{proof}
349 The algebraic first isomorphism theorem gives a bijection $\widetilde\Phi$.  By definition of the quotient topology, a set $U\subseteq X/K$ is open exactly when its preimage in $X$ is open.  Because $\Phi$ is a quotient map, this is equivalent to $\widetilde\Phi(U)$ being open in $Y$.  Thus $\widetilde\Phi$ is a homeomorphism.  The second statement applies the dense completion argument of \cref{thm:completed-presentation} to the injective map $D/(D\cap K)\to Y$.
350 \end{proof}
351 
Statement: Continuous surjections and quotient topology352 \begin{boundary}[Continuous surjections and quotient topology]
353 \label{bnd:topological-quotient}
354 Continuity and surjectivity transport density as in \cref{thm:dense-realization}.  They do not by themselves identify the given topology on $Y$ with the quotient topology from $X$.  The stronger conclusion in \cref{thm:quotient-topology} requires the quotient map hypothesis or an equivalent open mapping condition.
355 \end{boundary}
356 \RecordID{PSC-I-B-TOPOLOGICAL-QUOTIENT}
357 
358 \begin{warningbox}
359 A continuous surjective linear map need not be a quotient map in arbitrary topological vector spaces.  The algebraic first isomorphism theorem gives a bijection on the quotient.  A topological isomorphism requires the quotient topology to agree with the target topology.  An applicable open mapping theorem can supply this agreement, as it does for continuous linear surjections between Banach spaces.
360 \end{warningbox}
361 
362 The completion statement uses the topology transported from the target space.  This choice ensures that approximation in the quotient means approximation in the target.  A topology inherited from the original subspace need not give the same completion unless the two topologies agree.  The theorem therefore names the topology as part of its conclusion.
363 
364 \begin{sectionrecap}
365 Packet systems transport by conjugation, form a category under packet compatible seeded morphisms, restrict to invariant subspaces, descend to invariant quotients, and survive completion under explicit boundedness and quotient topology hypotheses.
366 \end{sectionrecap}
367 
368 
369 \begin{figure}[htbp]
370 \centering
371 \includegraphics[width=0.96\textwidth]{09_coordinate_transport.pdf}
372 \caption{Numerical certificate for a nonorthogonal transported packet system. The diagonal products retain idempotent size while off diagonal products remain at roundoff level.}
373 \label{fig:coordinate-transport}
374 \end{figure}
375 
376 \section{Realization functors and semantic theorem transport}
377 \begin{readerroadmap}
378 A later domain is a genuine realization only when the relevant structures and identities are preserved.  The purpose of this section is to replace informal analogy by a precise preservation profile.
379 \end{readerroadmap}
380 \subsection{Preservation profiles}
381 
Statement: Realization functor and preservation profile382 \begin{definition}[Realization functor and preservation profile]
383 \label{def:realization-functor}
384 Let $\mathbf{SeedSys}_{\mathrm{abs}}$ be an abstract category of seed systems and let $\mathbf C_D$ be a domain category.  A realization functor is a functor
385 \[
386 \mathsf{Ev}_D:\mathbf{SeedSys}_{\mathrm{abs}}\longrightarrow\mathbf C_D
387 \]
388 with a declared preservation profile specifying which of the following structures are preserved:
389 \[
390 \begin{gathered}
391 0,\ I,\ \text{finite sums},\ \text{composition},\ \text{biproducts},\\
392 \text{kernels},\ \text{cokernels},\ \text{quotients},\ \text{tensor products},\\
393 \text{packet idempotents},\ \text{transfer blocks},\ \text{topological completions}.
394 \end{gathered}
395 \]
396 Preservation of a structure means preservation of its defining identity or universal property, not merely a similarity of notation.
397 \end{definition}
398 \RecordID{PSC-I-D-REALIZATION-FUNCTOR}
399 
Statement: Equational realization principle · Go to proof · Read statement and proof side by side400 \begin{theorem}[Equational realization principle]
401 \label{thm:realization-export}
402 Let $F:\mathbf C\to\mathbf D$ be an additive functor between preadditive categories.  Any equality of morphisms constructed from declared generating morphisms by finite sums, additive inverses, identities, zero maps, and composition is preserved by $F$.  Scalar multiplication by a coefficient ring is also preserved when the categories are enriched over that ring and $F$ is linear for the declared enrichment.  If a proof additionally uses a chosen biproduct, kernel, cokernel, quotient, tensor product, or completion and $F$ preserves that construction in its declared profile, then the corresponding proof diagram is transported to $\mathbf D$.
403 \end{theorem}
404 \RecordID{PSC-I-T-REALIZATION-EXPORT}
405 \Depends{PSC-I-D-REALIZATION-FUNCTOR.}
406 \Exports{The formal criterion for semantic transfer across domains.}
407 
Proof block: Equational realization principle · Go to statement · Read statement and proof side by side408 \begin{proof}
409 Functoriality gives
410 \[
411 F(I)=I,
412 \qquad
413 F(g\circ f)=F(g)\circ F(f),
414 \]
415 and additivity gives
416 \[
417 F(0)=0,
418 \qquad
419 F(f+g)=F(f)+F(g),
420 \qquad
421 F(-f)=-F(f).
422 \]
423 If the declared enrichment is present, linearity additionally gives $F(af)=aF(f)$ for every coefficient $a$.  A structural induction on the construction of a morphism expression therefore carries every permitted equational proof to its image under $F$.  If a step invokes a universal construction, preservation means that the image diagram satisfies the same universal property.  The uniquely induced morphism in the source proof is therefore carried to the uniquely induced morphism in the target proof.  Repeating this argument through the finite proof diagram transports the conclusion.
424 \end{proof}
425 
426 \begin{interpretation}
427 The equational principle covers identities built from operations the functor preserves.  Additive identities require additivity.  Identities with scalar coefficients require linear enrichment.  Quotients, tensor products, completions, kernels, or limits require their own preservation assumptions.  The preservation profile records the assumptions needed to carry each step of the proof into the target category.
428 \end{interpretation}
429 
430 
431 \subsection{From equation transport to semantic realization}
Statement: Realization export principle · Go to proof · Read statement and proof side by side432 \begin{proposition}[Realization export principle]
433 \label{prop:realization-export}
434 Every canonical Paper I identity whose proof uses only the operations listed in a realization functor's verified preservation profile remains valid after applying that functor.  If the proof uses a domain specific hypothesis not encoded by the functor, that hypothesis must be verified separately before the transported statement is promoted to a theorem.
435 \end{proposition}
436 \RecordID{PSC-I-P-REALIZATION-EXPORT}
437 \Depends{PSC-I-T-REALIZATION-EXPORT.}
438 
Proof block: Realization export principle · Go to statement · Read statement and proof side by side439 \begin{proof}
440 The first assertion is \cref{thm:realization-export}.  The second is a logical boundary: a functor transports established identities and preserved universal constructions, but it does not create an unverified analytic, topological, positivity, finiteness, or integrality hypothesis.
441 \end{proof}
442 
Statement: Semantic realization criterion443 \begin{definition}[Semantic realization criterion]
444 \label{def:semantic-realization}
445 A domain theorem is a semantic realization of a canonical seed calculus theorem only when:
446 \begin{enumerate}[label=(\roman*)]
447 \item An explicit realization functor or intertwining construction is given.
448 \item The preservation profile covers every construction used in the canonical proof.
449 \item Every additional analytic, finiteness, convergence, positivity, or integrality hypothesis is verified in the domain.
450 \item The resulting conclusion is stated in the domain's native objects.
451 \end{enumerate}
452 Reuse of the words ``seed'', ``packet'', or ``transfer'' without these data is only syntactic reuse.
453 \end{definition}
454 \RecordID{PSC-I-D-SEMANTIC-REALIZATION}
455 
456 \begin{warningbox}
457 A change of nouns is not a realization theorem.  Calling a frequency band, a ramification sector, and a symmetry sector a ``packet'' is only terminology until one exhibits the idempotents, proves reconstruction, identifies the transfer blocks, and checks that the relevant morphisms or limits preserve those structures.
458 \end{warningbox}
459 
460 \begin{sectionrecap}
461 The preservation profile determines which equations and proof constructions pass to a new domain.  Checking it gives later papers a concrete test for transporting a theorem: identify the realization, check each operation used in the proof, and verify the additional domain hypotheses.
462 \end{sectionrecap}
463 
464 
465 \section{Canonical export interface and claim boundary}
466 \begin{readerroadmap}
467 The export interface lets later papers use the foundational proofs directly.  Each paper can cite the stable record ID, state its domain hypotheses, and prove the new step specific to its realization.
468 \end{readerroadmap}
469 
Statement: Reserved example slots470 \begin{definition}[Worked realization interface]
471 \label{def:reserved-example-slots}
472 The foundational calculus is illustrated by four canonical algebraic realizations:
473 \begin{enumerate}[label=(\roman*)]
474 \item A typed quiver reachability model.
475 \item An algebraic coordinate ring presentation.
476 \item A companion and repeated primary single operator model.
477 \item Path and cycle adjacency models.
478 \end{enumerate}
479 The worked model sections below instantiate these four interfaces. A bilateral shift example records the analytic completion mechanism also used in Paper V. Computational specifications connect the proofs with the verification companion and are not premises of the foundational theorems.
480 \end{definition}
481 \RecordID{PSC-I-ALG-EXAMPLE-SLOTS}
482 
Statement: Paper I export object483 \begin{definition}[Paper I export object]
484 \label{def:paper-one-export}
485 The canonical Paper I export is
486 \[
487 \boxed{
488 \mathsf{PSC}_I=
489 \left(
490 \begin{array}{c}
491 \text{typed grammars and realized operator algebras},\\
492 \text{seed systems, free presentations, and seed rank},\\
493 \text{module-top, semisimple, and single-operator formulas},\\
494 \text{finite and unconditional packet coordinates},\\
495 \text{transfer blocks and support algebras},\\
496 \text{reachability and packet-pure source generation},\\
497 \text{morphisms, invariant exact sequences, quotients, completions},\\
498 \text{realization functors and equational theorem transport}
499 \end{array}
500 \right).
501 }
502 \]
503 \end{definition}
504 \RecordID{PSC-I-EXPORT}
505 
506 
507 
508 \subsection{Use across papers}
509 \begin{center}
510 \begin{longtable}{@{}>{\raggedright\arraybackslash}p{0.26\textwidth}>{\raggedright\arraybackslash}p{0.18\textwidth}>{\raggedright\arraybackslash}p{0.49\textwidth}@{}}
511 \toprule
512 \textbf{Paper I export} & \textbf{Primary users} & \textbf{Later role}\\
513 \midrule
514 \endhead
515 Typed grammar and module equivalence & II to XII & Gives each domain a legal operator syntax and a concrete module realization.\\
516 Free seed presentation & IV, IX, X & Converts generated families into quotient presentations and relation modules.\\
517 Jacobson top seed rank & VII, X, XII & Computes minimal generators from semisimple multiplicity data.\\
518 Single operator formula & IV, VI, IX & Resolves recurrence, companion, and spectral chain generator counts.\\
519 Exact packet coordinates & II to XII & Supplies analysis, synthesis, and packetwise equality.\\
520 Tensor and dual packet systems & V, VII, VIII, XI & Controls product systems, observables, and paired representations.\\
521 Transfer block multiplication & II to XII & Converts operator composition into sums over packet paths.\\
522 Block intertwining equations & III, VII, XI & Expresses global equivalence or gluing as local packet equations.\\
523 Support preorder algebra & II, VIII, X & Produces triangular transfer structure and nilpotent strict transfer ideals.\\
524 Source component seed rank & VIII, X & Identifies the packet pure source requirements under propagation hypotheses.\\
525 Packet exact sequences and quotient descent & III, VI, X, XII & Carries packets through constraints, reductions, and deformation quotients.\\
526 Semantic realization criterion & IV to XII & Specifies when a domain theorem is a true realization of the common calculus.\\
527 \bottomrule
528 \end{longtable}
529 \end{center}
530 
531 
Statement: Exact limits of Paper I532 \begin{boundary}[Exact limits of Paper I]
533 \label{bnd:final-claim-boundary}
534 The existence of an exact packet decomposition does not imply that the decomposition is computationally discoverable, numerically well conditioned, statistically identifiable, dynamically invariant, or mathematically useful.  The condition number in \cref{def:packet-condition-number} quantifies only coordinate stability once the packets are supplied.  Refinement towers, filtered transfer, nonlinear obstruction objects, automatic packet recovery, continuum limits, arithmetic lifts, and automorphic occupancy require additional theorems in later papers.
535 \end{boundary}
536 \RecordID{PSC-I-B-FINAL-CLAIM-BOUNDARY}
537 
538 
539 

Back to source controls

Back to Paper I: Typed Operator Systems, Seed Rank, and Exact Packet Coordinates