washburn_uniqueness
plain-language theorem explainer
Any function F from positive reals to reals obeying reciprocity F(x)=F(1/x), normalization F(1)=0, the Recognition Composition Law, calibration of the second derivative at zero after log reparametrization, and the listed continuity plus regularity conditions must equal the J-cost J(x)=(x + x^{-1})/2 - 1 on all positives. Workers on the T5 step of the forcing chain or on uniqueness of the canonical cost algebra cite this result. The argument converts the composition law into a d'Alembert equation on the shifted H function, invokes the Aczél cosh
Claim. Let $F : (0,∞) → ℝ$ satisfy reciprocity $F(x) = F(x^{-1})$ for $x>0$, normalization $F(1)=0$, the Recognition Composition Law $F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(y)$ for all $x,y>0$, calibration $G''(0)=1$ where $G(t)=F(e^t)$, continuity on $(0,∞)$, and the regularity hypotheses on the shifted function $H=G+1$. Then $F(x)=J(x)$ for all $x>0$, where $J(x)=(x+x^{-1})/2-1$.
background
The module supplies functional-equation helpers for the T5 cost-uniqueness argument. IsReciprocalCost encodes reciprocity $F(x)=F(1/x)$, IsNormalized encodes $F(1)=0$, SatisfiesCompositionLaw is the Recognition Composition Law, and IsCalibrated is the second-derivative condition $G''(0)=1$ with $G(t)=F(e^t)$. The auxiliary $H$ is the shift $H(t)=G(t)+1$. Upstream, the CostAlgebra definition of $H$ shows that the RCL becomes the standard d'Alembert equation $H(xy)+H(x/y)=2H(x)H(y)$. The local setting is the T5 uniqueness proof that selects the explicit $J$ form used downstream for mass ladders and constants.
proof idea
The tactic proof first converts the composition law to CoshAddIdentity via composition_law_equiv_coshAdd. It defines $G$ and $H$, obtains evenness of $G$ from G_even_of_reciprocal_symmetry, $G(0)=0$ from G_zero_of_unit, $H(0)=1$ from normalization, and continuity of both. It derives the d'Alembert equation for $H$ from DirectCoshAdd and the second-derivative condition from calibration. It then applies dAlembert_cosh_solution (with the four regularity hypotheses) to conclude $H(t)=cosh t$, unshifting to $G(t)=cosh t-1$, and recovers $F(x)=Jcost(x)$ by the log change of variables and Jcost_G_eq_cosh_sub_one.
why it matters
This is the core T5 J-uniqueness theorem in the forcing chain. It feeds cost_algebra_unique (the canonical cost algebra is unique) and primitive_to_uniqueness_of_kernel (the public Aczél-kernel form of T5). The doc-comment identifies it as Theorem 1.1 of Washburn & Zlatanović on uniqueness of the canonical reciprocal cost. It closes the seam between the Recognition Composition Law and the explicit $J$ used for the phi-ladder mass formula and the constants $c=1$, $hbar=phi^{-5}$. No open scaffolding remains inside the proved claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
New supergravity inflation models tie ξ to α by ξ = 1/(6α)
"We presented {\it new supergravity ξ-attractor models with non-minimal coupling to gravity}... ξ-attractors relation to exponential and polynomial α-attractors under condition that α = 1/(6ξ)."