law_of_logic_forces_jcost_with_regularization
plain-language theorem explainer
Under reciprocity, normalization, the Recognition Composition Law, unit second-derivative calibration, continuity on (0,∞), and Aczél regularity on the shifted log-reparametrization, any cost F equals the canonical J-cost J(x)=(x+1/x)/2−1. T5 uniqueness proofs and cost-algebra uniqueness cite this as the main functional-equation engine. The argument reduces RCL to d'Alembert on H=G+1, then forces H=cosh via continuous uniqueness with H''(0)=1.
Claim. Let $F:(0,\infty)\to\mathbb{R}$ satisfy $F(x)=F(1/x)$, $F(1)=0$, the composition law $F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(y)$ for $x,y>0$, calibration $G''(0)=1$ where $G(t)=F(e^t)$, continuity on $(0,\infty)$, and the listed continuous d'Alembert / ODE regularity hypotheses on $H=G+1$. Then for every $x>0$, $F(x)=J(x)$ with $J(x)=\frac{x+x^{-1}}{2}-1$.
background
This module supplies functional-equation helpers for the T5 cost-uniqueness argument. A reciprocal cost obeys $F(x)=F(1/x)$ on $(0,\infty)$; normalized means $F(1)=0$. The Recognition Composition Law (RCL) is $F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(y)$. Calibration is the second-derivative condition $G''(0)=1$ for the log reparametrization $G(t)=F(e^t)$, equivalently the limit form $\lim_{t\to 0}2F(e^t)/t^2=1$.
The shift $H=G+1$ converts RCL into the classical d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$. Upstream, the same shift on the canonical cost reads $H(x)=J(x)+1=\frac12(x+x^{-1})$, under which RCL becomes that multiplicative d'Alembert form. Continuity of $F$ on $(0,\infty)$ lifts to continuity of $G$ and $H$ via the exponential chart.
The five named regularity hypotheses package the Aczél-theory bridge: continuous d'Alembert solutions are smooth, reduce to an ODE, and admit a linear regularity bootstrap so that the calibrated continuous solutions are exactly $\cosh$.
proof idea
Tactic proof following the T5 uniqueness skeleton. Reciprocity is rewritten as pointwise symmetry; RCL is converted to CoshAddIdentity via composition_law_equiv_coshAdd. Define $G_F(t)=F(e^t)$ and $H_F=G_F+1$. Evenness of $G_F$ comes from G_even_of_reciprocal_symmetry; $G_F(0)=0$ from G_zero_of_unit and normalization, so $H_F(0)=1$. Continuity of $F$ on $(0,\infty)$ plus continuous $\exp$ yields continuous $G_F$ and $H_F$.
CoshAddIdentity_implies_DirectCoshAdd plus algebra produces the d'Alembert identity for $H_F$. Calibration transfers: $\mathrm{deriv}^2 G_F(0)=1$ implies $\mathrm{deriv}^2 H_F(0)=1$ because adding a constant does not change derivatives. dAlembert_cosh_solution with the five regularity hypotheses forces $H_F=\cosh$. Unshifting gives $G_F=\cosh-1$. Comparing to Jcost_G_eq_cosh_sub_one and substituting $t=\log x$ recovers $F(x)=J(x)$.
why it matters
This is the reformulated main result (Theorem 1.1) of Washburn–Zlatanović on uniqueness of the canonical reciprocal cost, and the concrete engine behind T5 J-uniqueness in the forcing chain: $J(x)=(x+x^{-1})/2-1=\cosh(\log x)-1$. Downstream, cost_algebra_unique quotes it to conclude that any cost algebra with the same axioms and calibration has cost equal to $J$ (explicitly labeled T5). unique_cost_on_pos_from_rcl is the axiom-free IM-facing T5 surface that packages the same hypotheses. primitive_to_uniqueness_of_kernel routes the primitive cost hypotheses through an explicit Aczél regularity kernel to the same conclusion.
Within Recognition Science the result pins the cost functional that feeds the rest of the chain (φ as self-similar fixed point, eight-tick octave, $D=3$). The regularity package is the only remaining seam: once those Aczél hypotheses are discharged or replaced by a weaker kernel, T5 becomes fully unconditional on the RCL surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.