T5_uniqueness_complete
plain-language theorem explainer
Any cost functional F on positive reals satisfying reciprocity under inversion, normalization at 1, strict convexity on (0,∞), calibration of the second derivative of F∘exp at 0, continuity, and the cosh-add functional identity must equal the J-cost. Recognition Science researchers cite this as the complete T5 uniqueness result. The proof reduces to logarithmic coordinates, converts the identity to the d'Alembert equation for the shifted H, and invokes the cosh solution under the regularity hypotheses.
Claim. Let $F : (0,∞) → ℝ$ be continuous and strictly convex, with $F(x) = F(x^{-1})$ for $x>0$, $F(1)=0$, second derivative of $F∘exp$ at 0 equal to 1, and satisfying the cosh-add identity $G(t+u)+G(t-u)=2G(t)G(u)+2(G(t)+G(u))$ where $G(t)=F(e^t)$, together with the regularity hypotheses on the shifted $H=G+1$. Then $F(x)=J(x)$ for all $x>0$, where $J(x)=(x+x^{-1})/2-1$.
background
The J-cost is the function $J(x)=(x+x^{-1})/2-1$, equivalently $G(t)=J(e^t)=cosh(t)-1$ in log coordinates. Its shift $H(t)=G(t)+1=cosh(t)$ satisfies the d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$. The module states that any cost functional satisfying symmetry, unit normalization, strict convexity, and calibration must equal Jcost on ℝ₊. Upstream, CoshAddIdentity is the cosh-type functional identity for G_F, while dAlembert_cosh_solution supplies the cosh uniqueness for solutions to the d'Alembert equation under the listed regularity hypotheses.
proof idea
The proof defines Gf as F∘exp, verifies evenness from symmetry, Gf(0)=0 from normalization, and continuity. It applies CoshAddIdentity_implies_DirectCoshAdd to obtain the direct cosh-add identity on Gf. Shifting to Hf=Gf+1 produces the d'Alembert equation with Hf(0)=1 and second derivative 1 at 0. The regularity hypotheses then permit dAlembert_cosh_solution to conclude Hf(t)=cosh(t), hence Gf(t)=cosh(t)-1. Substituting t=log x recovers F(x)=Jcost(x) via the log identity for Jcost.
why it matters
This is the full T5 uniqueness theorem, feeding directly into unique_cost_on_pos (the main statement on ℝ₊) and washburn_uniqueness (the reformulated main result). It supplies the central uniqueness cited in uniqueness_specification as the proof that admissible costs equal J. In the forcing chain it realizes T5 J-uniqueness, which forces the self-similar fixed point phi and the eight-tick octave. The remaining open question is full unification with the information aggregator in H_UniquenessVerified.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.