ledgerAlg_id
plain-language theorem explainer
The identity morphism in LedgerAlg sends each admissible-flow subspace to itself by the identity linear map on its carrier. Category theorists assembling Recognition Science algebras cite this when forming composite identities such as the one for LayerSys⁺. The definition is a direct one-line wrapper that installs Mathlib's LinearMap.id into the LedgerAlgHom record.
Claim. For any natural number $n$ and any object $A$ in LedgerAlg (a submodule of FlowSpace $n$ whose elements are antisymmetric and conserved flows), the identity morphism $A$ to $A$ is the linear map given by the identity on the carrier submodule.
background
LedgerAlgObj is the structure whose carrier is a submodule of FlowSpace $n$ together with proofs that every element is antisymmetric and conserved. LedgerAlgHom consists of linear maps between such carriers. The module RecognitionCategory imports CostAlgebra, PhiRing, LedgerAlgebra and OctaveAlgebra to equip these objects with the multiplicative structure required by the Recognition Composition Law.
proof idea
One-line wrapper that applies LinearMap.id to populate the map field of LedgerAlgHom.
why it matters
Supplies the identity required by the LedgerAlg category and is invoked inside layerSysPlus_id to assemble the full identity for LayerSys⁺. It also feeds the left and right unit theorems ledgerAlg_id_left and ledgerAlg_id_right. In the Recognition framework this closes the algebraic layer that supports the forcing chain T0-T8 and the J-cost compatibility enforced by CostAxioms.Composition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.