dAlembert_forces_cosh_is_theorem
plain-language theorem explainer
The theorem shows that any C² function H satisfying the d'Alembert equation with H(0)=1 and H''(0)=1 must equal cosh. Researchers closing the Recognition Science inevitability argument for the J-cost would cite this to obtain uniqueness from the multiplicative consistency condition. The proof is a one-line wrapper that invokes the Aczél-form d'Alembert solution after replacing the C² hypothesis with its continuity consequence.
Claim. Let $H : ℝ → ℝ$. If $H(0) = 1$, $H$ is twice continuously differentiable, $H(t+u) + H(t-u) = 2 H(t) H(u)$ holds for all real $t,u$, and $H''(0) = 1$, then $H(t) = cosh(t)$.
background
In Recognition Science the cost is reparametrized by $H(x) = J(x) + 1$ with $J(x) = (x + x^{-1})/2 - 1$, converting the Recognition Composition Law into the d'Alembert equation $H(xy) + H(x/y) = 2 H(x) H(y)$. The log-coordinate map $G(t) = F(exp t)$ then yields the additive form $H(t+u) + H(t-u) = 2 H(t) H(u)$. The module proves the strongest unconditional form: any C² $F$ obeying symmetry, normalization $F(1)=0$, and the existence of some combiner $P$ must satisfy $F = J$ and $P(u,v) = 2uv + 2u + 2v$ on the nonnegative quadrant.
proof idea
This is a one-line wrapper that applies dAlembert_cosh_solution_aczel. The only extra step extracts continuity from the ContDiff ℝ 2 hypothesis and passes it together with the remaining data (H(0)=1, the d'Alembert equation, and H''(0)=1) to the Aczél version.
why it matters
The result supplies the cosh-uniqueness step required by the full unconditional RCL theorem. It is invoked directly by full_inevitability_explicit and washburn_full_unconditional to finish the argument that both F and P are forced with no prior assumption on P. In the forcing chain this realizes T5 J-uniqueness, confirming that the self-similar fixed point is the only C² solution. It closes the gap between earlier partial unconditional theorems and the strongest form that assumes nothing about the combiner.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.