CostAlgPlusHom
plain-language theorem explainer
Morphisms between CostAlg⁺ objects are positive real exponents α satisfying the scaling relation α κ₂ = κ₁ on the cost parameters. Category theorists and Recognition Science formalizers working with order-preserving cost maps would cite this structure. It is introduced as a plain record type whose extensionality lemma follows by case analysis and simplification.
Claim. A morphism from object $C_1$ to object $C_2$ consists of a real number $α > 0$ such that $α · κ_2 = κ_1$, where each object $C_i$ is a positive real parameter $κ_i > 0$ equipped with the cost map costFamily($κ_i$).
background
Objects of CostAlg⁺ are structures CostAlgPlusObj carrying a positive real parameter κ together with the cost map costFamily κ; the negative branch is excluded to preserve order. The module RecognitionCategory assembles a category whose morphisms are exactly the positive exponents satisfying the displayed intertwining relation on κ. Upstream results from CostAlgebra supply the J-automorphism notions of multiplicativity and cost preservation that justify the powerMap implementation of the induced map on positive reals.
proof idea
The structure is a direct record definition of the three fields. The accompanying extensionality theorem proceeds by cases on the two morphisms and the equality of α values, followed by simplification.
why it matters
The structure supplies the hom-sets of the category CostAlg⁺ and thereby realizes the paper's order-preserving morphism classification for positive cost families. It is placed immediately before the initial object costAlgPlusInitial (κ = 1) and the identity and composition operations that complete the category. No downstream uses are recorded in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.