costFamily
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not restrict κ to positive values.
- Does not restrict the domain to positive reals.
- Does not prove any functional equations satisfied by the family.
- Does not reference phi, the forcing chain steps T5-T8, or physical constants.
formal statement (Lean)
113noncomputable def costFamily (κ : ℝ) (x : ℝ) : ℝ :=
proof body
Definition body.
114 (x ^ κ + x ^ (-κ)) / 2 - 1
115
116/-- The canonical `κ = 1` family recovers the J-cost on positive reals. -/