logCurvature_forces_normalized
plain-language theorem explainer
Composition law plus unit log-curvature force F(1)=0. Anyone proving T5 cost uniqueness from only RCL and κ=1 cites this: normalization is a conclusion, not an assumption. Proof is contradiction: non-normalization collapses F to the constant −1, whose curvature quotient is negative near 0 and cannot tend to 1.
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)$ for all $x,y>0$, and suppose the log-curvature of $H_F(t):=F(e^t)+1$ equals $1$, i.e. $\lim_{t\to 0,\,t\neq 0} 2(H_F(t)-1)/t^2=1$. Then $F$ is normalized: $F(1)=0$.
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 $J$.
Reparametrization uses $G_F(t)=F(e^t)$ and the shift $H_F(t)=G_F(t)+1$. Log curvature is the paper's calibration $\kappa(F)=\lim_{t\to 0} 2(H_F(t)-1)/t^2$, stated on the punctured filter nhdsWithin 0 {0}ᶜ. The puncture is essential: Lean's total division sends the quotient to $0$ at $t=0$, so the full-neighbourhood reading would force $\kappa=0$ and make unit curvature unsatisfiable.
Normalization means simply $F(1)=0$. Downstream T5 arguments prefer to derive it from RCL and $\kappa=1$ rather than assume it.
proof idea
Contradiction on $F(1)\neq 0$. Specialize RCL at $y=1$: after simplifying $xy=x/y=x$ one obtains the quadratic relation $F(1)\cdot(F(x)+1)=0$ for every $x>0$. The left factor is nonzero by hypothesis, so $F\equiv -1$ on positives.
Under that constant, $H_F\equiv 0$. Unit log-curvature supplies an eventually-true inequality $1/2 < 2(H_F(t)-1)/t^2$ on a punctured neighbourhood of $0$. Pick such a $t\neq 0$: the right-hand side becomes $2(0-1)/t^2=-2/t^2<0$, contradicting the lower bound. Hence $F(1)=0$.
why it matters
Feeds the two-premise cost theorem composition_logCurvature_forces_jcost, whose doc-comment states: composition law and unit log curvature force $F=J$ on the positives, with "Normalization, nonnegativity, and continuity all conclusions rather than hypotheses." That parent is the lean form of T5 (J-uniqueness) under minimal analytic input.
In the forcing chain, T5 identifies $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$) as the unique cost. Deriving normalization here means the RCL-plus-calibration package is self-calibrating: one does not smuggle $F(1)=0$ in by hand. The argument also documents why the constant $-1$ is excluded by curvature, closing a natural degenerate branch of the functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.