ledgerAlg_id_left
plain-language theorem explainer
The left identity law for morphisms in the LedgerAlg category states that composing the identity on the codomain with any morphism f recovers f exactly. Algebraists verifying that LedgerAlg forms a category within Recognition Science would cite this result. The proof is a one-line wrapper that unfolds the definitions of composition and identity then applies extensionality and reflexivity on the underlying linear maps.
Claim. Let $n$ be a natural number, let $A$ and $B$ be subspaces of admissible flows (antisymmetric and conserved) in the flow space of dimension $n$, and let $f$ be a linear map from the carrier of $A$ to the carrier of $B$. Then the composition of the identity linear map on $B$ with $f$ equals $f$.
background
LedgerAlgObj consists of subspaces of the flow space that satisfy antisymmetry and conservation. LedgerAlgHom are linear maps between these carriers. The identity morphism is defined as the identity linear map, while composition is ordinary composition of linear maps. This declaration lives in the Algebra.RecognitionCategory module, which imports CostAlgebra, PhiRing, LedgerAlgebra and OctaveAlgebra. Upstream results include the identity event at the J-cost minimum from ObserverForcing and the active edge count A from IntegrationGap.
proof idea
The proof is a one-line wrapper. It applies the definition of ledgerAlg_comp (which composes the underlying linear maps) and ledgerAlg_id (which supplies the identity map), then uses extensionality on the linear map followed by reflexivity.
why it matters
This result supplies the left unit law required for LedgerAlg to be a category, feeding the larger RecognitionCategory construction that models admissible flows and costs. It sits alongside the right identity and associativity siblings and supports the algebraic layer beneath the forcing chain (T0-T8) and Recognition Composition Law. No open questions are touched; the declaration is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.