washburn_uniqueness_of_contDiff
plain-language theorem explainer
Any function F on the reals that is normalized, obeys the Recognition Composition Law, is calibrated, and has its shifted version H twice continuously differentiable must coincide with the canonical J-cost on positive reals. Researchers closing the T5 J-uniqueness step in the forcing chain would cite this sharpened surface result. The argument converts the composition law into the cosh-add identity, derives the d'Alembert equation for H, solves it via the cosh theorem under the C2 and calibration hypotheses, then matches the expression to Jcost
Claim. Let $F:ℝ→ℝ$ satisfy normalization, the composition law $F(xy)+F(x/y)=2F(x)F(y)+2F(x)+2F(y)$, calibration, and $C^2$ regularity of the shifted function $H=G+1$. Then $F(x)=J(x)$ for all $x>0$, where $J(x)=cosh(log x)-1$.
background
The module ContDiffReduction removes an explicit regularity seam from the T5 J-uniqueness surface. H is the shifted cost $H(x)=J(x)+1$; under this change the Recognition Composition Law becomes the d'Alembert equation $H(xy)+H(x/y)=2H(x)H(y)$. G F is the reparametrized map satisfying $G F(t)=F(e^t)$, so that the composition law on F is equivalent to the cosh-add identity on G F. The upstream theorem dAlembert_cosh_solution_of_contDiff asserts that any $C^2$ solution of the d'Alembert equation with value 1 at 0 and second derivative 1 at 0 equals cosh. The module doc states that on the ContDiff surface the canonical reciprocal cost follows from normalization, composition and calibration alone.
proof idea
The tactic proof first applies composition_law_equiv_coshAdd to obtain CoshAddIdentity, then CoshAddIdentity_implies_DirectCoshAdd to reach the direct cosh-add form on G F. It derives the d'Alembert equation for H F from that identity, extracts the second-derivative condition at zero from calibration, and invokes dAlembert_cosh_solution_of_contDiff to conclude H F equals cosh. It deduces G F equals cosh minus one, then substitutes $x=exp(log x)$ and uses the known identity Jcost_G_eq_cosh_sub_one to match F x with Jcost x.
why it matters
This theorem sharpens the T5 surface by deriving reciprocal symmetry rather than assuming it; normalization, the composition law, calibration and $C^2$ regularity of H already force the canonical J-cost. It belongs to the ContDiffReduction module whose stated goal is to remove explicit T5 regularity seams. The result supports the J-uniqueness step (T5) in the forcing chain where J is identified with cosh(log x)-1. No downstream uses are recorded, but the declaration closes part of the regularity gap between the composition law and the self-similar fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.