Paper III: Typed Transfer, Nonlinear Packets, and Obstruction Theory

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 \part{Finite typed transfer and the formal contract}\label{part:finite}
2 \noindent The finite release 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 thirty original result environments and their proof bodies are retained. The source contract has 41 mapping rows because it also includes definitions and other interfaces.
3 
4 \medskip\noindent The preserved v1.0.1 release records Lean v4.34.0-rc2 against Mathlib revision \leanname{aeb72f1e9981b6d35b426b16dca7759be3e7ba06} \cite{lean,mathlib}. The current release rebuilds the Paper III source at these exact pins and records fresh kernel replay and axiom checks. References to declarations from Papers I--II retain their explicitly inherited status. The companion Lean guide distinguishes the original finite map from the additional packet-coordinate and analytic interfaces.
5 \section{Purpose and formal status}
6 \label{sec:purpose}
7 
8 Paper I fixed typed seeds, operator grammars, exact projector packets,
9 generated hulls, and reconstruction \cite{paperI}.  Paper II added coherent
10 refinement coordinates, weighted transfer, arithmetic separation, and linear
11 defect identities \cite{paperII}.  The present paper 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 Paper 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 Paper III}: the displayed scope is no stronger
32 than the named compiled declaration in the released Paper III module.
33 \item \textbf{Inherited Lean-backed}: the displayed result is supplied by the
34 frozen formal contract of Paper I or 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 
Statement: Final theorem denominator39 \begin{boundary}[Final theorem denominator]
40 The completion denominator of the finite v1.0.1 contract consists of the
41 thirty result environments in Part~I. Of these, 26 resolve to compiled
42 Paper III declarations and four resolve to the frozen Papers 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 
Statement: Packet graph and scalar edge system64 \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 
Statement: Declared support96 \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 
Statement: Typed interface annihilation103 \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 
Statement: Collapse of a matched edge pair121 \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 matrix-product sum 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 
Statement: Current fiber scope142 \begin{boundary}[Current fiber scope]
143 The compiled Paper 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 Paper 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 
Statement: Composable word and execution operator171 \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 
Statement: First broken interface188 \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 
Statement: Noncomposable words vanish195 \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 
Statement: Recursive word expansion210 \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 
Statement: Transfer power equals recursive word expansion221 \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 
Statement: One word is one endpoint block254 \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 
Statement: Finite operator expansion from words to walks285 \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 
Statement: Endpoint coefficient walk sum320 \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 
Statement: Reachability obstruction at fixed length341 \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 
Statement: Orbit support obstruction351 \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 Paper III frame model}
376 
377 Let every chart $a$ carry a linear frame equivalence
378 $F_a:M\xrightarrow{\sim}M$.  The formal Paper 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 
Statement: Exact frame transport is coherent386 \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 function-composition notation fixed in this paper.
405 \end{proof}
406 
Statement: Every finite canonical path telescopes407 \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 
Statement: Canonical exact coordinate transport469 \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 
Statement: Identity, inverse, and cocycle for canonical transport483 \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 
Statement: Canonical coordinate naturality517 \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 
Statement: Canonical triangle holonomy is trivial534 \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 
Statement: Refinement is not reduction543 \begin{boundary}[Refinement is not reduction]
544 Although Paper 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 Paper III: Typed Transfer, Nonlinear Packets, and Obstruction Theory