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 \section{A distinct noncanonical connection API}
2 \label{sec:connection}
3 
4 \subsection{The minimal compiled API}
5 
6 The compiled Chapter III API assumes only normalization at each chart.  All
7 chart transports act on one module $M$, so chart labels distinguish routes
8 but not Lean types.
9 
10 \begin{definition}[Noncanonical connection normalized at each chart]
11 \label{def:minimal-connection}
12 A minimal connection is a family
13 \[
14 \Gamma_{b\leftarrow a}\in\operatorname{Aut}_R(M)
15 \qquad(a,b\in B)
16 \]
17 with only
18 \[
19 \Gamma_{a\leftarrow a}=\id_M.
20 \]
21 Neither inversion on reversed edges nor the cocycle law is a field of the
22 structure.
23 \end{definition}
24 \statusleanthree{Komorebi.PaperIII.Transport.Connection}
25 
26 At a triple $(a,b,c)$, the compiled cocycle predicate is
27 \[
28 \Gamma_{c\leftarrow b}\Gamma_{b\leftarrow a}
29 =\Gamma_{c\leftarrow a}.
30 \]
31 Flatness means this equality holds for every triple.  The formal
32 multiplicative relative defect and triangle holonomy are
33 \[
34 D^\times_{c,b,a}
35 =
36 \bigl(\Gamma_{c\leftarrow b}\Gamma_{b\leftarrow a}\bigr)
37 \Gamma_{c\leftarrow a}^{-1},
38 \qquad
39 H_{c,b,a}
40 =
41 \Gamma_{a\leftarrow c}
42 \Gamma_{c\leftarrow b}
43 \Gamma_{b\leftarrow a}.
44 \]
45 The defect is based at the target $c$.  The holonomy is based at $a$.
46 \statusleanthree{Komorebi.PaperIII.Transport.Connection.CocycleAt; Komorebi.PaperIII.Transport.Connection.Flat; Komorebi.PaperIII.Transport.Connection.cocycleDefect; Komorebi.PaperIII.Transport.Connection.triangleHolonomy}
47 
48 \begin{theorem}[Checked flatness consequences]
49 \label{thm:minimal-flatness}
50 For the minimal connection API, flatness implies
51 \[
52 D^\times_{c,b,a}=\id_M,
53 \qquad
54 H_{c,b,a}=\id_M
55 \]
56 for every $a,b,c$.
57 \end{theorem}
58 \statusleanthree{Komorebi.PaperIII.Transport.Connection.cocycleDefect_eq_refl_of_flat; Komorebi.PaperIII.Transport.Connection.triangleHolonomy_eq_refl_of_flat}
59 
60 \begin{proof}
61 Flatness replaces the two-edge route in $D^\times$ by the direct route,
62 which cancels its inverse.  For $H$, flatness first collapses $a\to b\to c$
63 to $a\to c$, then collapses $a\to c\to a$ to the normalized transport
64 $a\to a$.
65 \end{proof}
66 
67 \begin{proposition}[The minimal API admits nontrivial holonomy]
68 \label{prop:twisted-loop}
69 There is a connection on three points over $\mathbb Q$ for which transport
70 $0\to1$ is multiplication by $2$, every other transport between distinct
71 endpoints is the identity, and
72 \[
73 H_{2,1,0}(1)=2.
74 \]
75 In particular $H_{2,1,0}\ne\id$.
76 \end{proposition}
77 \statusleanthree{Komorebi.PaperIII.Transport.twistedThreePointConnection; Komorebi.PaperIII.Transport.twisted_triangleHolonomy_apply_one; Komorebi.PaperIII.Transport.twisted_triangleHolonomy_ne_refl}
78 
79 \begin{boundary}[Why the minimal defect and loop are distinct]
80 Without reverse-edge inversion,
81 $\Gamma_{a\leftarrow c}$ need not equal
82 $\Gamma_{c\leftarrow a}^{-1}$.  Therefore the multiplicative relative defect
83 $D^\times_{c,b,a}$ and triangle holonomy $H_{c,b,a}$ are different
84 comparisons.  The formal module proves that global flatness trivializes both.
85 It does not identify them for an arbitrary connection.
86 \end{boundary}
87 
88 \begin{figure}[H]
89 \centering
90 \includegraphics[width=.96\linewidth]{transport_vs_connection.pdf}
91 \caption{Exact coordinate transport and connection transport are distinct.
92 The canonical loop telescopes to the identity.  A chosen connection may
93 carry nontrivial holonomy, which transforms by conjugation under gauge.}
94 \label{fig:transport-connection}
95 \end{figure}
96 
97 \Cref{fig:transport-connection} records this separation visually: the exact
98 coordinate route telescopes, whereas the chosen connection route may carry a
99 nonidentity loop.
100 
101 \begin{keyidea}[title={Coordinate transport and connection choice}]
102 Canonical transport compares exact coordinate descriptions of the same
103 object.  Its loops telescope.  A connection supplies a separate family of
104 comparison maps, so its loops can carry information about that choice.
105 The distinction keeps coordinate identities separate from connection
106 assumptions.
107 \end{keyidea}
108 
109 \subsection{A stronger reversible pair API}
110 
111 Let $R$ be a commutative ring, let $B$ be a type of charts or refinement
112 states, and let each $C_a$ be an $R$-module.  The chart type is not assumed
113 finite.  The following definition is deliberately not derived from analysis
114 and synthesis.
115 
116 \begin{definition}[Normalized reversible connection]
117 \label{def:connection}
118 A normalized reversible connection is a family of linear equivalences
119 \[
120 \Gamma_{b\leftarrow a}:C_a\xrightarrow{\;\sim\;}C_b
121 \qquad(a,b\in B)
122 \]
123 such that
124 \[
125 \Gamma_{a\leftarrow a}=\id,
126 \qquad
127 \Gamma_{a\leftarrow b}=\Gamma_{b\leftarrow a}^{-1}.
128 \]
129 No cocycle equation is included in the structure.
130 \end{definition}
131 \statusleanthree{Komorebi.PaperIII.Transport.ReversibleConnection}
132 
133 This adds heterogeneous fibers and inversion on reversed edges to the
134 homogeneous minimal connection.  The connection is still a separate choice
135 of maps, rather than a definition of canonical coordinate transport.
136 
137 \begin{definition}[Calibration and flatness]
138 \label{def:calibration-flatness}
139 When the $C_a$ are exact packet coordinates of one ambient module, the
140 connection is \emph{canonically calibrated} if
141 \[
142 \Gamma_{b\leftarrow a}=J_{b\leftarrow a}
143 \quad\text{for every }a,b.
144 \]
145 It is \emph{flat} if
146 \[
147 \Gamma_{c\leftarrow b}\Gamma_{b\leftarrow a}
148 =
149 \Gamma_{c\leftarrow a}
150 \quad\text{for every }a,b,c.
151 \]
152 The canonical connection is flat.  A general flat connection is proved in
153 \cref{thm:flat-gauge-canonical} to be related to it by a gauge change.
154 \end{definition}
155 \statusleanthree{Komorebi.PaperIII.Transport.ReversibleConnection.CocycleAt; Komorebi.PaperIII.Transport.ReversibleConnection.Flat; Komorebi.PaperIII.Transport.ReversibleConnection.canonicalConnection; Komorebi.PaperIII.Transport.ReversibleConnection.canonicalConnection_flat}
156 
157 The words \emph{calibrated} and \emph{flat} have only the algebraic meanings
158 displayed above.
159 
160 \begin{remark}[A connection on a chart graph]
161 One may specify $\Gamma_e$ only on the oriented edges of a chart graph,
162 together with inverse maps on reversed edges.  Path transport and loop
163 holonomy below still make sense.  A direct cocycle defect for $(a,b,c)$,
164 however, requires a declared direct transport from $a$ to $c$.  The pairwise
165 API in \cref{def:connection} keeps this comparison total.
166 \end{remark}
167 
168 \subsection{Cocycle defect and triangle holonomy}
169 
170 The commutative ring hypothesis makes subtraction of linear maps available
171 from this point through \cref{sec:obstruction-packets}.
172 
173 \begin{definition}[Cocycle defect]
174 \label{def:cocycle-defect}
175 For $a,b,c\in B$, define the additive cocycle defect
176 \[
177 \Delta_{c,b,a}
178 =
179 \Gamma_{c\leftarrow b}\Gamma_{b\leftarrow a}
180 -\Gamma_{c\leftarrow a}
181 \in\Hom_R(C_a,C_c).
182 \]
183 \end{definition}
184 \statusleanthree{Komorebi.PaperIII.Transport.ReversibleConnection.cocycleDefect}
185 
186 The manuscript subscript order is target, intermediate, source.  The Lean
187 arguments are supplied in traversal order \leanname{(a,b,c)}.
188 
189 \begin{definition}[Triangle holonomy]
190 \label{def:triangle-holonomy}
191 The triangle holonomy based at $a$ is
192 \[
193 H_{c,b,a}
194 =
195 \Gamma_{a\leftarrow c}
196 \Gamma_{c\leftarrow b}
197 \Gamma_{b\leftarrow a}
198 \in\operatorname{Aut}_R(C_a).
199 \]
200 It traverses $a\to b\to c\to a$.
201 \end{definition}
202 \statusleanthree{Komorebi.PaperIII.Transport.ReversibleConnection.triangleHolonomy; Komorebi.PaperIII.Transport.ReversibleConnection.triangleObstruction}
203 
204 Holonomy is attached to the chosen connection $\Gamma$, never to an
205 unspecified coordinate change.
206 
207 \begin{theorem}[Identity between defect and holonomy]
208 \label{thm:defect-holonomy}
209 For every triple $(a,b,c)$,
210 \[
211 \boxed{
212 H_{c,b,a}-\id_{C_a}
213 =
214 \Gamma_{a\leftarrow c}\Delta_{c,b,a}.
215 }
216 \]
217 Consequently,
218 \[
219 \Delta_{c,b,a}=0
220 \quad\Longleftrightarrow\quad
221 H_{c,b,a}=\id_{C_a}.
222 \]
223 \end{theorem}
224 \statusleanthree{Komorebi.PaperIII.Transport.ReversibleConnection.triangleHolonomy_sub_id; Komorebi.PaperIII.Transport.ReversibleConnection.cocycleDefect_eq_zero_iff_triangleHolonomy_eq_refl}
225 
226 \begin{proof}
227 Using reversibility,
228 \[
229 \begin{aligned}
230 \Gamma_{a\leftarrow c}\Delta_{c,b,a}
231 &=
232 \Gamma_{a\leftarrow c}
233 \Gamma_{c\leftarrow b}
234 \Gamma_{b\leftarrow a}
235 -
236 \Gamma_{a\leftarrow c}\Gamma_{c\leftarrow a}\\
237 &=H_{c,b,a}-\id_{C_a}.
238 \end{aligned}
239 \]
240 Left composition by the equivalence $\Gamma_{a\leftarrow c}$ is injective,
241 which gives the equivalence of the two vanishing statements.
242 \end{proof}
243 
244 \begin{corollary}[Canonical transport has zero connection defect]
245 \label{cor:canonical-zero-defect}
246 If $\Gamma_{b\leftarrow a}=J_{b\leftarrow a}$, then
247 \[
248 \Delta_{c,b,a}=0,
249 \qquad
250 H_{c,b,a}=\id
251 \]
252 for all triples.
253 \end{corollary}
254 \statusleanthree{Komorebi.PaperIII.Transport.ReversibleConnection.canonicalTransport_zero_connectionDefect; Komorebi.PaperIII.Transport.ReversibleConnection.canonicalTransport_triangleHolonomy_eq_refl}
255 
256 \begin{proof}
257 The defect vanishes by the canonical cocycle in
258 \cref{thm:J-cocycle}. Apply \cref{thm:defect-holonomy}.
259 \end{proof}
260 
261 \subsection{Paths and endpoint independence}
262 
263 \begin{definition}[Connection transport along a path]
264 \label{def:path-transport}
265 For a vertex sequence
266 $p=(a_0,a_1,\ldots,a_n)$, define
267 \[
268 \Gamma_p
269 =
270 \Gamma_{a_n\leftarrow a_{n-1}}\cdots
271 \Gamma_{a_1\leftarrow a_0},
272 \qquad
273 \Gamma_{(a_0)}=\id_{C_{a_0}}.
274 \]
275 If $a_n=a_0$, then $\Gamma_p$ is the holonomy of the loop $p$.
276 \end{definition}
277 \statusleanthree{Komorebi.PaperIII.Transport.ReversibleConnection.pathTransport; Komorebi.PaperIII.Transport.ReversibleConnection.VertexPath; Komorebi.PaperIII.Transport.ReversibleConnection.indexedPathTransport}
278 
279 Products follow path order: the first traversed edge acts on the right.
280 
281 \begin{proposition}[Flat pair transport collapses to endpoints]
282 \label{prop:flat-endpoints}
283 If $\Gamma$ is flat, then every path satisfies
284 \[
285 \Gamma_p=\Gamma_{a_n\leftarrow a_0}.
286 \]
287 In particular, every loop has identity holonomy.
288 \end{proposition}
289 \statusleanthree{Komorebi.PaperIII.Transport.ReversibleConnection.pathTransport_eq_direct_of_flat; Komorebi.PaperIII.Transport.ReversibleConnection.indexedPathTransport_eq_direct_of_flat; Komorebi.PaperIII.Transport.ReversibleConnection.indexedLoopTransport_eq_refl_of_flat}
290 
291 \begin{proof}
292 Induct on the path length.  Appending $a_{n+1}$ left-multiplies the
293 inductive expression by $\Gamma_{a_{n+1}\leftarrow a_n}$, and flatness
294 replaces the two factors by
295 $\Gamma_{a_{n+1}\leftarrow a_0}$.  For a loop, normalization gives
296 $\Gamma_{a_0\leftarrow a_0}=\id$.
297 \end{proof}
298 
299 \begin{remark}
300 The converse \emph{trivial holonomy implies flatness} depends on which loops
301 are present in an API defined on a chart graph.  In the complete pair API,
302 triviality of every triangle holonomy is equivalent to flatness by
303 \cref{thm:defect-holonomy}.  No theorem about topological simple connectivity is
304 being invoked.
305 \end{remark}
306 
307 \section{Gauge covariance and comparison with canonical transport}
308 \label{sec:gauge}
309 
310 \begin{definition}[Gauge change]
311 \label{def:gauge-change}
312 A gauge is a family of automorphisms $G_a\in\operatorname{Aut}_R(C_a)$.
313 It acts on a connection by
314 \[
315 \Gamma^G_{b\leftarrow a}
316 =
317 G_b\Gamma_{b\leftarrow a}G_a^{-1}.
318 \]
319 \end{definition}
320 \statusleanthree{Komorebi.PaperIII.Transport.ReversibleConnection.Gauge; Komorebi.PaperIII.Transport.ReversibleConnection.gauge}
321 
322 A gauge changes coordinate representatives at each chart.  The chart graph
323 stays the same.
324 
325 \begin{theorem}[Gauge covariance]
326 \label{thm:gauge-covariance}
327 The defect and triangle holonomy transform as
328 \[
329 \Delta^G_{c,b,a}
330 =G_c\Delta_{c,b,a}G_a^{-1},
331 \qquad
332 H^G_{c,b,a}
333 =G_aH_{c,b,a}G_a^{-1}.
334 \]
335 Thus flatness and triviality of triangle holonomy are gauge invariant.
336 \end{theorem}
337 \statusleanthree{Komorebi.PaperIII.Transport.ReversibleConnection.gauge_cocycleDefect; Komorebi.PaperIII.Transport.ReversibleConnection.gauge_triangleHolonomy; Komorebi.PaperIII.Transport.ReversibleConnection.gauge_flat_iff; Komorebi.PaperIII.Transport.ReversibleConnection.gauge_triangleHolonomy_eq_refl_iff}
338 
339 \begin{proof}
340 Substitute the definition of $\Gamma^G$.  Adjacent factors
341 $G_b^{-1}G_b$ and $G_c^{-1}G_c$ cancel.  In the defect, both the composite
342 and direct terms acquire the same outer factors $G_c$ and $G_a^{-1}$.  In
343 the loop, all inner factors cancel and only conjugation at the base remains.
344 \end{proof}
345 
346 \begin{theorem}[Flat connections are gauges of the canonical pair transport]
347 \label{thm:flat-gauge-canonical}
348 Suppose the $C_a$ are exact packet coordinate modules for one ambient module,
349 so the canonical $J_{b\leftarrow a}$ is available.  If $\Gamma$ is a flat
350 normalized reversible pair connection, choose $o\in B$ and set
351 \[
352 G_a=\Gamma_{a\leftarrow o}J_{o\leftarrow a}.
353 \]
354 Then every pair transport satisfies
355 \[
356 \boxed{
357 \Gamma_{b\leftarrow a}
358 =G_bJ_{b\leftarrow a}G_a^{-1}.
359 }
360 \]
361 \end{theorem}
362 \statusleanthree{Komorebi.PaperIII.Transport.ReversibleConnection.flatGauge; Komorebi.PaperIII.Transport.ReversibleConnection.flat_isGaugeOfCanonical}
363 
364 \begin{proof}
365 Reversibility gives
366 $G_a^{-1}=J_{a\leftarrow o}\Gamma_{o\leftarrow a}$.  Therefore
367 \[
368 \begin{aligned}
369 G_bJ_{b\leftarrow a}G_a^{-1}
370 &=
371 \Gamma_{b\leftarrow o}
372 J_{o\leftarrow b}J_{b\leftarrow a}
373 J_{a\leftarrow o}
374 \Gamma_{o\leftarrow a}\\
375 &=
376 \Gamma_{b\leftarrow o}\Gamma_{o\leftarrow a}\\
377 &=
378 \Gamma_{b\leftarrow a}.
379 \end{aligned}
380 \]
381 The first reduction uses the canonical cocycle twice. The second uses
382 flatness of $\Gamma$.
383 \end{proof}
384 
385 \begin{boundary}[Flat does not mean calibrated]
386 The theorem produces a gauge relating $\Gamma$ to $J$.  It does not prove
387 $\Gamma=J$ before that gauge is chosen.  Conversely, nontrivial triangle
388 holonomy cannot be removed by a gauge, because conjugation cannot turn a
389 nonidentity automorphism into the identity.
390 \end{boundary}
391 
392 \section{Obstruction packets: local certificates and holonomy blocks}
393 \label{sec:obstruction-packets}
394 
395 \subsection{The generic compiled certificate}
396 
397 Let $\mathsf{Candidate}$, $\mathsf{Packet}$, and $\mathsf{Residual}$ be
398 arbitrary types, with a distinguished
399 $0\in\mathsf{Residual}$, and let
400 \[
401 r:\mathsf{Candidate}\longrightarrow
402 \mathsf{Packet}\longrightarrow\mathsf{Residual}
403 \]
404 be a residual function.
405 
406 \begin{definition}[Solution and obstruction packet for a candidate]
407 \label{def:generic-obstruction}
408 A candidate $x$ is a solution when
409 \[
410 \operatorname{IsSolution}_r(x)
411 \quad\Longleftrightarrow\quad
412 \forall p,\ r(x,p)=0.
413 \]
414 An obstruction packet for $x$ is a pair consisting of a named packet $p$
415 and a certificate $r(x,p)\ne0$.
416 \end{definition}
417 \statusleanthree{Komorebi.PaperIII.NonlinearObstructions.IsSolution; Komorebi.PaperIII.NonlinearObstructions.ObstructionPacket}
418 
419 \begin{theorem}[Exact logical force of a local obstruction]
420 \label{thm:generic-obstruction}
421 Every obstruction packet for $x$ proves that $x$ is not a solution, and
422 \[
423 \neg\operatorname{IsSolution}_r(x)
424 \quad\Longleftrightarrow\quad
425 \text{there exists an obstruction packet for }x.
426 \]
427 The reverse implication from failure to a packet witness is classical and
428 does not require the packet type to be finite.
429 \end{theorem}
430 \statusleanthree{Komorebi.PaperIII.NonlinearObstructions.ObstructionPacket.not_isSolution; Komorebi.PaperIII.NonlinearObstructions.obstructionPacket_of_not_isSolution; Komorebi.PaperIII.NonlinearObstructions.not_isSolution_iff_nonempty_obstructionPacket}
431 
432 \begin{proof}
433 A purported solution would make the residual vanish at the certified packet,
434 contradicting its nonzero field.  Conversely, if no packet carries a nonzero
435 residual, then every residual is zero and the candidate satisfies the
436 definition of solution.
437 \end{proof}
438 
439 \begin{interpretation}[title={What one obstruction certifies}]
440 The certificate answers one question: does this specified candidate satisfy
441 every declared packet condition?  One nonzero residual settles that question
442 for this candidate.  A statement that no candidate can solve the problem
443 would require an obstruction for every candidate.
444 \end{interpretation}
445 
446 \begin{boundary}[Candidate-specific means candidate-specific]
447 The theorem rules out the named $x$.  It neither constructs a solution nor
448 shows that every candidate is obstructed.  It provides no minimality,
449 stability, computability, or classification theorem for the packet witness.
450 \end{boundary}
451 
452 \subsection{Specialization to holonomy blocks}
453 
454 For a reversible connection, specialize the generic residual at a fixed
455 triangle by taking a packet label to be a pair $(\mu,\nu)$ and the residual
456 to be the corresponding block of $H-\id$.  A nonzero block, together with its
457 label and a proof of nonvanishing, gives an obstruction packet certificate
458 in the sense of \cref{def:generic-obstruction}.  The reconstruction theorem
459 below supplies the further step: vanishing of all these local residuals is
460 equivalent to the cocycle equation at that triangle.
461 
462 Fix a triangle $(a,b,c)$ and resolve the base fiber $C_a$ by a finite complete
463 family of idempotents $(\Pi^a_\mu)_{\mu\in I_a}$.  Orthogonality may also hold,
464 as it does for the exact range coordinate projectors below, but the compiled
465 reconstruction theorem does not require it.  In exact range coordinates,
466 $\Pi^a_\mu$ is simply the projector that retains component $\mu$ and zeros
467 the other components.
468 
469 \begin{definition}[Holonomy obstruction and packet residuals]
470 \label{def:obstruction-packet}
471 Define
472 \[
473 \Ob_{c,b,a}=H_{c,b,a}-\id_{C_a},
474 \qquad
475 \Ob^{\mu\nu}_{c,b,a}
476 =
477 \Pi^a_\mu\Ob_{c,b,a}\Pi^a_\nu.
478 \]
479 The map $\Ob^{\mu\nu}_{c,b,a}$ is the obstruction block, or packet residual,
480 from input packet $\nu$ to output packet $\mu$.  If it is nonzero, then
481 $(\mu,\nu)$ and that nonvanishing proof form an obstruction packet
482 certificate.  Diagonal blocks detect holonomy within one packet.  Off-diagonal
483 blocks detect packet mixing induced by holonomy.
484 \end{definition}
485 \statusleanthree{Komorebi.PaperIII.HolonomyBlocks.PacketResolution; Komorebi.PaperIII.HolonomyBlocks.PacketResolution.block}
486 
487 The certificate records a specified holonomy defect, the label of an input
488 and output packet, and a proof that the corresponding block is nonzero.
489 
490 \begin{theorem}[Exact reconstruction and detection by obstruction blocks]
491 \label{thm:obstruction-detection}
492 The total obstruction has the exact finite resolution
493 \[
494 \boxed{
495 \Ob_{c,b,a}
496 =
497 \sum_{\mu,\nu\in I_a}
498 \Ob^{\mu\nu}_{c,b,a}.
499 }
500 \]
501 Moreover, the following are equivalent:
502 \begin{enumerate}[label=(\roman*)]
503 \item $\Delta_{c,b,a}=0$;
504 \item $H_{c,b,a}=\id$;
505 \item $\Ob_{c,b,a}=0$;
506 \item $\Ob^{\mu\nu}_{c,b,a}=0$ for every $\mu,\nu$.
507 \end{enumerate}
508 \end{theorem}
509 \statusleanthree{Komorebi.PaperIII.HolonomyBlocks.obstruction_sum_blocks; Komorebi.PaperIII.HolonomyBlocks.obstructionBlocks_zero_iff; Komorebi.PaperIII.HolonomyBlocks.obstructionDetection_equivalences}
510 
511 \begin{proof}
512 Insert completeness on both sides:
513 \[
514 \Ob
515 =
516 \left(\sum_\mu\Pi^a_\mu\right)
517 \Ob
518 \left(\sum_\nu\Pi^a_\nu\right)
519 =
520 \sum_{\mu,\nu}\Pi^a_\mu\Ob\Pi^a_\nu.
521 \]
522 Thus (iv) implies (iii), and (iii) implies (iv) by composition with the
523 projectors.  Conditions (ii) and (iii) are equivalent by the definition of
524 $\Ob$ and additive cancellation.
525 Conditions (i) and (ii) are equivalent by
526 \cref{thm:defect-holonomy}.
527 \end{proof}
528 
529 \begin{keyidea}[title={Why both packet indices matter}]
530 For the declared finite complete resolution, reconstruction uses both
531 packet indices.  Inspecting only diagonal blocks can miss transport from one
532 packet to another.  The full family records that mixing and reconstructs the
533 total obstruction exactly.
534 \end{keyidea}
535 
536 \Cref{fig:holonomy-obstruction-blocks} depicts the finite block resolution
537 on both sides of the obstruction and the off-diagonal blocks that witness
538 packet mixing.
539 
540 \begin{figure}[H]
541 \centering
542 \includegraphics[width=.96\linewidth]{holonomy_obstruction_blocks.pdf}
543 \caption{A finite complete packet resolution reconstructs the total holonomy
544 obstruction from blocks indexed by input and output packets.  A nonzero
545 off-diagonal block is an exact witness of packet mixing.}
546 \label{fig:holonomy-obstruction-blocks}
547 \end{figure}
548 
549 \begin{corollary}[Witness supported in one packet]
550 \label{cor:packet-witness}
551 If $\Ob^{\mu\nu}_{c,b,a}\ne0$, then there is a vector $x$ supported in packet
552 $\nu$ such that
553 \[
554 \Pi^a_\mu\Ob_{c,b,a}x\ne0.
555 \]
556 Such an $x$ is an exact finite witness of nonflatness.
557 \end{corollary}
558 \statusleanthree{Komorebi.PaperIII.HolonomyBlocks.exists_packetWitness_of_obstructionBlock_ne_zero}
559 
560 \begin{proof}
561 Classically choose $y$ on which the nonzero linear map
562 $\Pi^a_\mu\Ob\Pi^a_\nu$ is nonzero and set $x=\Pi^a_\nu y$.
563 Idempotence gives $\Pi^a_\nu x=x$, and the required output is the chosen
564 nonzero value.
565 \end{proof}
566 
567 \subsection{Gauge behavior of packet blocks}
568 
569 Vanishing or nonvanishing of the total triangle obstruction is gauge invariant
570 by \cref{thm:gauge-covariance}, but a fixed packet pattern need not be.  A
571 general $G_a$ can mix the projectors $\Pi^a_\mu$.
572 
573 \begin{proposition}[Gauge covariance when packet projectors are preserved]
574 \label{prop:packet-gauge}
575 If $G_a\Pi^a_\mu=\Pi^a_\mu G_a$ for every $\mu$, then
576 \[
577 \left(\Ob^G\right)^{\mu\nu}
578 =
579 G_a\Ob^{\mu\nu}G_a^{-1}.
580 \]
581 Consequently the zero/nonzero status of each obstruction block is preserved
582 by gauges that preserve the packet projectors.
583 \end{proposition}
584 \statusleanthree{Komorebi.PaperIII.HolonomyBlocks.obstructionBlock_gauge_of_commutes; Komorebi.PaperIII.HolonomyBlocks.obstructionBlock_gauge_eq_zero_iff}
585 
586 \begin{proof}
587 Use $\Ob^G=G_a\Ob G_a^{-1}$ and commute $G_a$ and $G_a^{-1}$ through the
588 two packet projectors.  Composition by an equivalence is injective in both
589 directions.
590 \end{proof}
591 
592 \begin{boundary}[Packet patterns are not absolute]
593 Without the commutation hypothesis in \cref{prop:packet-gauge}, only the
594 vanishing of the total obstruction is gauge invariant.  The location of
595 individual nonzero blocks may change under a gauge that mixes packets.
596 \end{boundary}
597 
598 \section{Products supported in packets and holonomy walks}
599 \label{sec:holonomy-walks}
600 
601 The passage from words to walks also applies to products of different matrices.
602 Let $V$
603 be one finite packet type, let $R$ be a semiring, and let
604 $B_1,\ldots,B_m\in R^{V\times V}$ be a finite sequence of possibly different
605 packet matrices.  Rows are targets and columns are sources as before.
606 
607 \begin{proposition}[Packet path expansion for different matrices]
608 \label{prop:heterogeneous-path}
609 For $i,j\in V$ and $m\geq1$, set $i_0=i$ and $i_m=j$.  Then
610 \[
611 \boxed{
612 (B_m\cdots B_1)_{ji}
613 =
614 \sum_{(i_1,\ldots,i_{m-1})\in V^{m-1}}
615   B_m[i_m,i_{m-1}]\cdots B_1[i_1,i_0].
616 }
617 \]
618 When $m=1$, the sum is over the unique empty tuple and its summand is
619 $B_1[j,i]$.
620 For $m=0$, the product is the identity and the entry is the Kronecker delta
621 $\delta_{ji}$.  If every $B_r[q,p]$ vanishes outside a declared relation
622 $\mathcal R_r(p,q)$, then the endpoint entry is zero whenever there is no
623 packet path compatible with the successive relations.
624 \end{proposition}
625 \statusleanthree{Komorebi.PaperIII.EdgeOperators.heterogeneousProduct; Komorebi.PaperIII.EdgeOperators.heterogeneousPathSum; Komorebi.PaperIII.EdgeOperators.heterogeneousPacketPathExpansion; Komorebi.PaperIII.EdgeOperators.SupportedStep; Komorebi.PaperIII.EdgeOperators.SupportedPath; Komorebi.PaperIII.EdgeOperators.heterogeneousProduct_apply_eq_zero_of_no_supportedPath}
626 
627 \begin{proof}
628 Expand each matrix product entry and distribute the finite sums.  Induction on
629 the factor list yields the displayed path sum, with the empty list evaluated
630 as the identity matrix.  If no supported intermediate packet exists, every
631 summand contains an entry that is zero by its declared support relation.
632 \end{proof}
633 
634 \begin{boundary}[Changing packet types along a chain]
635 The compiled theorems
636 \leanname{heterogeneousPacketPathExpansion_two} and
637 \leanname{heterogeneousPacketPathExpansion_three} allow different packet
638 types at the successive stages of two- and three-factor products.  The
639 arbitrary-length theorem above permits different factors but uses one common
640 finite packet type $V$.  A fully dependent arbitrary-length chain of changing
641 modules and packet types remains outside the finite algebraic contract.
642 \end{boundary}
643 
644 \begin{remark}[Checked specialization]
645 When every $B_r$ is one repeated endomorphism $T$, the recursive
646 specialization to packet powers is inherited from Chapter I.
647 \end{remark}
648 \statusleanprior{Komorebi.PacketNaturalityCompletion.Packets.transferBlock_pow_eq_packetPathSum}
649 
650 For a loop represented on one common finite scalar packet coordinate type,
651 the proposition resolves its successive transport matrices into packet
652 walks.  If $R$ is a ring, as in the reversible connection API, then
653 $(H-I)_{ji}=H_{ji}-\delta_{ji}$.  In particular, off-diagonal entries are
654 unchanged.  Thus a nonzero off-diagonal holonomy obstruction in this model
655 with a common index type requires a transport word along the closed chart
656 loop whose packet path runs from its input packet to its output packet.  This
657 conclusion requires declared block supports for the connection matrices.
658 An arbitrary connection need not respect the transfer graph from
659 \cref{sec:edge-operators}.
660 
661 \section{A minimal exact example}
662 \label{sec:example}
663 
664 \begin{example}[A scalar triangle]
665 Let $B=\{0,1,2\}$ and $C_0=C_1=C_2=\bbk$ for a field $\bbk$.  Choose
666 $u,v,w\in\bbk^\times$ and set
667 \[
668 \Gamma_{1\leftarrow0}(x)=ux,\qquad
669 \Gamma_{2\leftarrow1}(x)=vx,\qquad
670 \Gamma_{2\leftarrow0}(x)=wx,
671 \]
672 with reverse transports given by inverse scalars.  Then
673 \[
674 \Delta_{2,1,0}(x)=(vu-w)x,
675 \]
676 and the triangle holonomy based at $0$ is
677 \[
678 H_{2,1,0}(x)=w^{-1}vux.
679 \]
680 Therefore
681 \[
682 H_{2,1,0}-\id
683 =w^{-1}\Delta_{2,1,0}.
684 \]
685 The connection is flat on this triangle exactly when $vu=w$.  If the three
686 coordinate systems are literally the same and canonical transport is used,
687 then $u=v=w=1$ and the obstruction vanishes.  Choosing arbitrary nonzero
688 $u,v,w$ is a connection choice, not a consequence of changing exact packet
689 coordinates.
690 \end{example}
691 
692 \begin{example}[A transfer walk with two steps]
693 Let a packet graph have edges $e:0\to1$ and $f:1\to2$, with no other edges.
694 Then
695 \[
696 T=L_e+L_f,\qquad
697 (T^2)_{20}=c(f)c(e).
698 \]
699 The products $L_eL_e$, $L_eL_f$, and $L_fL_f$ vanish by typed mismatch.
700 Only $L_fL_e$, corresponding to the walk $0\to1\to2$, contributes to the
701 $(2,0)$ entry.  This example also fixes the noncommutative coefficient order.
702 \end{example}
703 
704 \section{Canonical coordinates for arbitrary maps}
705 \label{sec:arbitrary-maps}
706 
707 The analysis and synthesis identities are identities of functions, not only
708 of linear maps.  Consequently exact coordinate change does not become
709 curved merely because the represented operation is nonlinear.
710 
711 \begin{proposition}[Exact naturality for arbitrary functions]
712 \label{prop:set-naturality}
713 Let $\cA^X_a:X\xrightarrow{\sim}X_a$ and
714 $\cA^X_b:X\xrightarrow{\sim}X_b$ be exact coordinate equivalences for $X$,
715 with inverses $\cS^X_a$ and $\cS^X_b$.  Likewise, let
716 $\cA^Y_r:Y\xrightarrow{\sim}Y_r$ and
717 $\cA^Y_s:Y\xrightarrow{\sim}Y_s$ be exact coordinate equivalences for $Y$,
718 with inverses $\cS^Y_r$ and $\cS^Y_s$.  Let $F:X\to Y$ be any function, with
719 no linearity or differentiability hypothesis.  Set
720 \[
721 J^X_{b\leftarrow a}=\cA^X_b\circ\cS^X_a,
722 \qquad
723 J^Y_{s\leftarrow r}=\cA^Y_s\circ\cS^Y_r,
724 \]
725 and define
726 \[
727 \widehat F_{r\leftarrow a}
728 =
729 \cA^Y_r\circ F\circ\cS^X_a.
730 \]
731 Then
732 \[
733 J^Y_{s\leftarrow r}\circ\widehat F_{r\leftarrow a}
734 =
735 \widehat F_{s\leftarrow b}\circ J^X_{b\leftarrow a}.
736 \]
737 If $\cA^Z_t:Z\xrightarrow{\sim}Z_t$ is another exact coordinate equivalence
738 and $G:Y\to Z$ is any function, then exact coordinate representation also
739 preserves composition:
740 \[
741 \widehat{G\circ F}_{t\leftarrow a}
742 =
743 \widehat G_{t\leftarrow r}\circ\widehat F_{r\leftarrow a}.
744 \]
745 \end{proposition}
746 \statusleanthree{Komorebi.PaperIII.Transport.exactCoordinateMap; Komorebi.PaperIII.Transport.exactCoordinateMap_comp; Komorebi.PaperIII.Transport.exactCoordinateMap_naturality}
747 
748 \begin{proof}
749 Both sides of the naturality equation reduce to
750 $\cA^Y_s\circ F\circ\cS^X_a$ using
751 $\cS\circ\cA=\id$ in $X$ and $Y$.  For composition, the middle
752 $\cS^Y\circ\cA^Y$ cancels in the same way.
753 \end{proof}
754 
755 \begin{boundary}[Where nonlinear defects can enter]
756 A nonlinear \emph{coordinate} defect cannot be blamed on the exact canonical
757 $J$ of \cref{def:canonical-J}. By \cref{prop:set-naturality}, that defect is
758 identically zero.  Nonzero defects require extra structure such as a
759 noncanonical connection, truncation, approximation, restricted domains, or
760 failure of an operation to respect a declared packet model.
761 \end{boundary}
762 
763 \clearpage\section{Nonlinear operation trees: locality and the formalization frontier}
764 \label{sec:operation-trees}
765 
766 \subsection{The compiled foundation of unary and binary trees}
767 
768 \begin{definition}[Finite grammar for operation trees]
769 \label{def:compiled-operation-tree}
770 For types of input labels $I$, constants $K$, unary symbols $U$, and binary
771 symbols $B$, the finite formal grammar has four constructors:
772 \[
773 \begin{aligned}
774 t ::={}&\operatorname{input}(i)
775 \mid\operatorname{constant}(k)
776 \mid\operatorname{unary}(u,t)\\
777 &\mid\operatorname{binary}(b,t_1,t_2).
778 \end{aligned}
779 \]
780 Given an arbitrary value type $Y$, evaluation takes completely explicit maps
781 \[
782 I\to Y,\qquad K\to Y,\qquad U\to Y\to Y,\qquad
783 B\to Y\to Y\to Y.
784 \]
785 No algebraic, continuity, or differentiability law is imposed on these
786 semantics.
787 \end{definition}
788 \statusleanthree{Komorebi.PaperIII.NonlinearObstructions.OperationTree; Komorebi.PaperIII.NonlinearObstructions.OperationTree.eval}
789 
790 When $I$ has decidable equality, let $\operatorname{inputs}(t)$ be the finite
791 set of input labels actually occurring in $t$.
792 
793 \begin{theorem}[Input locality for operation trees]
794 \label{thm:tree-locality}
795 Let $\eta_1,\eta_2:I\to Y$ be two input environments.  If
796 \[
797 \eta_1(i)=\eta_2(i)
798 \qquad\text{for every }i\in\operatorname{inputs}(t),
799 \]
800 then the two evaluations of $t$ are equal under the same constant, unary, and
801 binary semantics.  In particular, if
802 $\operatorname{inputs}(t)=\varnothing$, evaluation is independent of the
803 input environment.
804 \end{theorem}
805 \statusleanthree{Komorebi.PaperIII.NonlinearObstructions.OperationTree.eval_congr_on_inputs; Komorebi.PaperIII.NonlinearObstructions.OperationTree.eval_eq_of_inputs_eq_empty}
806 
807 \begin{proof}
808 Structural induction on $t$.  The input case is the agreement hypothesis.
809 The constant case is reflexive. The unary case applies the induction
810 hypothesis to its child. The binary case applies it independently to the
811 left and right subtrees, whose input sets form a union.
812 \end{proof}
813 
814 \begin{boundary}[Exact force of locality]
815 The theorem says evaluation reads only syntactically named inputs.  It does
816 not prove that the operations are linear or nonlinear in any analytic sense,
817 that the tree is stable, that two different trees are equivalent, or that a
818 solution to a tree equation exists.
819 \end{boundary}
820 
821 \subsection{Typed colored extension beyond the finite contract}
822 
823 \begin{definition}[Finitary colored operation signature]
824 \label{def:signature}
825 A finitary colored signature consists of:
826 \begin{itemize}
827 \item a finite type $V$ of colors;
828 \item a type $\Sigma$ of operation symbols;
829 \item an arity $r(\sigma)\in\N$ for every $\sigma\in\Sigma$;
830 \item input colors
831 $\operatorname{in}_\sigma:\operatorname{Fin}(r(\sigma))\to V$;
832 \item an output color $\operatorname{out}(\sigma)\in V$.
833 \end{itemize}
834 A realization assigns a space $X_v$ to each color and a map
835 \[
836 \Phi_\sigma:
837 \prod_{q\in\operatorname{Fin}(r(\sigma))}X_{\operatorname{in}_\sigma(q)}
838 \longrightarrow X_{\operatorname{out}(\sigma)}.
839 \]
840 \end{definition}
841 \statusroadmap{The intended Lean target is a dependent inductive typed tree. No such declaration is part of the finite algebraic completion contract.}
842 
843 \begin{definition}[Typed operation tree and evaluation]
844 \label{def:operation-tree}
845 A typed operation tree is recursively either a leaf of declared color or a
846 node labeled by $\sigma$, with one correctly colored child for each input
847 slot of $\sigma$.  Evaluation is recursive:
848 \[
849 \ev(\operatorname{node}(\sigma;t_1,\ldots,t_{r(\sigma)}))
850 =
851 \Phi_\sigma(\ev(t_1),\ldots,\ev(t_{r(\sigma)})).
852 \]
853 \end{definition}
854 \statusroadmap{Candidate API: \leanname{Komorebi.PaperIII.NonlinearObstructions.ColoredOperationTree} and \leanname{ColoredOperationTree.eval}.  This is stronger than the compiled uncolored unary--binary grammar.}
855 
856 \subsection{Packet labelings and the multilinear first target}
857 
858 Suppose every $X_v$ has a finite complete packet family
859 $(P^v_i)_{i\in I_v}$.  A packet labeling assigns an admissible packet index
860 to each edge or node of a typed tree.  For multilinear $\Phi_\sigma$, inserting
861 \[
862 \id_{X_v}=\sum_{i\in I_v}P^v_i
863 \]
864 at every input and output yields a finite sum over trees with packet labels.
865 This is the branching analogue of inserting intermediate projectors in
866 \cref{prop:heterogeneous-path}.
867 
868 \begin{roadmap}[Finite multilinear tree expansion]
869 \label{roadmap:multilinear-tree}
870 The first milestone for the nonlinear module is an exact theorem saying that the
871 evaluation of a finite tree of multilinear nodes equals the finite sum of its
872 packet-resolved labeled evaluations.  Required proof obligations include:
873 \begin{enumerate}[label=(\alph*)]
874 \item a dependent well-typed tree syntax;
875 \item finite packet-label types at every color;
876 \item an explicit convention for nullary and unary nodes;
877 \item multilinearity in every input slot;
878 \item preservation of the order of input slots without assuming commutativity of
879 operations.
880 \end{enumerate}
881 \end{roadmap}
882 \statusroadmap{Candidate target: \leanname{Komorebi.PaperIII.NonlinearObstructions.ColoredOperationTree.eval_eq_sum_packetLabellings}.}
883 
884 \subsection{Connection defects at nonlinear nodes}
885 
886 For coordinate models of the source and target colors, an additive target
887 coordinate space, and a chosen noncanonical connection, a pointwise node
888 defect can be defined by
889 \[
890 \mathfrak D^\Gamma_{b,a}(\Phi)
891 =
892 \Gamma^Y_{b\leftarrow a}\circ\widehat\Phi_a
893 -
894 \widehat\Phi_b\circ
895 \left(\prod_q\Gamma^{X_q}_{b\leftarrow a}\right).
896 \]
897 This expression compares two \emph{chosen} routes.  With canonical exact
898 transport in every slot it vanishes by \cref{prop:set-naturality}.
899 
900 \begin{roadmap}[Operation-tree defect propagation]
901 \label{roadmap:tree-defect}
902 For multilinear nodes, one expects an exact finite expansion obtained by
903 replacing one or more nodes by their defects and transporting the remaining
904 branches.  For smooth nonlinear nodes, the corresponding chain rule is
905 indexed by rooted partitions and Fa\`a di Bruno trees.  A formal theorem will
906 require a fixed differentiability category, base points, derivative
907 conventions, symmetry factors, and remainder policy.
908 \end{roadmap}
909 \statusroadmap{Tree-level defect identities, higher chain rules, and nonlinear norm bounds are outside the finite Lean contract. Ordinary mathematical results in these directions appear in Part~II under their stated hypotheses.}
910 
911 \begin{boundary}[Analytic and geometric exclusions]
912 The finite formal contract does not include convergence of an infinite tree series, existence
913 of derivatives, a Banach-space Fa\`a di Bruno theorem, a Baker--Campbell--Hausdorff
914 expansion, a continuum limit, or an identification of algebraic holonomy with
915 curvature of a smooth bundle. Part~II supplies ordinary proofs for its explicit nonlinear and analytic statements. The theory does not derive a connection from
916 data, optimization, physics, or probability.
917 \end{boundary}
918 
919 \section{Finite algebraic formalization ledger}
920 \label{sec:ledger}
921 
922 \small
923 \begin{longtable}{L{0.17\textwidth}L{0.18\textwidth}L{0.25\textwidth}L{0.22\textwidth}}
924 \toprule
925 Topic & Status & Declaration or roadmap target & Exact boundary\\
926 \midrule
927 \endfirsthead
928 \toprule
929 Topic & Status & Declaration or roadmap target & Exact boundary\\
930 \midrule
931 \endhead
932 Packet matrix and edge operator
933 & Lean-backed III
934 & \leanname{PacketGraph.packetMatrix}; \leanname{EdgeSystem.edgeOp}
935 & Finite scalar matrices over a semiring, with one scalar coordinate per packet.\\
936 \addlinespace
937 Edge support and pair dichotomy
938 & Lean-backed III
939 & \leanname{edgeOp_eq_zero_off_support}; \leanname{edgeOp_mul_edgeOp_eq_zero}; \leanname{edgeOp_mul_edgeOp_of_composable}
940 & Broken interfaces vanish. Matched pairs collapse to the endpoint block with coefficient in operator order.\\
941 \addlinespace
942 Typed word evaluation
943 & Lean-backed III
944 & \leanname{Composable}; \leanname{wordOp}; \leanname{wordOp_append}; \leanname{wordOp_eq_zero_of_not_composable}
945 & List order is execution order. Concatenation reverses operator-product order. Nonwalks vanish.\\
946 \addlinespace
947 Finite word and walk expansions
948 & Lean-backed III
949 & \leanname{explicitWordExpansion}; \leanname{walkExpansion}; \leanname{wordExpansion_eq_explicitWordExpansion}; \leanname{transferOp_pow_eq_walkExpansion}
950 & Actual finite tuple sum and zero-filtered composable-walk sum over finite graph and packet types.\\
951 \addlinespace
952 Endpoint coefficient walk sum
953 & Lean-backed III
954 & \leanname{reverseCoefficient}; \leanname{Connects}; \leanname{transferOp_pow_apply_eq_sum_walks}
955 & Exact scalar endpoint entry, including the empty-walk case and noncommutative coefficient order.\\
956 \addlinespace
957 Fixed reachability and orbit support
958 & Lean-backed III, with an inherited hull bridge
959 & \leanname{transferOp_pow_apply_eq_zero_of_no_walk}; \leanname{transferOp_pow_mulVec_apply_eq_zero_of_unreachable_support}
960 & Finite powers and supported seeds. The orbit-hull span conclusion uses the frozen Chapter I contract.\\
961 \addlinespace
962 Exact frame transport
963 & Lean-backed III
964 & \leanname{exactTransport_cocycle}; \leanname{exactPathTransport_eq_endpoint}; \leanname{exactPathTransport_loop}
965 & One frame family on a single module. Arbitrary finite paths telescope and closed paths are trivial.\\
966 \addlinespace
967 Exact coordinate cocycle
968 & Inherited Lean-backed II
969 & \leanname{NestedRefinement.refineCoordinates_comp}; \leanname{NestedRefinement.coordinateRefinementEquiv_trans}
970 & Complete finite projector coordinates, not reduction.\\
971 \addlinespace
972 Typed coordinate naturality
973 & Inherited Lean-backed II
974 & \leanname{NestedRefinement.coordinateOperator_comp}; \leanname{NestedRefinement.coordinateOperator_naturality}
975 & Linear maps over semiring modules.\\
976 \addlinespace
977 Minimal connection API
978 & Lean-backed III
979 & \leanname{Transport.Connection}; \leanname{cocycleDefect}; \leanname{triangleHolonomy}; \leanname{triangleHolonomy_eq_refl_of_flat}
980 & Only self-normalization is assumed. Reverse inversion and the cocycle are not structure fields.\\
981 \addlinespace
982 Twisted three-point loop
983 & Lean-backed III
984 & \leanname{twistedThreePointConnection}; \leanname{twisted_triangleHolonomy_ne_refl}
985 & Concrete rational connection. The selected loop sends \(1\) to \(2\).\\
986 \addlinespace
987 Reversible additive defect
988 & Lean-backed III
989 & \leanname{ReversibleConnection}; \leanname{triangleHolonomy_sub_id}; \leanname{cocycleDefect_eq_zero_iff_triangleHolonomy_eq_refl}
990 & Heterogeneous module fibers, reverse-edge inversion, and an additive defect over a commutative ring.\\
991 \addlinespace
992 Reversible finite paths
993 & Lean-backed III
994 & \leanname{pathTransport_eq_direct_of_flat}; \leanname{indexedPathTransport_eq_direct_of_flat}; \leanname{indexedLoopTransport_eq_refl_of_flat}
995 & Finite pair-connection paths collapse to endpoints under algebraic flatness.\\
996 \addlinespace
997 Gauge covariance
998 & Lean-backed III
999 & \leanname{gauge_cocycleDefect}; \leanname{gauge_triangleHolonomy}; \leanname{gauge_flat_iff}
1000 & Fiberwise algebraic conjugation, without smooth gauge theory.\\
1001 \addlinespace
1002 Flat versus canonical transport
1003 & Lean-backed III
1004 & \leanname{flatGauge}; \leanname{flat_isGaugeOfCanonical}
1005 & A chosen base chart and ambient frames exhibit every flat pair connection as a gauge transform of canonical transport.\\
1006 \addlinespace
1007 Operation-tree locality
1008 & Lean-backed III
1009 & \leanname{OperationTree}; \leanname{OperationTree.eval}; \leanname{OperationTree.eval_congr_on_inputs}
1010 & Arbitrary unary and binary semantics. Only dependence on named inputs is proved.\\
1011 \addlinespace
1012 Generic obstruction packet
1013 & Lean-backed III
1014 & \leanname{ObstructionPacket.not_isSolution}; \leanname{not_isSolution_iff_nonempty_obstructionPacket}
1015 & Exact candidate-specific logical certificate, without global classification.\\
1016 \addlinespace
1017 Holonomy block obstruction
1018 & Lean-backed III
1019 & \leanname{obstruction_sum_blocks}; \leanname{obstructionBlocks_zero_iff}; \leanname{obstructionDetection_equivalences}
1020 & Finite complete idempotent packet family on the base fiber. Orthogonality is not required by the compiled reconstruction.\\
1021 \addlinespace
1022 Packet witness and block gauge
1023 & Lean-backed III
1024 & \leanname{exists_packetWitness_of_obstructionBlock_ne_zero}; \leanname{obstructionBlock_gauge_of_commutes}; \leanname{obstructionBlock_gauge_eq_zero_iff}
1025 & Witness extraction is classical. Blockwise covariance requires the gauge to commute with every packet projector.\\
1026 \addlinespace
1027 Heterogeneous matrix paths
1028 & Lean-backed III
1029 & \leanname{heterogeneousPacketPathExpansion}; \leanname{heterogeneousProduct_apply_eq_zero_of_no_supportedPath}
1030 & Arbitrarily many different matrices over one common finite packet type. Fully typed changing-index chains compile only at lengths two and three.\\
1031 \addlinespace
1032 Arbitrary-function coordinates
1033 & Lean-backed III
1034 & \leanname{exactCoordinateMap_comp}; \leanname{exactCoordinateMap_naturality}
1035 & Exact set-level equivalences and arbitrary functions, without a linearity or differentiability assumption.\\
1036 \addlinespace
1037 Colored and smooth trees
1038 & Roadmap only
1039 & roadmap \leanname{ColoredOperationTree.eval_eq_sum_packetLabellings}
1040 & Dependent colors, multilinear packet expansion, derivatives, and Fa\`a di Bruno identities remain outside the contract.\\
1041 \bottomrule
1042 \end{longtable}
1043 \normalsize
1044 
1045 \subsection{Kernel-backed Chapter III surface}
1046 
1047 The authoritative declaration-level contract is
1048 \path{formalization/lean/LEAN_THEOREM_MAP_v1.0.1.md}.  It groups the compiled
1049 surface as follows.
1050 \begin{itemize}
1051 \item \textbf{EdgeOperators and EdgeExtensions:} scalar packet matrices,
1052 typed edge and word support, finite word/walk expansions, endpoint coefficient
1053 sums, fixed-length reachability, orbit support, and common-index
1054 heterogeneous products with declared supports.
1055 \item \textbf{Transport and ReversibleConnections:} exact frame transport,
1056 the minimal connection, heterogeneous reversible pair transport, additive
1057 defect and triangle holonomy, finite paths, canonical connections, and the
1058 fiberwise gauge action.
1059 \item \textbf{CoordinateNaturality and HolonomyBlocks:} composition and
1060 naturality for arbitrary functions between exact coordinate systems, finite
1061 two-sided block reconstruction, equivalent obstruction criteria,
1062 packet-supported witnesses, and packet-preserving block gauges.
1063 \item \textbf{NonlinearObstructions:} finite unary--binary operation trees,
1064 input locality, and candidate-specific obstruction certificates.
1065 \end{itemize}
1066 The formal companion records the checker-generated declaration
1067 and audit totals.  The parity gate requires every fully qualified Chapter III
1068 target printed beside a statement to occur in the theorem map, rejects stale
1069 or duplicate targets, and checks it against the compiled environment.
1070 \path{KernelAudit.lean} reports dependencies for the mapped and supporting
1071 theorems, and its fail-closed gate scans every compiled
1072 \leanname{Komorebi.PaperIII} declaration.  The four inherited statement
1073 contracts remain identified separately by their inherited declaration names.
1074 
1075 \begin{boundary}[No scope promotion by prose]
1076 The displayed endpoint coefficient formula, reachability results, reversible
1077 connection theorems, additive defect--holonomy identity, gauge covariance,
1078 holonomy-block reconstruction, packet witnesses, common-index heterogeneous
1079 path expansion, and arbitrary-function coordinate naturality are all part of
1080 the finite algebraic kernel-backed surface.  What remains outside is the
1081 dependent fiber-valued edge-system generalization, a fully dependent
1082 arbitrary-length chain whose module and packet type change at every stage,
1083 dependent colored operation trees, packet-labeled multilinear tree
1084 expansions, nonlinear tree-defect and Fa\`a di Bruno identities, and the
1085 analytic and geometric extensions listed above.
1086 \end{boundary}
1087 
1088 \section{The finite contract and the nonlinear transition}
1089 
1090 Typed packet support turns the expansion of a transfer power into a walk
1091 calculus.  Incompatible words vanish because their interfaces do not match.
1092 Canonical packet coordinate transport is the exact equivalence obtained
1093 from analysis and synthesis.  It satisfies the cocycle law, so every finite
1094 canonical loop telescopes to the identity.  Holonomy enters after a separate
1095 connection is supplied.  The compiled minimal API proves that flatness makes
1096 both the relative defect and holonomy trivial, and it exhibits a nontrivial
1097 rational loop.  Under the compiled reversible API, a nonzero additive triangle
1098 defect is equivalent to nonidentity holonomy, transforms covariantly under
1099 gauge, and is detected exactly by a finite family of packet blocks.  Finite
1100 flat paths collapse to their endpoints.  Every flat reversible pair connection
1101 is explicitly related to canonical transport by a gauge change through a
1102 chosen base chart.
1103 
1104 These facts define the boundary of the finite formal contract.  At that
1105 boundary, exact coordinates preserve composition and satisfy naturality for
1106 arbitrary functions in Chapter III, while the typed linear packet coordinate
1107 counterpart remains inherited from Chapter~II.  Nontrivial nonlinear defects
1108 must therefore be attached to additional modeling choices or to
1109 packet compatibility of the particular operation.  Colored operation trees,
1110 multilinear packet labelings, and Fa\`a di Bruno expansions remain
1111 outside this finite Lean contract. Part~II develops the corresponding ordinary mathematics, including packet jets, rooted tree expansions, and explicit nonlinear obstruction theorems.
1112 
1113 
1114 \clearpage

Back to source controls

Back to Realization Calculus