CostAlgHomKappa
plain-language theorem explainer
Morphisms between CostAlg objects are given by a nonzero real α such that α κ₂ equals plus or minus κ₁. Recognition Science algebraists cite this structure when assembling the paper-facing category of κ-parameter families. The definition is a direct record of the scalar, its nonzeroness, and the sign choice in the intertwining condition.
Claim. A morphism from object $C_1$ to $C_2$ consists of a real number $α ≠ 0$ such that $α κ_2 = κ_1$ or $α κ_2 = -κ_1$, where each $C_i$ carries a positive parameter $κ_i > 0$.
background
Objects of the CostAlg category are structures CostAlgObjKappa carrying a positive real parameter κ together with the cost function costFamily κ. The module assembles these into a category whose morphisms realize the intertwining condition on the parameters. Upstream results from CostAlgebra establish multiplicativity and cost preservation for the underlying J-automorphisms, while costAlgKappaInitial supplies the canonical object with κ = 1.
proof idea
The declaration is a structure definition recording the three fields α, α_ne_zero, and intertwines. The accompanying extensionality theorem proceeds by cases on the two records followed by simp. Companion definitions for map, id, and comp are built directly from these fields, with comp handling the four sign combinations by case analysis on the two intertwines hypotheses.
why it matters
This structure supplies the hom-sets for the full paper-facing CostAlg category above the J-automorphism layer. It enables the initial object with κ = 1 and supports cost preservation via the costFamily lemmas. No downstream uses appear, indicating a foundational interface role in the algebra layer of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.