law_of_logic_forces_jcost
Reciprocal-symmetric cost has one solution: J(x) = ½(x + x⁻¹) − 1.
plain-language theorem explainer
Any reciprocal, normalized, calibrated, continuous cost on the positive reals that obeys the Recognition Composition Law equals the canonical J-cost J(x)=(x+1/x)/2-1. Cite this for T5 uniqueness (Law of Logic cost theorem) and for any bridge that derives the RCL from symplectic or ledger structure. The proof converts the RCL into d'Alembert's equation on the log-coordinate shift H=G+1, then invokes Aczél classification with H''(0)=1 to force H=cosh.
Claim. Let $F:\mathbb{R}\to\mathbb{R}$ be continuous on $(0,\infty)$, reciprocal ($F(x)=F(1/x)$ for $x>0$), normalized ($F(1)=0$), calibrated so $G''(0)=1$ where $G(t)=F(e^t)$, and satisfying the Recognition Composition Law $F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(y)$ for all $x,y>0$. Then for every $x>0$, $F(x)=J(x)$, where $J(x)=\frac{x+x^{-1}}{2}-1$.
background
This module supplies the functional-equation lemmas behind T5 cost uniqueness. A reciprocal cost obeys $F(x)=F(1/x)$ on $(0,\infty)$. Normalization is $F(1)=0$. Calibration is the unit log-curvature condition $G''(0)=1$ with $G(t)=F(e^t)$. The Recognition Composition Law (RCL) is $F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(y)$.
The shifted objects $G(t)=F(e^t)$ and $H=G+1$ convert the RCL into a d'Alembert equation. Under $H$, the identity becomes $H(t+u)+H(t-u)=2H(t)H(u)$, and the canonical target is $H=\cosh$, so $J(x)=\cosh(\log x)-1$. The typeclass AczelSmoothnessPackage packages the global Aczél regularity needed to upgrade continuous d'Alembert solutions to smooth ones without exposing extra hypotheses to the caller.
Upstream, $H$ is defined so that the RCL becomes the standard d'Alembert form, and $J$ itself is the RS recognition cost $(x+x^{-1})/2-1$.
proof idea
Fix $x>0$. Reciprocity gives evenness of $G$. The composition-law hypothesis is rewritten as a cosh-addition identity, then pushed to a direct addition law on $G$. Continuity of $F$ on $(0,\infty)$ yields continuity of $G$ and of $H=G+1$. Normalization forces $G(0)=0$ and $H(0)=1$. Algebra on the direct addition law produces the d'Alembert equation for $H$. Calibration transfers to $H''(0)=1$ because differentiating a constant shift does not change derivatives. Aczél's classification (dAlembert_cosh_solution_aczel) then forces $H=\cosh$, hence $G=\cosh-1$. Evaluating at $\log x$ and unwinding $G$ recovers $F(x)=J(x)$.
why it matters
This is the T5 J-uniqueness landmark in the forcing chain: the unique continuous reciprocal cost obeying the RCL with unit log curvature is $J(x)=\cosh(\log x)-1$. Downstream, the symplectic-action bridge cites it to conclude that any cost whose composition law comes from the area-preserving ledger group must be $J$ (jcost_forced_by_symplectic_action). The Aczél-closure wrapper and the non-vacuity witness that $J$ itself has unit log curvature both rest on this theorem. Foundation results on discrete RCL uniqueness and ledger comparison to composition cost also consume it. The module note after the proof records that normalization is in fact forced by RCL plus calibration, so two of the classical hypotheses are redundant; the published uniqueness paper's silent nonnegativity assumption is likewise a conclusion rather than an input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.