costFamily
plain-language theorem explainer
The costFamily definition supplies the explicit one-parameter family F_κ(x) = ½(x^κ + x^{-κ}) - 1 on the reals. Algebraists building the CostAlg category cite this as the generator for objects before the κ = 1 specialization. The definition is a direct algebraic transcription of the continuous solutions to the calibrated d'Alembert law.
Claim. The one-parameter cost family is the map given by $F_κ(x) = ½(x^κ + x^{-κ}) - 1$ for real κ and x.
background
In the RecognitionCategory module the cost algebra is organized around families satisfying the Recognition Composition Law. The J-cost recovered at κ = 1 is the function J(x) = (x + x^{-1})/2 - 1 that appears as the uniqueness condition T5 in the forcing chain. Upstream results define the cost of a recognition event as this J-cost (ObserverForcing.cost) and the cost induced by a multiplicative recognizer as derivedCost on positive ratios (MultiplicativeRecognizerL4.cost).
proof idea
The definition is a direct algebraic expression with no lemmas applied: costFamily κ x expands immediately to (x^κ + x^{-κ})/2 - 1.
why it matters
This definition is the base generator for the CostAlgObjKappa and CostAlgPlusObj structures, which support morphisms via power maps that scale the parameter (CostAlgHomKappa). It supplies the general continuous family to the d'Alembert law before the κ = 1 case recovers J-cost and links to the eight-tick octave. Downstream theorems such as costFamily_one_eq_J and costFamily_comp_powerMap derive the required algebraic properties from it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.