RecAlgHom
plain-language theorem explainer
RecAlgHom aliases morphisms in the recognition algebra category to cost morphisms between cost algebra data bundles. Category theorists in Recognition Science cite it when assembling the full category structure for RecAlg. The declaration is a direct one-line alias to CostMorphism, inheriting its multiplicative and positivity-preserving map without further conditions.
Claim. Let $C_1$ and $C_2$ be cost algebra data bundles. A morphism from $C_1$ to $C_2$ in the recognition algebra category is a cost morphism: a map $f : (0,∞) → (0,∞)$ that is multiplicative ($f(xy) = f(x)f(y)$) and positivity-preserving.
background
Objects in the recognition algebra category are cost algebra data bundles, which package a cost function (typically J) together with algebraic operations on positive reals. Morphisms are supplied by the CostMorphism structure, whose fields require a map from ℝ to ℝ that sends positives to positives and satisfies multiplicativity. The module Algebra.RecognitionCategory assembles these into a category RecAlg whose laws are checked downstream.
proof idea
One-line abbreviation that directly aliases CostMorphism C₁ C₂, inheriting the map, positivity, and multiplicativity fields without additional lemmas or tactics.
why it matters
RecAlgHom supplies the morphism type used in the category certificate theorem, which confirms associative composition, neutral identities, and the existence of an initial object. It also appears in LayerSysPlusHom and initial_morphism_exists, linking the algebraic layer to the forcing chain (T0-T8) and the recognition composition law. The abbreviation closes the basic categorical scaffolding before domain-specific instances (qualia, ethics) are attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.