ledgerAlg_id_right
plain-language theorem explainer
The right identity law holds for morphisms in LedgerAlg: composing any linear map f with the identity on its domain recovers f. Category theorists in Recognition Science cite this when confirming that LedgerAlg satisfies the axioms of a category. The proof reduces the equality to reflexivity after applying extensionality to the underlying maps.
Claim. For any natural number $n$, any LedgerAlg objects $A$ and $B$ (subspaces of admissible flows in FlowSpace $n$ satisfying antisymmetry and conservation), and any linear map $f$ from the carrier of $A$ to the carrier of $B$, the composition of $f$ with the identity linear map on $A$ equals $f$.
background
LedgerAlgObj n consists of subspaces of admissible flows equipped with antisymmetry and conservation conditions on their carriers. LedgerAlgHom are linear maps between such objects. The identity morphism is defined as the identity linear map on the carrier, while composition is defined by composing the underlying linear maps.
proof idea
One-line wrapper that applies extensionality to the linear map equality and then reflexivity.
why it matters
This result verifies the right identity axiom for the LedgerAlg category of admissible flows. It supports the construction of RecognitionCategory by ensuring standard categorical identities hold at the algebraic level of conserved flows. The declaration aligns with the algebra layer that underpins the forcing chain's consistency requirements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.