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 \part{Finite typed transfer and the formal contract}\label{part:finite}
2 \noindent The finite algebraic core supplies the algebraic foundation and a contract for its individual declarations. Here, ``roadmap'' and ``outside the contract'' describe the scope of the finite Lean formalization. Ordinary mathematical results in Part~II may lie beyond that scope. The finite contract covers thirty result environments. The source contract has 41 mapping rows because it also includes definitions and other interfaces.
3 
4 \medskip\noindent The formal companion records the exact Lean and Mathlib dependencies \cite{lean,mathlib}, compilation, kernel replay, and axiom checks. References to declarations from Chapters I--II retain their explicitly inherited status. The companion distinguishes the finite algebraic contract from the additional packet-coordinate and analytic interfaces.
5 \section{Purpose and formal status}
6 \label{sec:purpose}
7 
8 Chapter I fixed typed seeds, operator grammars, exact projector packets,
9 generated hulls, and reconstruction \cite{paperI}.  Chapter II added coherent
10 refinement coordinates, weighted transfer, arithmetic separation, and linear
11 defect identities \cite{paperII}.  The present chapter begins the next layer:
12 explicit edge words, optional connection data, and obstructions within
13 individual packets.
14 
15 Canonical coordinate transport and a connection play different mathematical
16 roles. Canonical transport compares two exact descriptions of the
17 \emph{same} ambient object and is forced by analysis and synthesis. A
18 connection chooses transports that may carry extra modeling, discretization,
19 or gauge information. Canonical transport obeys a cocycle theorem. A
20 connection may fail to obey a cocycle, and that failure is meaningful data.
21 Keeping separate notation lets us distinguish the automatic coherence of
22 exact coordinates from the possible holonomy of a chosen connection.
23 
24 \subsection{Statement labels}
25 
26 Every substantial theorem, lemma, corollary, proposition, definition, API,
27 and roadmap item carries one or more of the three labels below. When separate
28 clauses use a Chapter III result and an inherited bridge, the statement carries
29 both applicable labels. Illustrative examples do not require a label.
30 \begin{enumerate}[label=\textbf{S\arabic*.},leftmargin=3.2em]
31 \item \textbf{Lean-backed in Chapter III}: the displayed scope is no stronger
32 than the named compiled declaration in the identified Chapter III module.
33 \item \textbf{Inherited Lean-backed}: the displayed result is supplied by the
34 frozen formal contract of Chapter I or Chapter II.
35 \item \textbf{Roadmap only}: the text states a future interface or theorem
36 target and is excluded from the completion denominator.
37 \end{enumerate}
38 
39 \begin{boundary}[Finite theorem denominator]
40 The completion denominator of the finite algebraic contract consists of the
41 thirty result environments in Part~I. Of these, 26 resolve to compiled
42 Chapter III declarations and four resolve to the frozen Chapters I--II
43 contracts. The authoritative theorem map names the exact declarations used
44 by each statement. The kernel audit checks those targets and their supporting
45 theorems. The namespace gate requires every declaration in the compiled
46 \leanname{Komorebi.PaperIII} namespace to pass its checks. Roadmap items are
47 excluded from the denominator and remain visibly marked.
48 \end{boundary}
49 
50 \section{Finite typed packet graphs}
51 \label{sec:edge-operators}
52 
53 \subsection{Orientation and matrix convention}
54 
55 Let $V$ be a finite packet type, $E$ a finite edge type, and $R$ a semiring.
56 A directed multigraph is a pair of endpoint functions
57 \[
58   \src,\tgt:E\longrightarrow V.
59 \]
60 Parallel edges remain distinct elements of $E$.  Rows are targets and columns
61 are sources.  Thus an edge $e:i\to j$ is represented by a matrix supported at
62 row $j$, column $i$.
63 
64 \begin{definition}[Packet graph and scalar edge system]
65 \label{def:edge-system}
66 For $a,b\in V$ and $r\in R$, define
67 \[
68   \operatorname{packetMatrix}(a,b;r)_{yx}
69   =
70   \begin{cases}
71   r,&y=b\text{ and }x=a,\\
72   0,&\text{otherwise}.
73   \end{cases}
74 \]
75 An edge system is a coefficient function $c:E\to R$.  Its elementary edge
76 operator and total transfer operator are
77 \[
78   L_e=\operatorname{packetMatrix}(\src(e),\tgt(e);c(e)),
79   \qquad
80   T=\sum_{e\in E}L_e.
81 \]
82 \end{definition}
83 \statusleanthree{Komorebi.PaperIII.EdgeOperators.PacketGraph; Komorebi.PaperIII.EdgeOperators.PacketGraph.packetMatrix; Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem; Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.edgeOp; Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.transferOp}
84 
85 Words are written in execution order. In $L_fL_e$, the rightmost operator
86 $L_e$ acts first. For a written word $(e_1,\ldots,e_n)$, $e_1$ acts first
87 and the operator product is $L_{e_n}\cdots L_{e_1}$.
88 
89 \begin{keyidea}[title={Reading the execution order}]
90 Read the edge list in the order of execution. The matrix product writes later
91 actions farther to the left. The target packet of one edge must equal the
92 source packet of the next before multiplication can contribute. Over a noncommutative
93 semiring, this order also fixes the order of the scalar coefficients.
94 \end{keyidea}
95 
96 \begin{lemma}[Declared support]
97 \label{lem:edge-support}
98 For every edge $e$, $(L_e)_{yx}=0$ unless
99 $y=\tgt(e)$ and $x=\src(e)$.
100 \end{lemma}
101 \statusleanthree{Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.edgeOp_eq_zero_off_support}
102 
103 \begin{theorem}[Typed interface annihilation]
104 \label{thm:edge-annihilation}
105 If $\tgt(e)\ne\src(f)$, then
106 \[
107   L_fL_e=0.
108 \]
109 \end{theorem}
110 \statusleanthree{Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.edgeOp_mul_edgeOp_eq_zero}
111 
112 \begin{proof}
113 For a matrix entry $(y,x)$,
114 \[
115   (L_fL_e)_{yx}=\sum_{z\in V}(L_f)_{yz}(L_e)_{zx}.
116 \]
117 A potentially nonzero summand would require simultaneously
118 $z=\src(f)$ and $z=\tgt(e)$, contrary to the hypothesis.
119 \end{proof}
120 
121 \begin{theorem}[Collapse of a matched edge pair]
122 \label{thm:edge-composable}
123 If $\tgt(e)=\src(f)$, then
124 \[
125 L_fL_e
126 =
127 \operatorname{packetMatrix}
128 \bigl(\src(e),\tgt(f);c(f)c(e)\bigr).
129 \]
130 Together with \cref{thm:edge-annihilation}, this gives both cases for
131 the composition of two edge operators.
132 \end{theorem}
133 \statusleanthree{Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.edgeOp_mul_edgeOp_of_composable}
134 
135 \begin{proof}
136 The sum defining the matrix product has exactly one potentially nonzero intermediate
137 index, namely $\tgt(e)=\src(f)$.  At that index the coefficients occur in
138 operator order as $c(f)c(e)$, and the outer source and target are
139 $\src(e)$ and $\tgt(f)$.
140 \end{proof}
141 
142 \begin{boundary}[Current fiber scope]
143 The compiled Chapter III model above has one scalar coordinate per packet.
144 For a family of modules $(X_i)_{i\in V}$, an intrinsic edge map would instead
145 have type $\ell_e:X_{\src(e)}\to X_{\tgt(e)}$, and its totalization on
146 $\bigoplus_iX_i$ would be
147 $\iota_{\tgt(e)}\ell_e\pi_{\src(e)}$.  The same support proof applies, but
148 this generalization with dependent fibers is not attributed to the released
149 Chapter III modules for scalar edge systems.
150 \end{boundary}
151 
152 \Cref{fig:typed-edge-walks} summarizes the support convention and shows
153 how composable words differ from words with a broken interface. The next
154 section uses this distinction.
155 
156 \begin{figure}[tbp]
157 \centering
158 \includegraphics[width=.96\linewidth]{typed_edge_walks.pdf}
159 \caption{Rows record target packets and columns record source packets.
160 This convention fixes execution order. Composable words collapse to endpoint
161 blocks, while one broken packet interface annihilates the entire operator
162 product.}
163 \label{fig:typed-edge-walks}
164 \end{figure}
165 
166 \section{Operator words and directed walks}
167 \label{sec:words-walks}
168 
169 \subsection{Typed words}
170 
171 \begin{definition}[Composable word and execution operator]
172 \label{def:word-op}
173 A finite word $w=(e_1,\ldots,e_n)$ is composable when
174 \[
175   \tgt(e_r)=\src(e_{r+1})
176   \qquad (1\le r<n).
177 \]
178 Set
179 \[
180   L_w=L_{e_n}\cdots L_{e_1},
181   \qquad L_{\varnothing}=I.
182 \]
183 This definition records the written order of execution even though matrix
184 composition is read right to left.
185 \end{definition}
186 \statusleanthree{Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.Composable; Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.wordOp}
187 
188 \begin{theorem}[First broken interface]
189 \label{thm:first-break}
190 If a word begins $(e,f,\ldots)$ and $\tgt(e)\ne\src(f)$, then its word
191 operator is zero.
192 \end{theorem}
193 \statusleanthree{Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.wordOp_eq_zero_of_first_break}
194 
195 \begin{theorem}[Noncomposable words vanish]
196 \label{thm:nonwalk-vanish}
197 If $w$ is not composable, then $L_w=0$.
198 \end{theorem}
199 \statusleanthree{Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.wordOp_eq_zero_of_not_composable}
200 
201 \begin{proof}
202 Choose the first broken adjacent pair.  The corresponding consecutive factor
203 is zero by \cref{thm:edge-annihilation}, and associativity absorbs that zero
204 into the complete product.  The Lean proof implements the same argument by
205 induction on the list.
206 \end{proof}
207 
208 \subsection{The checked recursive expansion}
209 
210 \begin{definition}[Recursive word expansion]
211 \label{def:recursive-word-expansion}
212 Define
213 \[
214   \cW_0=I,
215   \qquad
216   \cW_{n+1}=T\cW_n.
217 \]
218 \end{definition}
219 \statusleanthree{Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.wordExpansion}
220 
221 \begin{theorem}[Transfer power equals recursive word expansion]
222 \label{thm:power-recursive-expansion}
223 For every $n\in\N$,
224 \[
225   T^n=\cW_n.
226 \]
227 \end{theorem}
228 \statusleanthree{Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.transferOp_pow_eq_wordExpansion}
229 
230 \begin{proof}
231 The zero case is the identity matrix.  If $T^n=\cW_n$, then the
232 left-successor power convention gives
233 $T^{n+1}=TT^n=T\cW_n=\cW_{n+1}$.
234 \end{proof}
235 
236 \begin{remark}
237 The formal module also defines an explicit sum over tuples
238 $w:\operatorname{Fin}(n)\to E$ and a second sum in which noncomposable tuples
239 are replaced by zero.  It proves that the recursive matrix, the explicit tuple sum, and the sum
240 filtered by composability agree. The separate declarations make the finite
241 enumeration claim directly checkable.
242 \end{remark}
243 \statusleanthree{Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.explicitWordExpansion; Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.walkExpansion; Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.wordExpansion_eq_explicitWordExpansion; Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.explicitWordExpansion_eq_walkExpansion}
244 
245 \subsection{Exact expansion from words to walks}
246 
247 For a nonempty composable word $w=(e_1,\ldots,e_n)$, define its reverse
248 coefficient product
249 \[
250   c^\leftarrow(w)=c(e_n)c(e_{n-1})\cdots c(e_1).
251 \]
252 The reversal is essential over a noncommutative semiring.
253 
254 \begin{lemma}[One word is one endpoint block]
255 \label{lem:word-endpoint}
256 If $w=(e_1,\ldots,e_n)$ is nonempty and composable, then
257 \[
258   L_w
259   =
260   \operatorname{packetMatrix}
261   \bigl(\src(e_1),\tgt(e_n);c^\leftarrow(w)\bigr).
262 \]
263 \end{lemma}
264 \statusleanthree{Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.reverseCoefficient; Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.terminalTarget; Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.wordOp_eq_packetMatrix_of_composable}
265 
266 \begin{proof}
267 Induct on $n$.  The case $n=1$ is the definition of $L_e$.  Suppose the
268 formula holds for the prefix $(e_1,\ldots,e_n)$ and append $f$.  Composability
269 gives $\tgt(e_n)=\src(f)$.  Multiplying the two packet matrices leaves one
270 intermediate index and changes the coefficient to
271 $c(f)c(e_n)\cdots c(e_1)$, with source $\src(e_1)$ and target $\tgt(f)$.
272 \end{proof}
273 
274 Write $\Walk_n(i,j)$ for the finite set of composable edge tuples of length $n$
275 whose first source is $i$ and whose final target is $j$. For $n=0$, it has
276 one empty walk when $i=j$ and is empty otherwise. Assign the empty walk the
277 coefficient $1$.
278 
279 \begin{interpretation}[title={The empty walk}]
280 The empty walk records doing nothing at a chosen packet. It contributes only
281 to a diagonal entry. Thus the convention for length zero matches the identity
282 matrix and lets the walk sum include every nonnegative power.
283 \end{interpretation}
284 
285 \begin{theorem}[Finite operator expansion from words to walks]
286 \label{thm:word-to-walk}
287 For every $n\in\N$,
288 \[
289   \boxed{
290   T^n
291   =
292   \sum_{w\in E^n}L_w
293   =
294   \sum_{w\in E^n}
295   \begin{cases}
296   L_w,&w\text{ composable},\\
297   0,&w\text{ not composable}.
298   \end{cases}
299   }
300 \]
301 Parallel edges occur as distinct summands.
302 \end{theorem}
303 \statusleanthree{Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.transferOp_pow_eq_explicitWordExpansion; Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.transferOp_pow_eq_walkExpansion}
304 
305 \begin{proof}
306 Induction and finite distributivity give
307 \[
308 \left(\sum_{e\in E}L_e\right)^n
309 =
310 \sum_{(e_1,\ldots,e_n)\in E^n}L_{e_n}\cdots L_{e_1}.
311 \]
312 Every noncomposable summand is zero by
313 \cref{thm:nonwalk-vanish}, so inserting the composability filter does not
314 change the sum.  In Lean, tuple concatenation and the successor sum are
315 handled by \leanname{tupleWordOp_snoc} and
316 \leanname{explicitWordExpansion_succ}. The two bridge equalities then yield
317 the displayed theorem.
318 \end{proof}
319 
320 \begin{corollary}[Endpoint coefficient walk sum]
321 \label{cor:word-to-walk-entry}
322 For all $n\in\N$ and $i,j\in V$,
323 \[
324   \boxed{
325   (T^n)_{ji}
326   =
327   \sum_{w\in\Walk_n(i,j)}c^\leftarrow(w).
328   }
329 \]
330 \end{corollary}
331 \statusleanthree{Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.Connects; Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.endpointWalkCoefficientSum; Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.transferOp_pow_apply_eq_sum_walks}
332 
333 \begin{proof}
334 Take the $(j,i)$ entry in \cref{thm:word-to-walk}.  By
335 \cref{lem:word-endpoint}, a surviving word contributes
336 $c^\leftarrow(w)$ exactly when its endpoints are $i$ and $j$, and contributes
337 zero otherwise.  At $n=0$, the identity matrix gives the unique empty
338 diagonal walk.
339 \end{proof}
340 
341 \begin{corollary}[Reachability obstruction at fixed length]
342 \label{cor:fixed-reachability}
343 If $\Walk_n(i,j)=\varnothing$, then $(T^n)_{ji}=0$.
344 \end{corollary}
345 \statusleanthree{Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.transferOp_pow_apply_eq_zero_of_no_walk}
346 
347 \begin{proof}
348 This is immediate from the empty sum in the preceding corollary.
349 \end{proof}
350 
351 \begin{corollary}[Orbit support obstruction]
352 \label{cor:orbit-reachability}
353 Let $S\subseteq V$, and let $x\in R^V$ be supported on $S$.  If $j$ is not
354 reachable by a directed path from any vertex of $S$, then
355 \[
356   (T^nx)_j=0\qquad\text{for every }n\in\N.
357 \]
358 Hence the orbit under $T$ of $x$ cannot generate a vector with a nonzero
359 coordinate at $j$.
360 \end{corollary}
361 \statusleanthree{Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.Reachable; Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.transferOp_pow_mulVec_apply_eq_zero_of_unreachable_support}
362 \statusleanprior{Komorebi.PacketNaturalityCompletion.Reachability.algebraicOrbitHull_le_reachable_support; Komorebi.PacketNaturalityCompletion.Reachability.unreachable_nonzero_packet_obstruction}
363 
364 \begin{proof}
365 Expand $(T^nx)_j=\sum_i(T^n)_{ji}x_i$.  Terms with $i\notin S$ vanish by
366 the support of $x$, and terms with $i\in S$ vanish by
367 \cref{cor:fixed-reachability}.  The final claim follows because the
368 $j$-coordinate also vanishes on every finite linear combination of orbit
369 vectors.
370 \end{proof}
371 
372 \section{Canonical exact coordinate transport}
373 \label{sec:canonical-transport}
374 
375 \subsection{The Chapter III frame model}
376 
377 Let every chart $a$ carry a linear frame equivalence
378 $F_a:M\xrightarrow{\sim}M$.  The formal Chapter III module defines transport
379 from $a$ to $b$ by
380 \[
381 J_{b\leftarrow a}=F_b^{-1}F_a.
382 \]
383 This frame formula means \emph{synthesize in chart \(a\), then
384 analyze in chart \(b\)}.
385 
386 \begin{theorem}[Exact frame transport is coherent]
387 \label{thm:exact-frame-transport}
388 For every $a,b,c$,
389 \[
390 J_{a\leftarrow a}=\id,\qquad
391 J_{a\leftarrow b}J_{b\leftarrow a}=\id,\qquad
392 J_{c\leftarrow b}J_{b\leftarrow a}=J_{c\leftarrow a},
393 \]
394 and therefore
395 \[
396 J_{a\leftarrow c}J_{c\leftarrow b}J_{b\leftarrow a}=\id.
397 \]
398 \end{theorem}
399 \statusleanthree{Komorebi.PaperIII.Transport.exactTransport_self; Komorebi.PaperIII.Transport.exactTransport_roundTrip; Komorebi.PaperIII.Transport.exactTransport_cocycle; Komorebi.PaperIII.Transport.exactTransport_triangleLoop}
400 
401 \begin{proof}
402 Every identity is cancellation of adjacent $F_rF_r^{-1}$ factors.  The Lean
403 definitions use \leanname{LinearEquiv.trans}. The displayed formulas use the
404 equivalent right-to-left notation for function composition fixed in this chapter.
405 \end{proof}
406 
407 \begin{theorem}[Every finite canonical path telescopes]
408 \label{thm:exact-path-transport}
409 Let $p=(a_0,a_1,\ldots,a_n)$ be any finite vertex list and put
410 \[
411 J_p
412 =J_{a_n\leftarrow a_{n-1}}\cdots J_{a_1\leftarrow a_0},
413 \qquad
414 J_{(a_0)}=\id.
415 \]
416 Then
417 \[
418 J_p=J_{a_n\leftarrow a_0}.
419 \]
420 In particular, if $a_n=a_0$, then $J_p=\id$.
421 \end{theorem}
422 \statusleanthree{Komorebi.PaperIII.Transport.pathEndpoint; Komorebi.PaperIII.Transport.exactPathTransport; Komorebi.PaperIII.Transport.exactPathTransport_eq_endpoint; Komorebi.PaperIII.Transport.exactPathTransport_loop}
423 
424 \begin{proof}
425 Induct on the list of successive vertices and apply the cocycle in
426 \cref{thm:exact-frame-transport} at each step.  If the endpoint is the start,
427 the endpoint transport is the identity.
428 \end{proof}
429 
430 \subsection{Exact packet coordinates}
431 
432 The graph model above resolves a fixed scalar matrix.  Coordinate transport
433 is a separate construction.  Let $X$ be an $R$-module, and let
434 \[
435 \cP^a=(P^a_i)_{i\in I_a}
436 \]
437 be a finite complete family of pairwise orthogonal linear idempotents:
438 \[
439 P^a_iP^a_j=\delta_{ij}P^a_i,
440 \qquad
441 \sum_{i\in I_a}P^a_i=I_X.
442 \]
443 Define the exact packet coordinate module
444 \[
445 \Coord(\cP^a)
446 =
447 \left\{(x_i)_{i\in I_a}:P^a_ix_i=x_i\right\}.
448 \]
449 Its analysis and synthesis maps are
450 \[
451 \cA_a(x)=(P^a_ix)_i,
452 \qquad
453 \cS_a((x_i)_i)=\sum_ix_i.
454 \]
455 Completeness and orthogonality give
456 \[
457 \cS_a\cA_a=\id_X,
458 \qquad
459 \cA_a\cS_a=\id_{\Coord(\cP^a)}.
460 \]
461 
462 \begin{keyidea}[title={What a packet coordinate contains}]
463 A packet coordinate is a whole vector fixed by its projector. Analysis splits
464 an ambient vector into these components, and synthesis adds them back. The
465 transport between exact systems keeps the ambient vector and changes its
466 packet presentation.
467 \end{keyidea}
468 
469 \begin{definition}[Canonical exact coordinate transport]
470 \label{def:canonical-J}
471 For two exact packet systems on the same ambient module, define
472 \[
473   J^X_{b\leftarrow a}
474   =
475   \cA_b\cS_a:
476   \Coord(\cP^a)\longrightarrow\Coord(\cP^b).
477 \]
478 The arrow points from the source coordinate system $a$ to the target
479 coordinate system $b$.
480 \end{definition}
481 \statusleanprior{Komorebi.PaperII.NestedRefinement.refineCoordinates; Komorebi.PaperII.NestedRefinement.coordinateRefinementEquiv}
482 
483 \begin{theorem}[Identity, inverse, and cocycle for canonical transport]
484 \label{thm:J-cocycle}
485 For any exact packet systems $a,b,c$ on $X$,
486 \[
487 J^X_{a\leftarrow a}=\id,
488 \qquad
489 \left(J^X_{b\leftarrow a}\right)^{-1}=J^X_{a\leftarrow b},
490 \qquad
491 J^X_{c\leftarrow b}J^X_{b\leftarrow a}=J^X_{c\leftarrow a}.
492 \]
493 \end{theorem}
494 \statusleanprior{Komorebi.PaperII.NestedRefinement.refineCoordinates_self; Komorebi.PaperII.NestedRefinement.coarsenCoordinates_refineCoordinates; Komorebi.PaperII.NestedRefinement.refineCoordinates_coarsenCoordinates; Komorebi.PaperII.NestedRefinement.refineCoordinates_comp; Komorebi.PaperII.NestedRefinement.coordinateRefinementEquiv_trans}
495 
496 \begin{proof}
497 Insert $\cS_b\cA_b=\id_X$:
498 \[
499 J^X_{c\leftarrow b}J^X_{b\leftarrow a}
500 =\cA_c\cS_b\cA_b\cS_a
501 =\cA_c\cS_a
502 =J^X_{c\leftarrow a}.
503 \]
504 The identity statement is $\cA_a\cS_a=\id$.  Setting $c=a$ in the cocycle
505 gives $J^X_{a\leftarrow b}J^X_{b\leftarrow a}=\id$. Interchanging $a$ and $b$
506 gives the other composition, so the two transports are inverses.
507 \end{proof}
508 
509 If $F:X\to Y$ is linear and $\cP^a,\cP^b$ are source packet systems while
510 $\cQ^r,\cQ^s$ are target packet systems, put
511 \[
512 \widehat F_{r\leftarrow a}
513 =
514 \cA^Y_rF\cS^X_a.
515 \]
516 
517 \begin{theorem}[Canonical coordinate naturality]
518 \label{thm:canonical-naturality}
519 The exact coordinate representation preserves typed composition and satisfies
520 \[
521 J^Y_{s\leftarrow r}\widehat F_{r\leftarrow a}
522 =
523 \widehat F_{s\leftarrow b}J^X_{b\leftarrow a}.
524 \]
525 \end{theorem}
526 \statusleanprior{Komorebi.PaperII.NestedRefinement.coordinateOperator_comp; Komorebi.PaperII.NestedRefinement.coordinateOperator_naturality}
527 
528 \begin{proof}
529 Both sides reduce to $\cA^Y_sF\cS^X_a$ after inserting the appropriate
530 synthesis--analysis identity.  The composition law is the same calculation
531 with the middle ambient module inserted.
532 \end{proof}
533 
534 \begin{corollary}[Canonical triangle holonomy is trivial]
535 \label{cor:J-flat}
536 For every triple $a,b,c$,
537 \[
538 J^X_{a\leftarrow c}J^X_{c\leftarrow b}J^X_{b\leftarrow a}=\id.
539 \]
540 \end{corollary}
541 \statusleanprior{Komorebi.PaperII.NestedRefinement.refineCoordinates_comp; Komorebi.PaperII.NestedRefinement.refineCoordinates_self}
542 
543 \begin{boundary}[Refinement is not reduction]
544 Although Chapter II uses the name \emph{refineCoordinates}, $J$ is an
545 equivalence between two complete coordinate presentations.  It neither
546 truncates packets nor projects to a smaller state space.  Any lossy
547 restriction, interpolation, or learned identification is extra data and
548 cannot inherit \cref{thm:J-cocycle} without proof.
549 \end{boundary}
550 

Back to source controls

Back to Realization Calculus