recAlg_comp
plain-language theorem explainer
recAlg_comp supplies the composition of morphisms in the Recognition Algebra category by delegating to the underlying CostMorphism operation. Researchers assembling categorical models of cost algebras cite it when verifying that RecAlg satisfies the category axioms. The definition is a direct one-line wrapper around CostMorphism.comp.
Claim. Let $C_1, C_2, C_3$ be cost algebra data bundles. For cost morphisms $g: C_2 → C_3$ and $f: C_1 → C_2$, the composite $g ∘ f : C_1 → C_3$ is the cost morphism whose underlying map is the pointwise composition of the maps of $g$ and $f$.
background
In RecognitionCategory, objects are cost algebra data bundles (RecAlgObj := CostAlgebraData) and morphisms are cost morphisms (RecAlgHom := CostMorphism C₁ C₂). A cost morphism consists of a map ℝ → ℝ that preserves positivity and multiplication while preserving the J-cost function. The module constructs the category RecAlg whose morphisms must satisfy the standard category laws on these underlying maps. Upstream, CostAlgebra.comp defines composition of J-automorphisms by pointwise function composition and a multiplicativity check; CostAxioms.Composition encodes the Recognition Composition Law as the d'Alembert equation F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y).
proof idea
One-line wrapper that applies CostMorphism.comp g f. The underlying CostAlgebra.comp constructs the composite map and reuses the multiplicativity proof already established for J-automorphisms.
why it matters
This definition supplies the composition operation required by category_certificate, which certifies that RecAlg forms a category with associative composition and neutral identities. It is invoked directly by recAlg_comp_assoc, recAlg_id_left, and layerSysPlus_comp. In the Recognition framework it closes the algebraic layer that supports the forcing chain from the Recognition Composition Law through J-uniqueness (T5) to the eight-tick octave and D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.