recAlg_comp_assoc
plain-language theorem explainer
Composition of cost morphisms in the Recognition Algebra category is associative on their underlying maps. Researchers constructing the RecAlg category to support Recognition Science derivations cite this to confirm the associativity axiom holds. The proof is a one-line term-mode wrapper that applies extensionality and simplification on the definitions of recAlg_comp and CostMorphism.comp.
Claim. Let $C_1,C_2,C_3,C_4$ be cost algebra data bundles and let $h:C_3→C_4$, $g:C_2→C_3$, $f:C_1→C_2$ be cost morphisms. Then the underlying map of the composite $h∘(g∘f)$ equals the underlying map of the composite $(h∘g)∘f$.
background
In the RecognitionCategory module objects are cost algebra data bundles carrying the J-function and multiplicative structure. Morphisms are cost morphisms: maps from positive reals to positive reals that are multiplicative and preserve cost, as defined in the CostMorphism structure. The local setting is the assembly of these data into a category whose composition is delegated to CostMorphism.comp.
proof idea
The proof applies extensionality to equate the two morphisms by their maps. It then simplifies using the definitions of recAlg_comp (which calls CostMorphism.comp) and Function.comp, reducing both sides to identical nested compositions.
why it matters
This theorem supplies the associativity axiom required for RecAlg to form a category, alongside the identity morphisms in sibling declarations such as recAlg_id_left and recAlg_id_right. It anchors the algebraic layer that feeds into the Recognition Composition Law and the forcing chain steps T5–T8. No open questions are resolved here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.