category_certificate
plain-language theorem explainer
The declaration establishes that identity morphisms in the recognition algebra category act as neutral elements under composition when restricted to underlying maps. Researchers formalizing categorical structures for Recognition Science would cite it to confirm the category axioms hold for cost algebra data bundles. The proof is a direct term-mode pairing of the left and right identity lemmas.
Claim. For all cost algebra data bundles $C_1, C_2$ and cost morphisms $f: C_1 → C_2$, the composition of the identity on $C_2$ with $f$ satisfies $(id_{C_2} ∘ f).map = f.map$, and the composition of $f$ with the identity on $C_1$ satisfies $(f ∘ id_{C_1}).map = f.map$.
background
Objects in RecAlg are cost algebra data bundles; morphisms are cost morphisms between them. Composition of morphisms and identity morphisms are defined by lifting the corresponding operations from CostMorphism. The local setting is the categorical foundation for Recognition Science, where this category encodes cost structures with initial object given by the canonical J-cost. The theorem relies on the upstream definitions of recAlg_id (identity morphism via CostMorphism.id) and recAlg_comp (composition via CostMorphism.comp), together with the prior theorems recAlg_id_left and recAlg_id_right that establish neutrality on underlying maps.
proof idea
The proof is a term-mode construction that directly returns the pair consisting of the left-identity lemma recAlg_id_left and the right-identity lemma recAlg_id_right.
why it matters
This result completes the verification of the identity axioms for the recognition algebra category, directly supporting the module claim that Recognition Science is the initial algebra (hence unique up to isomorphism) and that domains arise as functorial images. It feeds the broader certificate that includes associativity, initial object existence, and monotone invariance. The construction aligns with the forcing chain landmarks by ensuring representation independence for the phi-ladder and J-cost structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.