ledgerAlg_comp_assoc
plain-language theorem explainer
LedgerAlg composition is associative on the underlying linear maps between admissible flow subspaces. Category theorists in the Recognition algebra layer would cite this when confirming that LedgerAlg satisfies the category axioms. The proof is a one-line wrapper that applies extensionality to the maps and reduces by reflexivity after unfolding the composition definition.
Claim. Let $A,B,C,D$ be LedgerAlg objects over dimension $n$, each a submodule of FlowSpace $n$ consisting of antisymmetric conserved flows. Let $f:A.to B$, $g:B.to C$, $h:C.to D$ be morphisms given by linear maps on the carriers. Then the underlying map of the composite $h circ (g circ f)$ equals the underlying map of $(h circ g) circ f$.
background
LedgerAlgObj n is the structure whose carrier is a Submodule of FlowSpace n together with proofs that every element is an antisymmetric conserved flow. LedgerAlgHom consists of linear maps between such carriers. The upstream definition ledgerAlg_comp assembles a new morphism by composing the underlying linear maps via g.map.comp f.map. The module RecognitionCategory assembles these pieces into an algebraic category whose objects represent admissible flows.
proof idea
One-line wrapper that applies the extensionality tactic to the linear maps, then reflexivity. Both sides reduce to the same triple composition of linear maps once ledgerAlg_comp is unfolded.
why it matters
The result supplies the associativity axiom for morphism composition in LedgerAlg, a prerequisite for treating the admissible-flow spaces as a category inside the Recognition algebra. It sits alongside the sibling recAlg_comp_assoc and supports later constructions that embed the phi-ladder and eight-tick octave into categorical language. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.