composition_logCurvature_forces_jcost_unconditional
plain-language theorem explainer
Any positive-real cost F obeying the Recognition Composition Law and unit log curvature of its shift H equals the canonical J-cost J(x)=(x+x^{-1})/2-1. Cite this form rather than the instance-bearing sibling: the Aczel smoothness package is already in scope, so only the two working premises remain. The proof is a one-line application of the conditional two-premise theorem.
Claim. 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)$ on positives, and suppose the shifted map $H_F:=F+1$ has unit log curvature $\kappa(H_F)=\lim_{t\to 0,\,t\neq 0} 2(H_F(t)-1)/t^2=1$. Then $F(x)=J(x):=(x+x^{-1})/2-1$ for every $x>0$.
background
Recognition Science fixes the cost of a positive ratio by a functional equation (the RCL) rather than by an ansatz. The canonical solution is $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$. The shifted map $H=J+1=\frac12(x+x^{-1})$ converts RCL into d'Alembert's equation $H(xy)+H(x/y)=2H(x)H(y)$.
Log curvature is the paper's second-order calibration $\kappa(F)=\lim_{t\to 0} 2F(e^t)/t^2$, stated on the punctured neighbourhood of $0$. The puncture is essential: Lean's total division makes the full-filter reading force $\kappa=0$, so the calibrated value $\kappa=1$ would be unsatisfiable. HasLogCurvature carries that punctured filter and a non-vacuity witness for $J$.
This module is the strict surface of T5: it imports the Aczel smoothness package so instance arguments disappear, and it records that continuity, reciprocity, and normalization are conclusions rather than inputs once composition and unit log curvature are assumed.
proof idea
One-line term wrapper. The body is exactly the application of composition_logCurvature_forces_jcost to $F$ and the two hypotheses. That upstream theorem, under the now-available AczelSmoothnessPackage instance, first derives normalization from log curvature, then runs the Aczel/d'Alembert uniqueness argument to conclude $F=J$ on $(0,\infty)$. No extra tactics or local lemmas appear here.
why it matters
This is the citation form of the two-premise cost theorem (T5 J-uniqueness). The doc-comment is explicit: the sibling in FunctionalEquation still carries an AczelSmoothnessPackage instance argument because that module does not import the Aczel builder; this module does, so callers should quote the unconditional statement.
In the forcing chain, T5 pins $J(x)=\cosh(\log x)-1$ as the unique cost compatible with RCL plus unit curvature. Downstream structure (phi as self-similar fixed point, the eight-tick octave, $D=3$) sits on that uniqueness. The module history notes an earlier vacuous full-filter reading of curvature; the punctured predicate and the witness jcost_hasLogCurvature_one close that gap, so the trade of continuity for limit-form calibration now has content.
No used_by edges are recorded yet; the declaration is kept as the stable external API for the two-premise result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.