unique_cost_on_pos_from_rcl
plain-language theorem explainer
Any function F from reals to reals obeying the reciprocal cost property, unit normalization at 1, the full RCL composition law, calibration, and continuity on the positive reals, together with the listed d'Alembert regularity hypotheses on the shifted H, must coincide with Jcost on (0, ∞). Recognition Science researchers working on the T5 step of the forcing chain cite this as the central unconditional uniqueness statement. The argument is a one-line wrapper invoking washburn_uniqueness after packaging the hypotheses.
Claim. Let $F : ℝ → ℝ$ satisfy the reciprocal cost property, the normalization $F(1) = 0$, the composition law $F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y)$, the calibration condition, and be continuous on $(0, ∞)$. Assume the d'Alembert continuous-implies-smooth, to-ODE, and regularity hypotheses hold for the shifted $H(x) = F(x) + 1$. Then $F(x) = J(x)$ for all $x > 0$, where $J(x) = (x + x^{-1})/2 - 1$.
background
The CostUniqueness module consolidates convexity, calibration, and functional equation results to obtain uniqueness for the cost functional. The J-cost is defined by $J(x) = (x-1)^2/(2x)$, equivalently $(x + x^{-1})/2 - 1$, and satisfies symmetry $J(x) = J(x^{-1})$, unit normalization $J(1) = 0$, and strict convexity on $(0, ∞)$. The shifted $H(x) = J(x) + 1$ converts the RCL into the d'Alembert equation $H(xy) + H(x/y) = 2 H(x) H(y)$. Upstream lemmas supply Jcost_symm for symmetry, Jcost_unit0 for normalization, Jcost_strictConvexOn_pos for convexity, and the dAlembert hypotheses that encode Aczél's theorem: continuous solutions are smooth and obey the ODE $H'' = H$.
proof idea
The proof is a one-line wrapper that applies washburn_uniqueness from FunctionalEquation, passing the reciprocal, normalization, composition, calibration, continuity, and all five d'Alembert regularity hypotheses directly to obtain $F x = Jcost x$ for $x > 0$.
why it matters
This is the main unconditional T5 uniqueness statement on the RCL surface, realizing J-uniqueness in the forcing chain (T5) where J is the unique self-similar fixed point. It consolidates results from Cost, Convexity, and FunctionalEquation modules and supplies the core uniqueness needed for downstream claims such as T5_uniqueness_complete. The declaration closes the axiom-free path from the composition law and calibration to equality with Jcost, directly supporting the eight-tick octave and D = 3 steps that follow from T5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.