Part I Finite typed transfer and the formal contract
On this page · Permalink · Source line 1
The finite release supplies the algebraic foundation and a contract for its individual declarations. Here, “roadmap” and “outside the contract” describe the scope of the finite Lean formalization. Ordinary mathematical results in Part II may lie beyond that scope. The thirty original result environments and their proof bodies are retained. The source contract has 41 mapping rows because it also includes definitions and other interfaces.
The preserved v1.0.1 release records Lean v4.34.0-rc2 against Mathlib revision aeb72f1e9981b6d35b426b16dca7759be3e7ba06 [lean], [mathlib]. The current release rebuilds the Paper III source at these exact pins and records fresh kernel replay and axiom checks. References to declarations from Papers I–II retain their explicitly inherited status. The companion Lean guide distinguishes the original finite map from the additional packet-coordinate and analytic interfaces.
1 Purpose and formal status
On this page · Visual guide: Three objects, three different questions · Permalink · Source line 5
Paper I fixed typed seeds, operator grammars, exact projector packets, generated hulls, and reconstruction [paperI]. Paper II added coherent refinement coordinates, weighted transfer, arithmetic separation, and linear defect identities [paperII]. The present paper begins the next layer: explicit edge words, optional connection data, and obstructions within individual packets.
Canonical coordinate transport and a connection play different mathematical roles. Canonical transport compares two exact descriptions of the same ambient object and is forced by analysis and synthesis. A connection chooses transports that may carry extra modeling, discretization, or gauge information. Canonical transport obeys a cocycle theorem. A connection may fail to obey a cocycle, and that failure is meaningful data. Keeping separate notation lets us distinguish the automatic coherence of exact coordinates from the possible holonomy of a chosen connection.
1.1 Statement labels
On this page · Permalink · Source line 24
Every substantial theorem, lemma, corollary, proposition, definition, API, and roadmap item carries one or more of the three labels below. When separate clauses use a Paper III result and an inherited bridge, the statement carries both applicable labels. Illustrative examples do not require a label.
Lean-backed in Paper III: the displayed scope is no stronger than the named compiled declaration in the released Paper III module.
Inherited Lean-backed: the displayed result is supplied by the frozen formal contract of Paper I or II.
Roadmap only: the text states a future interface or theorem target and is excluded from the completion denominator.
Boundary 1.1: Final theorem denominator
The completion denominator of the finite v1.0.1 contract consists of the thirty result environments in Part I. Of these, 26 resolve to compiled Paper III declarations and four resolve to the frozen Papers I–II contracts. The authoritative theorem map names the exact declarations used by each statement. The kernel audit checks those targets and their supporting theorems. The namespace gate requires every declaration in the compiled Komorebi.PaperIII namespace to pass its checks. Roadmap items are excluded from the denominator and remain visibly marked.
Permalink · Source line 39 · Claim record · Lean coverage · Code · Worked examples
2 Finite typed packet graphs
On this page · Permalink · Source line 50
2.1 Orientation and matrix convention
On this page · Permalink · Source line 53
Let \(V\) be a finite packet type, \(E\) a finite edge type, and \(R\) a semiring. A directed multigraph is a pair of endpoint functions
Parallel edges remain distinct elements of \(E\). Rows are targets and columns are sources. Thus an edge \(e:i\to j\) is represented by a matrix supported at row \(j\), column \(i\).
Definition 2.1: Packet graph and scalar edge system
For \(a,b\in V\) and \(r\in R\), define
An edge system is a coefficient function \(c:E\to R\). Its elementary edge operator and total transfer operator are
Visual guide: An atlas of the objects · Permalink · Source line 64 · Claim record · Lean coverage · Code · Worked examples
Formal contract: Paper III v1.0.1. Komorebi.PaperIII.EdgeOperators.PacketGraph; Komorebi.PaperIII.EdgeOperators.PacketGraph.packetMatrix; Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem; Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.edgeOp; Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.transferOp
Words are written in execution order. In \(L_fL_e\), the rightmost operator \(L_e\) acts first. For a written word \((e_1,\ldots,e_n)\), \(e_1\) acts first and the operator product is \(L_{e_n}\cdots L_{e_1}\).
Reading the execution order
Read the edge list in the order of execution. The matrix product writes later actions farther to the left. The target packet of one edge must equal the source packet of the next before multiplication can contribute. Over a noncommutative semiring, this order also fixes the order of the scalar coefficients.
Lemma 2.2: Declared support
For every edge \(e\), \((L_e)_{yx}=0\) unless \(y={\operatorname{tgt}}(e)\) and \(x={\operatorname{src}}(e)\).
Visual guide: Read the product in execution order · Permalink · Source line 96 · Claim record · Lean coverage · Code · Worked examples
Formal contract: Paper III v1.0.1. Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.edgeOp_eq_zero_off_support
Theorem 2.3: Typed interface annihilation
If \({\operatorname{tgt}}(e)\ne{\operatorname{src}}(f)\), then
Visual guide: Read the product in execution order · Permalink · Source line 103 · Claim record · Lean coverage · Code · Worked examples
Formal contract: Paper III v1.0.1. Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.edgeOp_mul_edgeOp_eq_zero
Proof
For a matrix entry \((y,x)\),
A potentially nonzero summand would require simultaneously \(z={\operatorname{src}}(f)\) and \(z={\operatorname{tgt}}(e)\), contrary to the hypothesis.
Theorem 2.4: Collapse of a matched edge pair
If \({\operatorname{tgt}}(e)={\operatorname{src}}(f)\), then
Together with Theorem 2.3, this gives both cases for the composition of two edge operators.
Visual guide: Read the product in execution order · Permalink · Source line 121 · Claim record · Lean coverage · Code · Worked examples
Formal contract: Paper III v1.0.1. Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.edgeOp_mul_edgeOp_of_composable
Proof
The matrix-product sum has exactly one potentially nonzero intermediate index, namely \({\operatorname{tgt}}(e)={\operatorname{src}}(f)\). At that index the coefficients occur in operator order as \(c(f)c(e)\), and the outer source and target are \({\operatorname{src}}(e)\) and \({\operatorname{tgt}}(f)\).
Boundary 2.5: Current fiber scope
The compiled Paper III model above has one scalar coordinate per packet. For a family of modules \((X_i)_{i\in V}\), an intrinsic edge map would instead have type \(\ell_e:X_{{\operatorname{src}}(e)}\to X_{{\operatorname{tgt}}(e)}\), and its totalization on \(\bigoplus_iX_i\) would be \(\iota_{{\operatorname{tgt}}(e)}\ell_e\pi_{{\operatorname{src}}(e)}\). The same support proof applies, but this generalization with dependent fibers is not attributed to the released Paper III modules for scalar edge systems.
Permalink · Source line 142 · Claim record · Lean coverage · Code · Worked examples
Figure summarizes the support convention and shows how composable words differ from words with a broken interface. The next section uses this distinction.
3 Operator words and directed walks
On this page · Permalink · Source line 166
3.1 Typed words
On this page · Permalink · Source line 169
Definition 3.1: Composable word and execution operator
A finite word \(w=(e_1,\ldots,e_n)\) is composable when
Set
This definition records the written order of execution even though matrix composition is read right to left.
Permalink · Source line 171 · Claim record · Lean coverage · Code · Worked examples
Formal contract: Paper III v1.0.1. Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.Composable; Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.wordOp
Theorem 3.2: First broken interface
If a word begins \((e,f,\ldots)\) and \({\operatorname{tgt}}(e)\ne{\operatorname{src}}(f)\), then its word operator is zero.
Permalink · Source line 188 · Claim record · Lean coverage · Code · Worked examples
Formal contract: Paper III v1.0.1. Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.wordOp_eq_zero_of_first_break
Theorem 3.3: Noncomposable words vanish
If \(w\) is not composable, then \(L_w=0\).
Permalink · Source line 195 · Claim record · Lean coverage · Code · Worked examples
Formal contract: Paper III v1.0.1. Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.wordOp_eq_zero_of_not_composable
Proof
Choose the first broken adjacent pair. The corresponding consecutive factor is zero by Theorem 2.3, and associativity absorbs that zero into the complete product. The Lean proof implements the same argument by induction on the list.
3.2 The checked recursive expansion
On this page · Permalink · Source line 208
Definition 3.4: Recursive word expansion
Define
Permalink · Source line 210 · Claim record · Lean coverage · Code · Worked examples
Formal contract: Paper III v1.0.1. Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.wordExpansion
Theorem 3.5: Transfer power equals recursive word expansion
For every \(n\in{\mathbb N}\),
Permalink · Source line 221 · Claim record · Lean coverage · Code · Worked examples
Formal contract: Paper III v1.0.1. Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.transferOp_pow_eq_wordExpansion
Proof
The zero case is the identity matrix. If \(T^n={\mathcal W}_n\), then the left-successor power convention gives \(T^{n+1}=TT^n=T{\mathcal W}_n={\mathcal W}_{n+1}\).
Remark 3.6
The formal module also defines an explicit sum over tuples \(w:\operatorname{Fin}(n)\to E\) and a second sum in which noncomposable tuples are replaced by zero. It proves that the recursive matrix, the explicit tuple sum, and the sum filtered by composability agree. The separate declarations make the finite enumeration claim directly checkable.
Formal contract: Paper III v1.0.1. Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.explicitWordExpansion; Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.walkExpansion; Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.wordExpansion_eq_explicitWordExpansion; Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.explicitWordExpansion_eq_walkExpansion
3.3 Exact expansion from words to walks
On this page · Permalink · Source line 245
For a nonempty composable word \(w=(e_1,\ldots,e_n)\), define its reverse coefficient product
The reversal is essential over a noncommutative semiring.
Lemma 3.7: One word is one endpoint block
If \(w=(e_1,\ldots,e_n)\) is nonempty and composable, then
Visual guide: Coefficients need not commute · Permalink · Source line 254 · Claim record · Lean coverage · Code · Worked examples
Formal contract: Paper III v1.0.1. Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.reverseCoefficient; Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.terminalTarget; Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.wordOp_eq_packetMatrix_of_composable
Proof
Induct on \(n\). The case \(n=1\) is the definition of \(L_e\). Suppose the formula holds for the prefix \((e_1,\ldots,e_n)\) and append \(f\). Composability gives \({\operatorname{tgt}}(e_n)={\operatorname{src}}(f)\). Multiplying the two packet matrices leaves one intermediate index and changes the coefficient to \(c(f)c(e_n)\cdots c(e_1)\), with source \({\operatorname{src}}(e_1)\) and target \({\operatorname{tgt}}(f)\).
Write \({\operatorname{Walk}}_n(i,j)\) for the finite set of composable edge tuples of length \(n\) whose first source is \(i\) and whose final target is \(j\). For \(n=0\), it has one empty walk when \(i=j\) and is empty otherwise. Assign the empty walk the coefficient \(1\).
The empty walk
The empty walk records doing nothing at a chosen packet. It contributes only to a diagonal entry. Thus the convention for length zero matches the identity matrix and lets the walk sum include every nonnegative power.
Theorem 3.8: Finite operator expansion from words to walks
For every \(n\in{\mathbb N}\),
Parallel edges occur as distinct summands.
Visual guide: All sixteen words, only five walks · Permalink · Source line 285 · Claim record · Lean coverage · Code · Worked examples
Formal contract: Paper III v1.0.1. Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.transferOp_pow_eq_explicitWordExpansion; Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.transferOp_pow_eq_walkExpansion
Proof
Induction and finite distributivity give
Every noncomposable summand is zero by Theorem 3.3, so inserting the composability filter does not change the sum. In Lean, tuple concatenation and the successor sum are handled by tupleWordOp_snoc and explicitWordExpansion_succ; the two bridge equalities then yield the displayed theorem.
Corollary 3.9: Endpoint coefficient walk sum
For all \(n\in{\mathbb N}\) and \(i,j\in V\),
Visual guide: All sixteen words, only five walks · Visual guide: A reachable packet can receive zero · Permalink · Source line 320 · Claim record · Lean coverage · Code · Worked examples
Formal contract: Paper III v1.0.1. Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.Connects; Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.endpointWalkCoefficientSum; Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.transferOp_pow_apply_eq_sum_walks
Proof
Take the \((j,i)\) entry in Theorem 3.8. By Lemma 3.7, a surviving word contributes \(c^\leftarrow(w)\) exactly when its endpoints are \(i\) and \(j\), and contributes zero otherwise. At \(n=0\), the identity matrix gives the unique empty diagonal walk.
Corollary 3.10: Reachability obstruction at fixed length
If \({\operatorname{Walk}}_n(i,j)=\varnothing\), then \((T^n)_{ji}=0\).
Visual guide: A reachable packet can receive zero · Permalink · Source line 341 · Claim record · Lean coverage · Code · Worked examples
Formal contract: Paper III v1.0.1. Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.transferOp_pow_apply_eq_zero_of_no_walk
Proof
This is immediate from the empty sum in the preceding corollary.
Corollary 3.11: Orbit support obstruction
Let \(S\subseteq V\), and let \(x\in R^V\) be supported on \(S\). If \(j\) is not reachable by a directed path from any vertex of \(S\), then
Hence the orbit under \(T\) of \(x\) cannot generate a vector with a nonzero coordinate at \(j\).
Visual guide: Reachability is only an upper bound · Permalink · Source line 351 · Claim record · Lean coverage · Code · Worked examples
Formal contract: Paper III v1.0.1. Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.Reachable; Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.transferOp_pow_mulVec_apply_eq_zero_of_unreachable_support Inherited formal contract: Papers I–II. Komorebi.PacketNaturalityCompletion.Reachability.algebraicOrbitHull_le_reachable_support; Komorebi.PacketNaturalityCompletion.Reachability.unreachable_nonzero_packet_obstruction
Proof
Expand \((T^nx)_j=\sum_i(T^n)_{ji}x_i\). Terms with \(i\notin S\) vanish by the support of \(x\), and terms with \(i\in S\) vanish by Corollary 3.10. The final claim follows because the \(j\)-coordinate also vanishes on every finite linear combination of orbit vectors.
4 Canonical exact coordinate transport
On this page · Visual guide: Three objects, three different questions · Permalink · Source line 372
4.1 The Paper III frame model
On this page · Permalink · Source line 375
Let every chart \(a\) carry a linear frame equivalence \(F_a:M\xrightarrow{\sim}M\). The formal Paper III module defines transport from \(a\) to \(b\) by
This frame formula means synthesize in chart \(a\), then analyze in chart \(b\).
Theorem 4.1: Exact frame transport is coherent
For every \(a,b,c\),
and therefore
Visual guide: One vector, three exact frames · Permalink · Source line 386 · Claim record · Lean coverage · Code · Worked examples
Formal contract: Paper III v1.0.1. Komorebi.PaperIII.Transport.exactTransport_self; Komorebi.PaperIII.Transport.exactTransport_roundTrip; Komorebi.PaperIII.Transport.exactTransport_cocycle; Komorebi.PaperIII.Transport.exactTransport_triangleLoop
Proof
Every identity is cancellation of adjacent \(F_rF_r^{-1}\) factors. The Lean definitions use LinearEquiv.trans; the displayed formulas use the equivalent right-to-left function-composition notation fixed in this paper.
Theorem 4.2: Every finite canonical path telescopes
Let \(p=(a_0,a_1,\ldots,a_n)\) be any finite vertex list and put
Then
In particular, if \(a_n=a_0\), then \(J_p={\mathrm{id}}\).
Visual guide: One vector, three exact frames · Permalink · Source line 407 · Claim record · Lean coverage · Code · Worked examples
Formal contract: Paper III v1.0.1. Komorebi.PaperIII.Transport.pathEndpoint; Komorebi.PaperIII.Transport.exactPathTransport; Komorebi.PaperIII.Transport.exactPathTransport_eq_endpoint; Komorebi.PaperIII.Transport.exactPathTransport_loop
Proof
Induct on the list of successive vertices and apply the cocycle in Theorem 4.1 at each step. If the endpoint is the start, the endpoint transport is the identity.
4.2 Exact packet coordinates
On this page · Permalink · Source line 430
The graph model above resolves a fixed scalar matrix. Coordinate transport is a separate construction. Let \(X\) be an \(R\)-module, and let
be a finite complete family of pairwise orthogonal linear idempotents:
Define the exact packet coordinate module
Its analysis and synthesis maps are
Completeness and orthogonality give
What a packet coordinate contains
A packet coordinate is a whole vector fixed by its projector. Analysis splits an ambient vector into these components, and synthesis adds them back. The transport between exact systems keeps the ambient vector and changes its packet presentation.
Definition 4.3: Canonical exact coordinate transport
For two exact packet systems on the same ambient module, define
The arrow points from the source coordinate system \(a\) to the target coordinate system \(b\).
Permalink · Source line 469 · Claim record · Lean coverage · Code · Worked examples
Inherited formal contract: Papers I–II. Komorebi.PaperII.NestedRefinement.refineCoordinates; Komorebi.PaperII.NestedRefinement.coordinateRefinementEquiv
Theorem 4.4: Identity, inverse, and cocycle for canonical transport
For any exact packet systems \(a,b,c\) on \(X\),
Permalink · Source line 483 · Claim record · Lean coverage · Code · Worked examples
Inherited formal contract: Papers I–II. Komorebi.PaperII.NestedRefinement.refineCoordinates_self; Komorebi.PaperII.NestedRefinement.coarsenCoordinates_refineCoordinates; Komorebi.PaperII.NestedRefinement.refineCoordinates_coarsenCoordinates; Komorebi.PaperII.NestedRefinement.refineCoordinates_comp; Komorebi.PaperII.NestedRefinement.coordinateRefinementEquiv_trans
Proof
Insert \({\mathcal S}_b{\mathcal A}_b={\mathrm{id}}_X\):
The identity statement is \({\mathcal A}_a{\mathcal S}_a={\mathrm{id}}\). Setting \(c=a\) in the cocycle gives \(J^X_{a\leftarrow b}J^X_{b\leftarrow a}={\mathrm{id}}\); interchanging \(a\) and \(b\) gives the other composition, so the two transports are inverses.
If \(F:X\to Y\) is linear and \({\mathcal P}^a,{\mathcal P}^b\) are source packet systems while \({\mathcal Q}^r,{\mathcal Q}^s\) are target packet systems, put
Theorem 4.5: Canonical coordinate naturality
The exact coordinate representation preserves typed composition and satisfies
Permalink · Source line 517 · Claim record · Lean coverage · Code · Worked examples
Inherited formal contract: Papers I–II. Komorebi.PaperII.NestedRefinement.coordinateOperator_comp; Komorebi.PaperII.NestedRefinement.coordinateOperator_naturality
Proof
Both sides reduce to \({\mathcal A}^Y_sF{\mathcal S}^X_a\) after inserting the appropriate synthesis–analysis identity. The composition law is the same calculation with the middle ambient module inserted.
Corollary 4.6: Canonical triangle holonomy is trivial
For every triple \(a,b,c\),
Permalink · Source line 534 · Claim record · Lean coverage · Code · Worked examples
Inherited formal contract: Papers I–II. Komorebi.PaperII.NestedRefinement.refineCoordinates_comp; Komorebi.PaperII.NestedRefinement.refineCoordinates_self
Boundary 4.7: Refinement is not reduction
Although Paper II uses the name refineCoordinates, \(J\) is an equivalence between two complete coordinate presentations. It neither truncates packets nor projects to a smaller state space. Any lossy restriction, interpolation, or learned identification is extra data and cannot inherit Theorem 4.4 without proof.
Permalink · Source line 543 · Claim record · Lean coverage · Code · Worked examples