costFamily_unit
plain-language theorem explainer
The cost family F_κ(x) evaluates to zero at the unit element x=1 for any real parameter κ. Researchers working on the broad cost category in Recognition Science would cite this normalization property when fixing the zero point of the cost function. The proof is a direct algebraic reduction after unfolding the definition.
Claim. For every real number κ, F_κ(1) = 0 where F_κ(x) = (x^κ + x^{-κ})/2 - 1.
background
The cost family is the explicit one-parameter family F_κ(x) = ½(x^κ + x^{-κ}) - 1 on positive reals, providing the full continuous solution family to the calibrated d'Alembert law before imposing κ = 1. When κ = 1 this recovers the J-cost. The local setting is the RecognitionCategory module, which equips the algebra with cost structures compatible with the phi-ring and octave algebra imports.
proof idea
One-line wrapper that unfolds the costFamily definition and applies simp to reduce the expression at x=1 to zero.
why it matters
This normalization anchors the zero of the cost function at the multiplicative identity, supporting consistent composition in the recognition category. It aligns with the J-uniqueness step (T5) in the forcing chain where J(x) = (x + x^{-1})/2 - 1. The result ensures the family starts at zero before specialization to the J-cost case.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.