recAlg_id_left
plain-language theorem explainer
The left unit law holds for morphisms in the Recognition Algebra category: composing the identity on the target object with any cost morphism f recovers the underlying map of f. Algebraists working in Recognition Science cite this when confirming that RecAlg satisfies the category axioms. The proof is a one-line term that applies extensionality to the underlying maps and simplifies using the lifted definitions of composition and identity from CostAlgebra.
Claim. Let $C_1, C_2$ be cost algebra data bundles and let $f: C_1 → C_2$ be a cost morphism. Then $(id_{C_2} ∘ f).map = f.map$.
background
RecAlgObj is the type of cost algebra data bundles. RecAlgHom is the type of cost morphisms, i.e., maps on positive reals that are multiplicative and preserve the J-cost function. The category RecAlg is constructed by lifting the composition and identity operations defined in CostAlgebra, where comp composes two J-automorphisms and id is the identity J-automorphism.
proof idea
The proof applies the ext tactic to equate the morphisms by their underlying maps, then uses simp with the lemmas recAlg_comp, recAlg_id, CostMorphism.comp, CostMorphism.id and Function.comp to unfold the definitions and obtain the required equality.
why it matters
This lemma is invoked inside category_certificate to verify that RecAlg satisfies the left identity axiom. It completes one of the six items in the Recognition Category Certificate, confirming that the algebra of cost morphisms forms a category. The result supplies the neutral-element property required for the Recognition Composition Law and for the algebraic layer of the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.