uniqueness_specification
plain-language theorem explainer
Any cost functional F obeying the three primitive axioms plus continuity and strict convexity on positive reals must coincide with the canonical J. Recognition Science researchers cite this as the uniqueness half of T5. The proof derives symmetry, unit normalization, and the cosh-additive identity from the axioms then invokes T5_uniqueness_complete with the Aczél regularity hypotheses.
Claim. Let $F:(0,∞)→ℝ$ satisfy the three cost axioms (normalization $F(1)=0$, the recognition composition law $F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(y)$, and calibration with second logarithmic derivative at zero equal to one), be continuous and strictly convex on $(0,∞)$, and obey the Aczél regularity hypotheses ensuring the associated d'Alembert function $H=F∘exp+1$ is smooth and satisfies the ODE $H''=H$. Then $F(x)=J(x):=(x+x^{-1})/2-1$ for all $x>0$.
background
The CostAxioms module formalizes the three primitive axioms at level 0 of the hierarchy: Normalization requires $F(1)=0$, the Recognition Composition Law (RCL) encodes multiplicative consistency via $F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(y)$, and Calibration fixes the second derivative of $F∘exp$ at zero to one. These axioms describe the cost structure of configurations from which logical coherence emerges, with $J(x)=(x+x^{-1})/2-1$ as the canonical solution at level 1. The module doc states that the axioms are more primitive than logic because contradiction carries high cost while consistency carries low cost.
proof idea
This is a term-mode wrapper. It obtains symmetry $F(x)=F(x^{-1})$ from Composition and Normalization, unit normalization $F(1)=0$, calibration of the second derivative, and the CoshAddIdentity from Composition. It then applies CostUniqueness.T5_uniqueness_complete with the supplied regularity hypotheses (dAlembert_continuous_implies_smooth_hypothesis, dAlembert_to_ODE_hypothesis, and the ODE bootstrap) to conclude $F=J$.
why it matters
This is the central uniqueness theorem of Recognition Science, closing the uniqueness half of T5 J-uniqueness in the forcing chain (T0 to T8). It enables the Law of Existence and downstream derivations such as the phi-ladder and eight-tick octave. The doc-comment identifies it as the result that forces $J(x)=cosh(log x)-1$ via the d'Alembert equation and Aczél regularity. No open questions remain; the theorem is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.