ledgerAlg_comp
The definition supplies the composition of morphisms in the Ledger algebra category, where objects are submodules of admissible flows and morphisms are linear maps between them. Researchers building the algebraic backbone of Recognition Science cite it to assemble layered systems such as LayerSysPlus. The definition is realized as a one-line wrapper that composes the underlying linear maps of the input morphisms.
claimFor a natural number $n$ and objects $A, B, C$ consisting of submodules of the flow space that are antisymmetric and conserved, the composition of a morphism $g$ from $B$ to $C$ with a morphism $f$ from $A$ to $B$ is the morphism from $A$ to $C$ whose linear map is the composition of those of $g$ and $f$.
background
The RecognitionCategory module defines several algebraic categories to capture structures in Recognition Science. Ledger algebra objects consist of submodules of the flow space equipped with proofs that all elements are antisymmetric and conserved flows. Ledger algebra morphisms consist of linear maps from the carrier submodule of one object to that of another.
proof idea
The definition is a one-line wrapper that applies the composition of linear maps to the map components of the two input morphisms.
why it matters in Recognition Science
This definition is invoked in the construction of composition for the LayerSysPlus category and underpins the associativity and unit theorems for Ledger algebra morphisms. It contributes to the algebraic realization of the Recognition Composition Law within the framework's forcing chain, where composition of admissible flows supports the derivation of spatial dimensions and physical constants.
scope and limits
- Does not verify the category axioms for the Ledger algebra.
- Does not incorporate the J-cost function into the composition.
- Does not extend to morphisms outside the admissible flow subspaces.
- Does not address associativity or identity properties.
formal statement (Lean)
645def ledgerAlg_comp {n : ℕ} {A B C : LedgerAlgObj n}
646 (g : LedgerAlgHom B C) (f : LedgerAlgHom A B) : LedgerAlgHom A C where
647 map := g.map.comp f.map
proof body
Definition body.
648
649/-- Associativity of `LedgerAlg` composition on underlying linear maps. -/