recAlg_id_right
plain-language theorem explainer
The right unit law holds for morphisms in the recognition algebra category: composing any cost morphism f from C1 to C2 on the right with the identity on C1 leaves the underlying map of f unchanged. Category theorists verifying the axioms of RecAlg would cite this when confirming identity neutrality. The proof is a one-line wrapper that applies function extensionality followed by simplification on the definitions of composition and identity.
Claim. For cost algebras $C_1, C_2$ and a cost morphism $f: C_1 → C_2$, the composition of $f$ with the identity on $C_1$ satisfies $(f ∘ id_{C_1}).map = f.map$.
background
Objects in this category are cost algebra data bundles while morphisms are cost morphisms, i.e., positive multiplicative maps on the positive reals that preserve the cost function. The identity morphism on any such object is the identity map, which is a cost morphism by direct verification. This theorem establishes right neutrality of the identity under composition in the category RecAlg.
proof idea
The proof applies function extensionality to the underlying map and simplifies using the definitions of composition as CostMorphism.comp, identity as CostMorphism.id, and the explicit action of both operations.
why it matters
This result is invoked inside the category_certificate theorem that confirms RecAlg obeys the category axioms (associativity and identity neutrality). It completes the verification that identities act neutrally, supporting the claim that the canonical cost algebra J is initial in RecAlg and thereby grounding the forcing chain from T0 through T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.