CostAlgObjKappa
plain-language theorem explainer
Objects in the CostAlg category are positive real parameters κ equipped with the cost function F_κ(x) = (x^κ + x^{-κ})/2 - 1. Algebraists building the full cost category beyond the fixed J-cost case cite this structure when assembling objects for morphism definitions. The definition is a one-line wrapper around costFamily with an explicit positivity constraint on κ.
Claim. An object of the CostAlg category consists of a real parameter κ > 0 together with the associated cost function F_κ(x) = ½(x^κ + x^{-κ}) - 1.
background
CostAlgObjKappa supplies the objects of the paper-facing CostAlg category in RecognitionCategory. Each object is indexed by κ > 0 and carries the cost map given by costFamily, the explicit one-parameter family F_κ(x) = ½(x^κ + x^{-κ}) - 1 that solves the calibrated d'Alembert law on positive reals before κ is fixed to 1. This generalizes the J-cost used in ObserverForcing.cost and the derivedCost appearing in MultiplicativeRecognizerL4.cost.
proof idea
The definition is a one-line wrapper that applies costFamily to the κ field of the structure.
why it matters
This definition supplies the objects required by CostAlgHomKappa, whose morphisms are power maps x ↦ x^α satisfying α κ₂ = ± κ₁. It extends the recognition cost framework from the κ = 1 case to the full continuous family, supporting the algebraic treatment of recognition events before the eight-tick octave and D = 3 constraints are imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.