5 A distinct noncanonical connection API
On this page · Visual guide: Three objects, three different questions · Permalink · Source line 1
5.1 The minimal compiled API
On this page · Permalink · Source line 4
The compiled Paper III API assumes only normalization at each chart. All chart transports act on one module \(M\), so chart labels distinguish routes but not Lean types.
Definition 5.1: Noncanonical connection normalized at each chart
A minimal connection is a family
with only
Neither inversion on reversed edges nor the cocycle law is a field of the structure.
Visual guide: Reversibility is a real hypothesis · Permalink · Source line 10 · Claim record · Lean coverage · Code · Worked examples
Formal contract: Paper III v1.0.1. Komorebi.PaperIII.Transport.Connection
At a triple \((a,b,c)\), the compiled cocycle predicate is
Flatness means this equality holds for every triple. The formal multiplicative relative defect and triangle holonomy are
The defect is based at the target \(c\). The holonomy is based at \(a\). Formal contract: Paper III v1.0.1. Komorebi.PaperIII.Transport.Connection.CocycleAt; Komorebi.PaperIII.Transport.Connection.Flat; Komorebi.PaperIII.Transport.Connection.cocycleDefect; Komorebi.PaperIII.Transport.Connection.triangleHolonomy
Theorem 5.2: Checked flatness consequences
For the minimal connection API, flatness implies
for every \(a,b,c\).
Permalink · Source line 48 · Claim record · Lean coverage · Code · Worked examples
Formal contract: Paper III v1.0.1. Komorebi.PaperIII.Transport.Connection.cocycleDefect_eq_refl_of_flat; Komorebi.PaperIII.Transport.Connection.triangleHolonomy_eq_refl_of_flat
Proof
Flatness replaces the two-edge route in \(D^\times\) by the direct route, which cancels its inverse. For \(H\), flatness first collapses \(a\to b\to c\) to \(a\to c\), then collapses \(a\to c\to a\) to the normalized transport \(a\to a\).
Proposition 5.3: The minimal API admits nontrivial holonomy
There is a connection on three points over \(\mathbb Q\) for which transport \(0\to1\) is multiplication by \(2\), every other transport between distinct endpoints is the identity, and
In particular \(H_{2,1,0}\ne{\mathrm{id}}\).
Permalink · Source line 67 · Claim record · Lean coverage · Code · Worked examples
Formal contract: Paper III v1.0.1. Komorebi.PaperIII.Transport.twistedThreePointConnection; Komorebi.PaperIII.Transport.twisted_triangleHolonomy_apply_one; Komorebi.PaperIII.Transport.twisted_triangleHolonomy_ne_refl
Boundary 5.4: Why the minimal defect and loop are distinct
Without reverse-edge inversion, \(\Gamma_{a\leftarrow c}\) need not equal \(\Gamma_{c\leftarrow a}^{-1}\). Therefore the multiplicative relative defect \(D^\times_{c,b,a}\) and triangle holonomy \(H_{c,b,a}\) are different comparisons. The formal module proves that global flatness trivializes both; it does not identify them for an arbitrary connection.
Permalink · Source line 79 · Claim record · Lean coverage · Code · Worked examples
Figure records this separation visually: the exact coordinate route telescopes, whereas the chosen connection route may carry a nonidentity loop.
Coordinate transport and connection choice
Canonical transport compares exact coordinate descriptions of the same object. Its loops telescope. A connection supplies a separate family of comparison maps, so its loops can carry information about that choice. The distinction keeps coordinate identities separate from connection assumptions.
5.2 A stronger reversible pair API
On this page · Permalink · Source line 109
Let \(R\) be a commutative ring, let \(B\) be a type of charts or refinement states, and let each \(C_a\) be an \(R\)-module. The chart type is not assumed finite. The following definition is deliberately not derived from analysis and synthesis.
Definition 5.5: Normalized reversible connection
A normalized reversible connection is a family of linear equivalences
such that
No cocycle equation is included in the structure.
Visual guide: An atlas of the objects · Visual guide: Reversibility is a real hypothesis · Permalink · Source line 116 · Claim record · Lean coverage · Code · Worked examples
Formal contract: Paper III v1.0.1. Komorebi.PaperIII.Transport.ReversibleConnection
This adds heterogeneous fibers and inversion on reversed edges to the homogeneous minimal connection. The connection is still a separate choice of maps, rather than a definition of canonical coordinate transport.
Definition 5.6: Calibration and flatness
When the \(C_a\) are exact packet coordinates of one ambient module, the connection is canonically calibrated if
It is flat if
The canonical connection is flat. A general flat connection is proved in Theorem 6.3 to be related to it by a gauge change.
Permalink · Source line 137 · Claim record · Lean coverage · Code · Worked examples
Formal contract: Paper III v1.0.1. Komorebi.PaperIII.Transport.ReversibleConnection.CocycleAt; Komorebi.PaperIII.Transport.ReversibleConnection.Flat; Komorebi.PaperIII.Transport.ReversibleConnection.canonicalConnection; Komorebi.PaperIII.Transport.ReversibleConnection.canonicalConnection_flat
The words calibrated and flat have only the algebraic meanings displayed above.
Remark 5.7: A connection on a chart graph
One may specify \(\Gamma_e\) only on the oriented edges of a chart graph, together with inverse maps on reversed edges. Path transport and loop holonomy below still make sense. A direct cocycle defect for \((a,b,c)\), however, requires a declared direct transport from \(a\) to \(c\). The pairwise API in Definition 5.5 keeps this comparison total.
5.3 Cocycle defect and triangle holonomy
On this page · Permalink · Source line 168
The commutative ring hypothesis makes subtraction of linear maps available from this point through Section 7.
Definition 5.8: Cocycle defect
For \(a,b,c\in B\), define the additive cocycle defect
Permalink · Source line 173 · Claim record · Lean coverage · Code · Worked examples
Formal contract: Paper III v1.0.1. Komorebi.PaperIII.Transport.ReversibleConnection.cocycleDefect
The manuscript subscript order is target, intermediate, source. The Lean arguments are supplied in traversal order (a,b,c).
Definition 5.9: Triangle holonomy
The triangle holonomy based at \(a\) is
It traverses \(a\to b\to c\to a\).
Visual guide: The identity can hide in the spectrum · Permalink · Source line 189 · Claim record · Lean coverage · Code · Worked examples
Formal contract: Paper III v1.0.1. Komorebi.PaperIII.Transport.ReversibleConnection.triangleHolonomy; Komorebi.PaperIII.Transport.ReversibleConnection.triangleObstruction
Holonomy is attached to the chosen connection \(\Gamma\), never to an unspecified coordinate change.
Theorem 5.10: Identity between defect and holonomy
For every triple \((a,b,c)\),
Consequently,
Visual guide: Measure the mismatch at its base · Visual guide: From loop data to a packet witness · Permalink · Source line 207 · Claim record · Lean coverage · Code · Worked examples
Formal contract: Paper III v1.0.1. Komorebi.PaperIII.Transport.ReversibleConnection.triangleHolonomy_sub_id; Komorebi.PaperIII.Transport.ReversibleConnection.cocycleDefect_eq_zero_iff_triangleHolonomy_eq_refl
Proof
Using reversibility,
Left composition by the equivalence \(\Gamma_{a\leftarrow c}\) is injective, which gives the equivalence of the two vanishing statements.
Corollary 5.11: Canonical transport has zero connection defect
If \(\Gamma_{b\leftarrow a}=J_{b\leftarrow a}\), then
for all triples.
Permalink · Source line 244 · Claim record · Lean coverage · Code · Worked examples
Formal contract: Paper III v1.0.1. Komorebi.PaperIII.Transport.ReversibleConnection.canonicalTransport_zero_connectionDefect; Komorebi.PaperIII.Transport.ReversibleConnection.canonicalTransport_triangleHolonomy_eq_refl
Proof
The defect vanishes by the canonical cocycle in Theorem 4.4; apply Theorem 5.10.
5.4 Paths and endpoint independence
On this page · Permalink · Source line 261
Definition 5.12: Connection transport along a path
For a vertex sequence \(p=(a_0,a_1,\ldots,a_n)\), define
If \(a_n=a_0\), then \(\Gamma_p\) is the holonomy of the loop \(p\).
Permalink · Source line 263 · Claim record · Lean coverage · Code · Worked examples
Formal contract: Paper III v1.0.1. Komorebi.PaperIII.Transport.ReversibleConnection.pathTransport; Komorebi.PaperIII.Transport.ReversibleConnection.VertexPath; Komorebi.PaperIII.Transport.ReversibleConnection.indexedPathTransport
Products follow path order: the first traversed edge acts on the right.
Proposition 5.13: Flat pair transport collapses to endpoints
If \(\Gamma\) is flat, then every path satisfies
In particular, every loop has identity holonomy.
Permalink · Source line 281 · Claim record · Lean coverage · Code · Worked examples
Formal contract: Paper III v1.0.1. 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
Proof
Induct on the path length. Appending \(a_{n+1}\) left-multiplies the inductive expression by \(\Gamma_{a_{n+1}\leftarrow a_n}\), and flatness replaces the two factors by \(\Gamma_{a_{n+1}\leftarrow a_0}\). For a loop, normalization gives \(\Gamma_{a_0\leftarrow a_0}={\mathrm{id}}\).
Remark 5.14
The converse trivial holonomy implies flatness depends on which loops are present in an API defined on a chart graph. In the complete pair API, triviality of every triangle holonomy is equivalent to flatness by Theorem 5.10. No theorem about topological simple connectivity is being invoked.
6 Gauge covariance and comparison with canonical transport
On this page · Permalink · Source line 307
Definition 6.1: Gauge change
A gauge is a family of automorphisms \(G_a\in\operatorname{Aut}_R(C_a)\). It acts on a connection by
Permalink · Source line 310 · Claim record · Lean coverage · Code · Worked examples
Formal contract: Paper III v1.0.1. Komorebi.PaperIII.Transport.ReversibleConnection.Gauge; Komorebi.PaperIII.Transport.ReversibleConnection.gauge
A gauge changes coordinate representatives at each chart. The chart graph stays the same.
Theorem 6.2: Gauge covariance
The defect and triangle holonomy transform as
Thus flatness and triviality of triangle holonomy are gauge invariant.
Visual guide: Gauge changes the picture, not flatness · Visual guide: From loop data to a packet witness · Permalink · Source line 325 · Claim record · Lean coverage · Code · Worked examples
Formal contract: Paper III v1.0.1. 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
Proof
Substitute the definition of \(\Gamma^G\). Adjacent factors \(G_b^{-1}G_b\) and \(G_c^{-1}G_c\) cancel. In the defect, both the composite and direct terms acquire the same outer factors \(G_c\) and \(G_a^{-1}\). In the loop, all inner factors cancel and only conjugation at the base remains.
Theorem 6.3: Flat connections are gauges of the canonical pair transport
Suppose the \(C_a\) are exact packet coordinate modules for one ambient module, so the canonical \(J_{b\leftarrow a}\) is available. If \(\Gamma\) is a flat normalized reversible pair connection, choose \(o\in B\) and set
Then every pair transport satisfies
Visual guide: Flat is not the same as calibrated · Permalink · Source line 346 · Claim record · Lean coverage · Code · Worked examples
Formal contract: Paper III v1.0.1. Komorebi.PaperIII.Transport.ReversibleConnection.flatGauge; Komorebi.PaperIII.Transport.ReversibleConnection.flat_isGaugeOfCanonical
Proof
Reversibility gives \(G_a^{-1}=J_{a\leftarrow o}\Gamma_{o\leftarrow a}\). Therefore
The first reduction uses the canonical cocycle twice; the second uses flatness of \(\Gamma\).
Boundary 6.4: Flat does not mean calibrated
The theorem produces a gauge relating \(\Gamma\) to \(J\). It does not prove \(\Gamma=J\) before that gauge is chosen. Conversely, nontrivial triangle holonomy cannot be removed by a gauge, because conjugation cannot turn a nonidentity automorphism into the identity.
Permalink · Source line 385 · Claim record · Lean coverage · Code · Worked examples
7 Obstruction packets: local certificates and holonomy blocks
On this page · Permalink · Source line 392
7.1 The generic compiled certificate
On this page · Permalink · Source line 395
Let \(\mathsf{Candidate}\), \(\mathsf{Packet}\), and \(\mathsf{Residual}\) be arbitrary types, with a distinguished \(0\in\mathsf{Residual}\), and let
be a residual function.
Definition 7.1: Solution and obstruction packet for a candidate
A candidate \(x\) is a solution when
An obstruction packet for \(x\) is a pair consisting of a named packet \(p\) and a certificate \(r(x,p)\ne0\).
Permalink · Source line 406 · Claim record · Lean coverage · Code · Worked examples
Formal contract: Paper III v1.0.1. Komorebi.PaperIII.NonlinearObstructions.IsSolution; Komorebi.PaperIII.NonlinearObstructions.ObstructionPacket
Theorem 7.2: Exact logical force of a local obstruction
Every obstruction packet for \(x\) proves that \(x\) is not a solution, and
The reverse implication from failure to a packet witness is classical and does not require the packet type to be finite.
Visual guide: An obstruction rejects one candidate · Permalink · Source line 419 · Claim record · Lean coverage · Code · Worked examples
Formal contract: Paper III v1.0.1. Komorebi.PaperIII.NonlinearObstructions.ObstructionPacket.not_isSolution; Komorebi.PaperIII.NonlinearObstructions.obstructionPacket_of_not_isSolution; Komorebi.PaperIII.NonlinearObstructions.not_isSolution_iff_nonempty_obstructionPacket
Proof
A purported solution would make the residual vanish at the certified packet, contradicting its nonzero field. Conversely, if no packet carries a nonzero residual, then every residual is zero and the candidate satisfies the definition of solution.
What one obstruction certifies
The certificate answers one question: does this specified candidate satisfy every declared packet condition? One nonzero residual settles that question for this candidate. A statement that no candidate can solve the problem would require an obstruction for every candidate.
Boundary 7.3: Candidate-specific means candidate-specific
The theorem rules out the named \(x\). It neither constructs a solution nor shows that every candidate is obstructed. It provides no minimality, stability, computability, or classification theorem for the packet witness.
Permalink · Source line 446 · Claim record · Lean coverage · Code · Worked examples
7.2 Specialization to holonomy blocks
On this page · Permalink · Source line 452
For a reversible connection, specialize the generic residual at a fixed triangle by taking a packet label to be a pair \((\mu,\nu)\) and the residual to be the corresponding block of \(H-{\mathrm{id}}\). A nonzero block, together with its label and a proof of nonvanishing, gives an obstruction packet certificate in the sense of Definition 7.1. The reconstruction theorem below supplies the further step: vanishing of all these local residuals is equivalent to the cocycle equation at that triangle.
Fix a triangle \((a,b,c)\) and resolve the base fiber \(C_a\) by a finite complete family of idempotents \((\Pi^a_\mu)_{\mu\in I_a}\). Orthogonality may also hold, as it does for the exact range coordinate projectors below, but the compiled reconstruction theorem does not require it. In exact range coordinates, \(\Pi^a_\mu\) is simply the projector that retains component \(\mu\) and zeros the other components.
Definition 7.4: Holonomy obstruction and packet residuals
Define
The map \({\operatorname{Ob}}^{\mu\nu}_{c,b,a}\) is the obstruction block, or packet residual, from input packet \(\nu\) to output packet \(\mu\). If it is nonzero, then \((\mu,\nu)\) and that nonvanishing proof form an obstruction packet certificate. Diagonal blocks detect holonomy within one packet. Off-diagonal blocks detect packet mixing induced by holonomy.
Visual guide: An atlas of the objects · Visual guide: The identity can hide in the spectrum · Permalink · Source line 469 · Claim record · Lean coverage · Code · Worked examples
Formal contract: Paper III v1.0.1. Komorebi.PaperIII.HolonomyBlocks.PacketResolution; Komorebi.PaperIII.HolonomyBlocks.PacketResolution.block
The certificate records a specified holonomy defect, the label of an input and output packet, and a proof that the corresponding block is nonzero.
Theorem 7.5: Exact reconstruction and detection by obstruction blocks
The total obstruction has the exact finite resolution
Moreover, the following are equivalent:
\(\Delta_{c,b,a}=0\);
\(H_{c,b,a}={\mathrm{id}}\);
\({\operatorname{Ob}}_{c,b,a}=0\);
\({\operatorname{Ob}}^{\mu\nu}_{c,b,a}=0\) for every \(\mu,\nu\).
Visual guide: Resolve the entire obstruction · Visual guide: Why diagonal checks are insufficient · Permalink · Source line 490 · Claim record · Lean coverage · Code · Worked examples
Formal contract: Paper III v1.0.1. Komorebi.PaperIII.HolonomyBlocks.obstruction_sum_blocks; Komorebi.PaperIII.HolonomyBlocks.obstructionBlocks_zero_iff; Komorebi.PaperIII.HolonomyBlocks.obstructionDetection_equivalences
Proof
Insert completeness on both sides:
Thus (iv) implies (iii), and (iii) implies (iv) by composition with the projectors. Conditions (ii) and (iii) are equivalent by the definition of \({\operatorname{Ob}}\) and additive cancellation. Conditions (i) and (ii) are equivalent by Theorem 5.10.
Why both packet indices matter
For the declared finite complete resolution, reconstruction uses both packet indices. Inspecting only diagonal blocks can miss transport from one packet to another. The full family records that mixing and reconstructs the total obstruction exactly.
Figure depicts the finite block resolution on both sides of the obstruction and the off-diagonal blocks that witness packet mixing.
Corollary 7.6: Witness supported in one packet
If \({\operatorname{Ob}}^{\mu\nu}_{c,b,a}\ne0\), then there is a vector \(x\) supported in packet \(\nu\) such that
Such an \(x\) is an exact finite witness of nonflatness.
Visual guide: Resolve the entire obstruction · Visual guide: From loop data to a packet witness · Permalink · Source line 549 · Claim record · Lean coverage · Code · Worked examples
Formal contract: Paper III v1.0.1. Komorebi.PaperIII.HolonomyBlocks.exists_packetWitness_of_obstructionBlock_ne_zero
Proof
Classically choose \(y\) on which the nonzero linear map \(\Pi^a_\mu{\operatorname{Ob}}\Pi^a_\nu\) is nonzero and set \(x=\Pi^a_\nu y\). Idempotence gives \(\Pi^a_\nu x=x\), and the required output is the chosen nonzero value.
7.3 Gauge behavior of packet blocks
On this page · Permalink · Source line 567
Vanishing or nonvanishing of the total triangle obstruction is gauge invariant by Theorem 6.2, but a fixed packet pattern need not be. A general \(G_a\) can mix the projectors \(\Pi^a_\mu\).
Proposition 7.7: Gauge covariance when packet projectors are preserved
If \(G_a\Pi^a_\mu=\Pi^a_\mu G_a\) for every \(\mu\), then
Consequently the zero/nonzero status of each obstruction block is preserved by gauges that preserve the packet projectors.
Visual guide: A gauge can move every packet label · Permalink · Source line 573 · Claim record · Lean coverage · Code · Worked examples
Formal contract: Paper III v1.0.1. Komorebi.PaperIII.HolonomyBlocks.obstructionBlock_gauge_of_commutes; Komorebi.PaperIII.HolonomyBlocks.obstructionBlock_gauge_eq_zero_iff
Proof
Use \({\operatorname{Ob}}^G=G_a{\operatorname{Ob}} G_a^{-1}\) and commute \(G_a\) and \(G_a^{-1}\) through the two packet projectors. Composition by an equivalence is injective in both directions.
Boundary 7.8: Packet patterns are not absolute
Without the commutation hypothesis in Proposition 7.7, only the vanishing of the total obstruction is gauge invariant. The location of individual nonzero blocks may change under a gauge that mixes packets.
Permalink · Source line 592 · Claim record · Lean coverage · Code · Worked examples
8 Products supported in packets and holonomy walks
On this page · Permalink · Source line 598
The passage from words to walks also applies to products of different matrices. Let \(V\) be one finite packet type, let \(R\) be a semiring, and let \(B_1,\ldots,B_m\in R^{V\times V}\) be a finite sequence of possibly different packet matrices. Rows are targets and columns are sources as before.
Proposition 8.1: Packet path expansion for different matrices
For \(i,j\in V\) and \(m\geq1\), set \(i_0=i\) and \(i_m=j\). Then
When \(m=1\), the sum is over the unique empty tuple and its summand is \(B_1[j,i]\). For \(m=0\), the product is the identity and the entry is the Kronecker delta \(\delta_{ji}\). If every \(B_r[q,p]\) vanishes outside a declared relation \(\mathcal R_r(p,q)\), then the endpoint entry is zero whenever there is no packet path compatible with the successive relations.
Visual guide: Paths through changing packet lists · Permalink · Source line 607 · Claim record · Lean coverage · Code · Worked examples
Formal contract: Paper III v1.0.1. 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
Proof
Expand each matrix product entry and distribute the finite sums. Induction on the factor list yields the displayed path sum, with the empty list evaluated as the identity matrix. If no supported intermediate packet exists, every summand contains an entry that is zero by its declared support relation.
Boundary 8.2: Changing packet types along a chain
The compiled theorems heterogeneousPacketPathExpansion_two and heterogeneousPacketPathExpansion_three allow different packet types at the successive stages of two- and three-factor products. The arbitrary-length theorem above permits different factors but uses one common finite packet type \(V\). A fully dependent arbitrary-length chain of changing modules and packet types remains outside the version 1.0.1 contract.
Permalink · Source line 634 · Claim record · Lean coverage · Code · Worked examples
Remark 8.3: Checked specialization
When every \(B_r\) is one repeated endomorphism \(T\), the recursive specialization to packet powers is inherited from Paper I.
Inherited formal contract: Papers I–II. Komorebi.PacketNaturalityCompletion.Packets.transferBlock_pow_eq_packetPathSum
For a loop represented on one common finite scalar packet coordinate type, the proposition resolves its successive transport matrices into packet walks. If \(R\) is a ring, as in the reversible connection API, then \((H-I)_{ji}=H_{ji}-\delta_{ji}\). In particular, off-diagonal entries are unchanged. Thus a nonzero off-diagonal holonomy obstruction in this model with a common index type requires a transport word along the closed chart loop whose packet path runs from its input packet to its output packet. This conclusion requires declared block supports for the connection matrices. An arbitrary connection need not respect the transfer graph from Section 2.
9 A minimal exact example
On this page · Visual guide: Coefficients need not commute · Visual guide: Measure the mismatch at its base · Permalink · Source line 661
Example 9.1: A scalar triangle
Let \(B=\{0,1,2\}\) and \(C_0=C_1=C_2={\Bbbk}\) for a field \({\Bbbk}\). Choose \(u,v,w\in{\Bbbk}^\times\) and set
with reverse transports given by inverse scalars. Then
and the triangle holonomy based at \(0\) is
Therefore
The connection is flat on this triangle exactly when \(vu=w\). If the three coordinate systems are literally the same and canonical transport is used, then \(u=v=w=1\) and the obstruction vanishes. Choosing arbitrary nonzero \(u,v,w\) is a connection choice, not a consequence of changing exact packet coordinates.
Example 9.2: A transfer walk with two steps
Let a packet graph have edges \(e:0\to1\) and \(f:1\to2\), with no other edges. Then
The products \(L_eL_e\), \(L_eL_f\), and \(L_fL_f\) vanish by typed mismatch. Only \(L_fL_e\), corresponding to the walk \(0\to1\to2\), contributes to the \((2,0)\) entry. This example also fixes the noncommutative coefficient order.
10 Canonical coordinates for arbitrary maps
On this page · Permalink · Source line 704
The analysis and synthesis identities are identities of functions, not only of linear maps. Consequently exact coordinate change does not become curved merely because the represented operation is nonlinear.
Proposition 10.1: Exact naturality for arbitrary functions
Let \({\mathcal A}^X_a:X\xrightarrow{\sim}X_a\) and \({\mathcal A}^X_b:X\xrightarrow{\sim}X_b\) be exact coordinate equivalences for \(X\), with inverses \({\mathcal S}^X_a\) and \({\mathcal S}^X_b\). Likewise, let \({\mathcal A}^Y_r:Y\xrightarrow{\sim}Y_r\) and \({\mathcal A}^Y_s:Y\xrightarrow{\sim}Y_s\) be exact coordinate equivalences for \(Y\), with inverses \({\mathcal S}^Y_r\) and \({\mathcal S}^Y_s\). Let \(F:X\to Y\) be any function, with no linearity or differentiability hypothesis. Set
and define
Then
If \({\mathcal A}^Z_t:Z\xrightarrow{\sim}Z_t\) is another exact coordinate equivalence and \(G:Y\to Z\) is any function, then exact coordinate representation also preserves composition:
Visual guide: Nonlinear charts still cancel exactly · Visual guide: Where a nonlinear defect can enter · Permalink · Source line 711 · Claim record · Lean coverage · Code · Worked examples
Formal contract: Paper III v1.0.1. Komorebi.PaperIII.Transport.exactCoordinateMap; Komorebi.PaperIII.Transport.exactCoordinateMap_comp; Komorebi.PaperIII.Transport.exactCoordinateMap_naturality
Proof
Both sides of the naturality equation reduce to \({\mathcal A}^Y_s\circ F\circ{\mathcal S}^X_a\) using \({\mathcal S}\circ{\mathcal A}={\mathrm{id}}\) in \(X\) and \(Y\). For composition, the middle \({\mathcal S}^Y\circ{\mathcal A}^Y\) cancels in the same way.
Boundary 10.2: Where nonlinear defects can enter
A nonlinear coordinate defect cannot be blamed on the exact canonical \(J\) of Definition 4.3; Proposition 10.1 makes that defect identically zero. Nonzero defects require extra structure such as a noncanonical connection, truncation, approximation, restricted domains, or failure of an operation to respect a declared packet model.
Permalink · Source line 755 · Claim record · Lean coverage · Code · Worked examples
11 Nonlinear operation trees: locality and the formalization frontier
On this page · Permalink · Source line 763
11.1 The compiled foundation of unary and binary trees
On this page · Permalink · Source line 766
Definition 11.1: Finite grammar for operation trees
For types of input labels \(I\), constants \(K\), unary symbols \(U\), and binary symbols \(B\), the released formal grammar has four constructors:
Given an arbitrary value type \(Y\), evaluation takes completely explicit maps
No algebraic, continuity, or differentiability law is imposed on these semantics.
Visual guide: A tree reads its named leaves · Permalink · Source line 768 · Claim record · Lean coverage · Code · Worked examples
Formal contract: Paper III v1.0.1. Komorebi.PaperIII.NonlinearObstructions.OperationTree; Komorebi.PaperIII.NonlinearObstructions.OperationTree.eval
When \(I\) has decidable equality, let \(\operatorname{inputs}(t)\) be the finite set of input labels actually occurring in \(t\).
Theorem 11.2: Input locality for operation trees
Let \(\eta_1,\eta_2:I\to Y\) be two input environments. If
then the two evaluations of \(t\) are equal under the same constant, unary, and binary semantics. In particular, if \(\operatorname{inputs}(t)=\varnothing\), evaluation is independent of the input environment.
Visual guide: A tree reads its named leaves · Permalink · Source line 793 · Claim record · Lean coverage · Code · Worked examples
Formal contract: Paper III v1.0.1. Komorebi.PaperIII.NonlinearObstructions.OperationTree.eval_congr_on_inputs; Komorebi.PaperIII.NonlinearObstructions.OperationTree.eval_eq_of_inputs_eq_empty
Proof
Structural induction on \(t\). The input case is the agreement hypothesis; the constant case is reflexive; the unary case applies the induction hypothesis to its child; and the binary case applies it independently to the left and right subtrees, whose input sets form a union.
Boundary 11.3: Exact force of locality
The theorem says evaluation reads only syntactically named inputs. It does not prove that the operations are linear or nonlinear in any analytic sense, that the tree is stable, that two different trees are equivalent, or that a solution to a tree equation exists.
Permalink · Source line 814 · Claim record · Lean coverage · Code · Worked examples
11.2 Typed colored extension beyond the finite contract
On this page · Permalink · Source line 821
Definition 11.4: Finitary colored operation signature
A finitary colored signature consists of:
a finite type \(V\) of colors;
a type \(\Sigma\) of operation symbols;
an arity \(r(\sigma)\in{\mathbb N}\) for every \(\sigma\in\Sigma\);
input colors \(\operatorname{in}_\sigma:\operatorname{Fin}(r(\sigma))\to V\);
an output color \(\operatorname{out}(\sigma)\in V\).
A realization assigns a space \(X_v\) to each color and a map
Permalink · Source line 823 · Claim record · Lean coverage · Code · Worked examples
Outside the finite formal contract. The intended Lean target is a dependent inductive typed tree; no such declaration is part of the version 1.0.1 completion contract.
Definition 11.5: Typed operation tree and evaluation
A typed operation tree is recursively either a leaf of declared color or a node labeled by \(\sigma\), with one correctly colored child for each input slot of \(\sigma\). Evaluation is recursive:
Permalink · Source line 843 · Claim record · Lean coverage · Code · Worked examples
Outside the finite formal contract. Candidate API: Komorebi.PaperIII.NonlinearObstructions.ColoredOperationTree and ColoredOperationTree.eval. This is stronger than the compiled uncolored unary–binary grammar.
11.3 Packet labelings and the multilinear first target
On this page · Permalink · Source line 856
Suppose every \(X_v\) has a finite complete packet family \((P^v_i)_{i\in I_v}\). A packet labeling assigns an admissible packet index to each edge or node of a typed tree. For multilinear \(\Phi_\sigma\), inserting
at every input and output yields a finite sum over trees with packet labels. This is the branching analogue of inserting intermediate projectors in Proposition 8.1.
Formalization target 11.6: Finite multilinear tree expansion
The first milestone for the nonlinear module is an exact theorem saying that the evaluation of a finite tree of multilinear nodes equals the finite sum of its packet-resolved labeled evaluations. Required proof obligations include:
a dependent well-typed tree syntax;
finite packet-label types at every color;
an explicit convention for nullary and unary nodes;
multilinearity in every input slot;
preservation of input-slot order without assuming commutativity of operations.
Visual guide: Mixed terms are not optional · Permalink · Source line 868
Outside the finite formal contract. Candidate target: Komorebi.PaperIII.NonlinearObstructions.ColoredOperationTree.eval_eq_sum_packetLabellings.
11.4 Connection defects at nonlinear nodes
On this page · Permalink · Source line 884
For coordinate models of the source and target colors, an additive target coordinate space, and a chosen noncanonical connection, a pointwise node defect can be defined by
This expression compares two chosen routes. With canonical exact transport in every slot it vanishes by Proposition 10.1.
Formalization target 11.7: Operation-tree defect propagation
For multilinear nodes, one expects an exact finite expansion obtained by replacing one or more nodes by their defects and transporting the remaining branches. For smooth nonlinear nodes, the corresponding chain rule is indexed by rooted partitions and Faà di Bruno trees. A formal theorem will require a fixed differentiability category, base points, derivative conventions, symmetry factors, and remainder policy.
Visual guide: Where a nonlinear defect can enter · Permalink · Source line 900
Outside the finite formal contract. 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.
Boundary 11.8: Analytic and geometric exclusions
The finite formal contract does not include convergence of an infinite tree series, existence of derivatives, a Banach-space Faà di Bruno theorem, a Baker–Campbell–Hausdorff expansion, a continuum limit, or an identification of algebraic holonomy with curvature of a smooth bundle. Part II supplies ordinary proofs for its explicit nonlinear and analytic statements. This edition does not derive a connection from data, optimization, physics, or probability.
Permalink · Source line 911 · Claim record · Lean coverage · Code · Worked examples
12 Formalization ledger for version 1.0.1
On this page · Visual guide: Read the evidence with the pictures · Permalink · Source line 919
| Topic | Status | Declaration or roadmap target | Exact boundary |
|---|---|---|---|
| Packet matrix and edge operator | Lean-backed III | PacketGraph.packetMatrix; EdgeSystem.edgeOp | Finite scalar matrices over a semiring; one scalar coordinate per packet. |
| Edge support and pair dichotomy | Lean-backed III | edgeOp_eq_zero_off_support; edgeOp_mul_edgeOp_eq_zero; edgeOp_mul_edgeOp_of_composable | Broken interfaces vanish; matched pairs collapse to the endpoint block with coefficient in operator order. |
| Typed word evaluation | Lean-backed III | Composable; wordOp; wordOp_append; wordOp_eq_zero_of_not_composable | List order is execution order; concatenation reverses operator-product order; nonwalks vanish. |
| Finite word and walk expansions | Lean-backed III | explicitWordExpansion; walkExpansion; wordExpansion_eq_explicitWordExpansion; transferOp_pow_eq_walkExpansion | Actual finite tuple sum and zero-filtered composable-walk sum; finite graph and packet types. |
| Endpoint coefficient walk sum | Lean-backed III | reverseCoefficient; Connects; transferOp_pow_apply_eq_sum_walks | Exact scalar endpoint entry, including the empty-walk case and noncommutative coefficient order. |
| Fixed reachability and orbit support | Lean-backed III; inherited hull bridge | transferOp_pow_apply_eq_zero_of_no_walk; transferOp_pow_mulVec_apply_eq_zero_of_unreachable_support | Finite powers and supported seeds; the orbit-hull span conclusion uses the frozen Paper I contract. |
| Exact frame transport | Lean-backed III | exactTransport_cocycle; exactPathTransport_eq_endpoint; exactPathTransport_loop | One frame family on a single module; arbitrary finite paths telescope and closed paths are trivial. |
| Exact coordinate cocycle | Inherited Lean-backed II | NestedRefinement.refineCoordinates_comp; NestedRefinement.coordinateRefinementEquiv_trans | Complete finite projector coordinates, not reduction. |
| Typed coordinate naturality | Inherited Lean-backed II | NestedRefinement.coordinateOperator_comp; NestedRefinement.coordinateOperator_naturality | Linear maps over semiring modules. |
| Minimal connection API | Lean-backed III | Transport.Connection; cocycleDefect; triangleHolonomy; triangleHolonomy_eq_refl_of_flat | Only self-normalization is assumed; reverse inversion and the cocycle are not structure fields. |
| Twisted three-point loop | Lean-backed III | twistedThreePointConnection; twisted_triangleHolonomy_ne_refl | Concrete rational connection; the selected loop sends \(1\) to \(2\). |
| Reversible additive defect | Lean-backed III | ReversibleConnection; triangleHolonomy_sub_id; cocycleDefect_eq_zero_iff_triangleHolonomy_eq_refl | Heterogeneous module fibers, reverse-edge inversion, and an additive defect over a commutative ring. |
| Reversible finite paths | Lean-backed III | pathTransport_eq_direct_of_flat; indexedPathTransport_eq_direct_of_flat; indexedLoopTransport_eq_refl_of_flat | Finite pair-connection paths collapse to endpoints under algebraic flatness. |
| Gauge covariance | Lean-backed III | gauge_cocycleDefect; gauge_triangleHolonomy; gauge_flat_iff | Fiberwise algebraic conjugation; no smooth gauge theory. |
| Flat versus canonical transport | Lean-backed III | flatGauge; flat_isGaugeOfCanonical | A chosen base chart and ambient frames exhibit every flat pair connection as a gauge transform of canonical transport. |
| Operation-tree locality | Lean-backed III | OperationTree; OperationTree.eval; OperationTree.eval_congr_on_inputs | Arbitrary unary and binary semantics; only dependence on named inputs is proved. |
| Generic obstruction packet | Lean-backed III | ObstructionPacket.not_isSolution; not_isSolution_iff_nonempty_obstructionPacket | Exact candidate-specific logical certificate; no global classification. |
| Holonomy block obstruction | Lean-backed III | obstruction_sum_blocks; obstructionBlocks_zero_iff; obstructionDetection_equivalences | Finite complete idempotent packet family on the base fiber; orthogonality is not required by the compiled reconstruction. |
| Packet witness and block gauge | Lean-backed III | exists_packetWitness_of_obstructionBlock_ne_zero; obstructionBlock_gauge_of_commutes; obstructionBlock_gauge_eq_zero_iff | Witness extraction is classical; blockwise covariance requires the gauge to commute with every packet projector. |
| Heterogeneous matrix paths | Lean-backed III | heterogeneousPacketPathExpansion; heterogeneousProduct_apply_eq_zero_of_no_supportedPath | Arbitrarily many different matrices over one common finite packet type; fully typed changing-index chains compile only at lengths two and three. |
| Arbitrary-function coordinates | Lean-backed III | exactCoordinateMap_comp; exactCoordinateMap_naturality | Exact set-level equivalences and arbitrary functions; no linearity or differentiability assumption. |
| Colored and smooth trees | Roadmap only | roadmap ColoredOperationTree.eval_eq_sum_packetLabellings | Dependent colors, multilinear packet expansion, derivatives, and Faà di Bruno identities remain outside the contract. |
12.1 Kernel-backed Paper III surface
On this page · Permalink · Source line 1045
The authoritative declaration-level contract is formalization/lean/LEAN_THEOREM_MAP_v1.0.1.md. It groups the compiled surface as follows.
EdgeOperators and EdgeExtensions: scalar packet matrices, typed edge and word support, finite word/walk expansions, endpoint coefficient sums, fixed-length reachability, orbit support, and common-index heterogeneous products with declared supports.
Transport and ReversibleConnections: exact frame transport, the minimal connection, heterogeneous reversible pair transport, additive defect and triangle holonomy, finite paths, canonical connections, and the fiberwise gauge action.
CoordinateNaturality and HolonomyBlocks: composition and naturality for arbitrary functions between exact coordinate systems, finite two-sided block reconstruction, equivalent obstruction criteria, packet-supported witnesses, and packet-preserving block gauges.
NonlinearObstructions: finite unary–binary operation trees, input locality, and candidate-specific obstruction certificates.
The release verification report records the checker-generated declaration and audit totals. The parity gate requires every fully qualified Paper III target printed beside a statement to occur in the theorem map, rejects stale or duplicate targets, and checks it against the compiled environment. KernelAudit.lean reports dependencies for the mapped and supporting theorems, and its fail-closed gate scans every compiled Komorebi.PaperIII declaration. The four inherited statement contracts remain identified separately by their Papers I–II names.
Boundary 12.1: No scope promotion by prose
The displayed endpoint coefficient formula, reachability results, reversible connection theorems, additive defect–holonomy identity, gauge covariance, holonomy-block reconstruction, packet witnesses, common-index heterogeneous path expansion, and arbitrary-function coordinate naturality are all part of the version 1.0.1 kernel-backed surface. What remains outside is the dependent fiber-valued edge-system generalization, a fully dependent arbitrary-length chain whose module and packet type change at every stage, dependent colored operation trees, packet-labeled multilinear tree expansions, nonlinear tree-defect and Faà di Bruno identities, and the analytic and geometric extensions listed above.
Permalink · Source line 1075 · Claim record · Lean coverage · Code · Worked examples
13 The finite contract and the nonlinear transition
On this page · Permalink · Source line 1088
Typed packet support turns the expansion of a transfer power into a walk calculus. Incompatible words vanish because their interfaces do not match. Canonical packet coordinate transport is the exact equivalence obtained from analysis and synthesis. It satisfies the cocycle law, so every finite canonical loop telescopes to the identity. Holonomy enters after a separate connection is supplied. The compiled minimal API proves that flatness makes both the relative defect and holonomy trivial, and it exhibits a nontrivial rational loop. Under the compiled reversible API, a nonzero additive triangle defect is equivalent to nonidentity holonomy, transforms covariantly under gauge, and is detected exactly by a finite family of packet blocks. Finite flat paths collapse to their endpoints. Every flat reversible pair connection is explicitly related to canonical transport by a gauge change through a chosen base chart.
These facts define the boundary of the finite formal contract. At that boundary, exact coordinates preserve composition and satisfy naturality for arbitrary functions in Paper III, while the typed linear packet coordinate counterpart remains inherited from Paper II. Nontrivial nonlinear defects must therefore be attached to additional modeling choices or to packet compatibility of the particular operation. Colored operation trees, multilinear packet labelings, and Faà di Bruno expansions remain outside this finite Lean contract. Part II develops the corresponding ordinary mathematics, including packet jets, rooted tree expansions, and explicit nonlinear obstruction theorems.