composition_logCurvature_forces_jcost
plain-language theorem explainer
Composition law plus unit log-curvature of the log-reparametrized cost force F = J on the positives, with normalization and continuity derived rather than assumed. Cite this for the two-premise T5 uniqueness route (or the unconditional wrapper in FunctionalEquationStrict). The proof reduces RCL to d'Alembert for H_F, upgrades continuity to C^∞ via the Aczél package, pins the second derivative at 0 to 1, and identifies H_F with cosh.
Claim. Assume an Aczél smoothness package. Let $F:\mathbb{R}\to\mathbb{R}$ satisfy the Recognition Composition Law $F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(y)$ for all $x,y>0$, and suppose the log-reparametrization $H_F(t)=F(e^t)+1$ has unit log-curvature $\kappa(H_F)=1$ (limit of $2(H_F(t)-1)/t^2$ as $t\to 0$ along the punctured neighborhood). Then for every $x>0$, $F(x)=J(x):=(x+x^{-1})/2-1$.
background
This module supplies functional-equation lemmas for the T5 cost-uniqueness argument. The Recognition Composition Law (RCL) is the two-variable identity $F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(y)$ on positives; it is the algebraic skeleton of the cost theorem.
The log reparametrization is $G_F(t)=F(e^t)$ and $H_F(t)=G_F(t)+1$. Under $H$, RCL becomes the classical d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$. Log curvature is the paper's calibration $\kappa(H)=\lim_{t\to 0} 2(H(t)-1)/t^2$ on the punctured filter at 0 (the full-filter reading is unsatisfiable at $\kappa=1$). The target cost is $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$.
Upstream, composition_law_equiv_coshAdd converts RCL into a cosh-add identity for $G_F$, and aczel_dAlembert_smooth upgrades continuous d'Alembert solutions to $C^\infty$ once an AczelSmoothnessPackage instance is present.
proof idea
First, unit log-curvature plus RCL yields normalization ($F(1)=0$), so $H_F(0)=1$. Convert RCL to the cosh-add identity for $G_F$, then rewrite it as the d'Alembert equation for $H_F$. Continuity of $H_F$ follows from the log-curvature hypothesis; the Aczél package then gives $C^\infty$.
Evenness of d'Alembert solutions forces the first derivative at 0 to vanish. The curvature hypothesis pins the second derivative at 0 to 1. The calibrated continuous d'Alembert solution is therefore $H_F(t)=\cosh t$. Transporting back via $G_F(\log x)=\cosh(\log x)-1$ and the known identity for $J$ gives $F(x)=J(x)$ on $x>0$.
why it matters
This is the two-premise form of the T5 J-uniqueness theorem: RCL plus unit log-curvature alone force $F=J$, with normalization, nonnegativity, and continuity as conclusions rather than inputs. It sits on the forcing-chain landmark T5 (J-uniqueness via $J(x)=(x+x^{-1})/2-1=\cosh(\log x)-1$) and the Recognition Composition Law.
Downstream, composition_logCurvature_forces_jcost_unconditional re-exports the same statement without the package instance argument (cite that wrapper in applications). law_of_logic_forces_jcost_of_log_calibration uses the same route to drop an explicit continuity premise from a T5 variant once limit-form log calibration is present. Compared with fuller law-of-logic statements that assume reciprocity, normalization, and calibration up front, this declaration isolates the minimal analytic input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.