washburn_uniqueness_aczel
plain-language theorem explainer
washburn_uniqueness_aczel shows that any continuous reciprocal cost F on positive reals obeying the recognition composition law, normalization at unity, and unit log-curvature calibration must equal the J-cost J(x) = (x + x^{-1})/2 - 1. Recognition Science workers cite it to close uniqueness of the cost function in the T5 step of the forcing chain without extra regularity parameters. The tactic proof converts the multiplicative law to the d'Alembert equation via exponential substitution and G/H transforms, then invokes dAlembert_cosh_solution_
Claim. Let $F: (0,∞) → ℝ$ satisfy $F(x)=F(x^{-1})$ for $x>0$, $F(1)=0$, the recognition composition law $F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(y)$ for $x,y>0$, the calibration condition that the second derivative of $t ↦ F(e^t)$ at $t=0$ equals 1, and continuity on $(0,∞)$. Then $F(x)=½(x + x^{-1}) - 1$ for all $x>0$.
background
The recognition composition law (RCL) encodes route independence for comparisons of positive ratios and takes the explicit form $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$. The J-cost is the explicit solution $J(x) = ½(x + x^{-1}) - 1$, equivalently $J(e^t) = cosh t - 1$. The shifted transform $H_F(t) := F(e^t) + 1$ converts the RCL into the d'Alembert equation $H(t+u) + H(t-u) = 2H(t)H(u)$. This module supplies the Aczél-dependent closure theorems that the core FunctionalEquation module deliberately avoids; upstream results establish the equivalence between the multiplicative RCL and the additive cosh-add identity on the logarithmically transformed function.
proof idea
The tactic proof extracts reciprocity symmetry, applies composition_law_equiv_coshAdd to obtain CoshAddIdentity, defines the transformed functions Gf(t) := F(e^t) and Hf(t) := Gf(t) + 1, verifies Hf(0) = 1 from normalization, obtains continuity of both transforms, derives the direct d'Alembert equation for Hf, computes the second derivative of Hf at 0 from the calibration hypothesis, invokes dAlembert_cosh_solution_aczel to conclude Hf(t) = cosh t, and back-substitutes to recover F(x) = cosh(log x) - 1 = J(x).
why it matters
This is the clean Aczél form of the J-uniqueness theorem (T5 in the T0-T8 forcing chain). It is invoked directly by cost_algebra_unique_aczel to obtain uniqueness of the canonical cost algebra without regularity hypotheses. Downstream it supports J_is_unique_cost_under_logic and RCL_is_unique_functional_form_of_logic, which embed the cost function into the Aristotelian logic axioms and thereby force the physical constants (phi, alpha band, D=3) in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.