recAlg_comp
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove associativity of the defined composition.
- Does not establish that identities act as units.
- Does not define the objects or the cost function itself.
- Does not extend to functors or natural transformations between categories.
formal statement (Lean)
65def recAlg_comp {C₁ C₂ C₃ : RecAlgObj}
66 (g : RecAlgHom C₂ C₃) (f : RecAlgHom C₁ C₂) : RecAlgHom C₁ C₃ :=
proof body
Definition body.
67 CostMorphism.comp g f
68
69/-- **PROVED: Composition is associative (on underlying maps).** -/