CostMorphism
plain-language theorem explainer
The structure for cost algebra morphisms captures positive multiplicative maps between cost algebras that preserve the cost function J. Category theorists constructing the recognition algebra category cite this when defining homomorphisms between objects equipped with RCL-satisfying costs. It is introduced directly as a structure whose four fields encode the map, positivity, multiplicativity, and cost preservation, with no separate proof obligations.
Claim. A morphism from cost algebra $C_1$ to $C_2$ is a function $f : (0,∞) → (0,∞)$ such that $f(xy) = f(x)f(y)$ for all $x,y > 0$ and $J_2(f(x)) = J_1(x)$ for all $x > 0$, where $J_1$ and $J_2$ denote the cost functions of $C_1$ and $C_2$.
background
CostAlgebraData packages the positive reals under multiplication together with a cost function J that satisfies the Recognition Composition Law, vanishes at the identity 1, and is invariant under reciprocals. This supplies the objects for the algebraic layer of Recognition Science. The present structure then defines the arrows between such objects by requiring the map to be positive, multiplicative, and to intertwine the two cost functions.
proof idea
The declaration is a structure definition whose fields are stated directly. The identity morphism is obtained by taking the identity map on the reals; positivity, multiplicativity, and cost preservation hold by reflexivity. Composition is realized by ordinary function composition, with each required property obtained by applying the corresponding property of the second morphism to the image under the first.
why it matters
This supplies the morphisms for the recognition algebra category, where they are re-exported as RecAlgHom and used to prove that composition is associative and that identities act neutrally. It therefore closes the algebraic foundation needed for the J-uniqueness step and the subsequent forcing chain that derives spatial dimension three and the eight-tick octave from the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.