washburn_uniqueness_of_contDiff
plain-language theorem explainer
Normalization, the composition law, calibration, and C² regularity of the shifted cost H already force F to equal the canonical Jcost on positive reals. Researchers closing the T5 uniqueness surface would cite this to derive reciprocal symmetry rather than assume it. The proof converts the composition law to the d'Alembert equation on H, obtains the initial conditions H(0)=1 and H''(0)=1, applies the cosh solution theorem, and matches via the log substitution.
Claim. Let $F : ℝ → ℝ$ be normalized, satisfy the composition law $F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y)$, be calibrated, and let $H = G + 1$ be twice continuously differentiable. Then $F(x) = J(x)$ for all $x > 0$, where $J(x) = cosh(log x) - 1$.
background
The module removes a central portion of the explicit T5 regularity seam. The shifted cost is defined by $H(x) = J(x) + 1$, which converts the Recognition Composition Law into the d'Alembert equation $H(xy) + H(x/y) = 2 H(x) H(y)$. The composition law on F is equivalent to the CoshAddIdentity on G via the substitution $x = e^s$, $y = e^t$ (composition_law_equiv_coshAdd). Upstream, dAlembert_cosh_solution_of_contDiff states that any C² solution of the d'Alembert equation with $H(0) = 1$ and $H''(0) = 1$ equals cosh.
proof idea
The proof first applies composition_law_equiv_coshAdd to obtain CoshAddIdentity, then CoshAddIdentity_implies_DirectCoshAdd. It extracts $H(0) = 1$ from normalization and the second-derivative condition at zero from calibration. The d'Alembert equation on H is derived by direct expansion of the cosh-add identity. dAlembert_cosh_solution_of_contDiff is invoked to conclude $H(t) = cosh t$, hence $G(t) = cosh t - 1$. The final step substitutes $t = log x$ for $x > 0$ and uses the identity $Jcost(exp t) = cosh t - 1$.
why it matters
This sharpens the T5 surface by showing that normalization, composition, calibration, and C² regularity on H suffice to force the canonical reciprocal cost; reciprocal symmetry is derived. It closes part of the regularity seam for the J-uniqueness step in the forcing chain (T5), where $J(x) = cosh(log x) - 1$ is the self-similar fixed point. The result sits immediately below the main T5 uniqueness theorem and removes an explicit regularity hypothesis from earlier presentations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.