cost_algebra_unique
plain-language theorem explainer
The theorem shows that any cost function on positive reals obeying the Recognition Composition Law, normalization at the identity, reciprocity under inversion, and the calibration condition that the second derivative of cost composed with the exponential equals 1 at zero must equal the canonical J. Researchers deriving physical constants from the Recognition Science forcing chain cite this as the uniqueness step T5. The proof extracts the algebraic properties directly from the input structure and applies the washburn_uniqueness lemma under the
Claim. Let $f: (0,∞) → ℝ$ be a function satisfying the Recognition Composition Law $f(xy) + f(x/y) = 2f(x)f(y) + 2f(x) + 2f(y)$ for $x,y > 0$, normalized by $f(1) = 0$, reciprocal so that $f(x) = f(1/x)$, continuous on $(0,∞)$, and calibrated by the condition that the second derivative at 0 of $t ↦ f(e^t)$ equals 1. Assume the regularity hypotheses that continuous solutions to the associated d'Alembert equation are smooth and satisfy the ODE $H'' = H$. Then $f(x) = J(x)$ for all $x > 0$, where $J(x) = (x + x^{-1})/2 - 1$.
background
CostAlgebraData packages a cost function on positive reals together with the Recognition Composition Law (RCL), normalization at 1, and reciprocity under inversion. The shifted function H(x) = J(x) + 1 converts the RCL into the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y). The canonical J is the unique solution normalized so that J(1) = 0 and J''(1) = 1, equivalently written as cosh(log x) - 1. The module imports the Aczél smoothness result and the d'Alembert-to-ODE derivation, which supply the regularity hypotheses appearing in the signature.
proof idea
The tactic proof first constructs IsReciprocalCost, IsNormalized, SatisfiesCompositionLaw, and IsCalibrated by projecting the corresponding fields of the CostAlgebraData structure and the calibration hypothesis. It then applies the washburn_uniqueness lemma to these four properties together with the supplied continuity and regularity hypotheses, yielding the identification with J.
why it matters
This is the clean statement of T5 J-uniqueness in the forcing chain T0–T8. It establishes that the cost algebra is rigidly determined by the RCL and the single calibration condition, which is the algebraic prerequisite for forcing phi as the self-similar fixed point, the eight-tick octave, and D = 3. The result closes the uniqueness step before the mass formula and the derivation of constants such as G = phi^5 / pi.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.