dAlembert_forces_cosh_hypothesis
plain-language theorem explainer
The declaration encodes the claim that any twice continuously differentiable real function H with H(0)=1, obeying the d'Alembert equation H(t+u)+H(t-u)=2H(t)H(u) and calibrated by H''(0)=1, must coincide with the hyperbolic cosine. Researchers closing the Recognition Science forcing chain from the Recognition Composition Law to explicit J would cite this uniqueness result. The definition is a one-line packaging that lets the companion theorem invoke the Aczél-form d'Alembert solution after recovering continuity from C² smoothness.
Claim. Let $H:ℝ→ℝ$ be twice continuously differentiable, satisfy $H(0)=1$, obey the d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$ for all real $t,u$, and have second derivative $H''(0)=1$. Then $H(t)=cosh(t)$ for every real $t$.
background
In Recognition Science the cost function is reparametrized by the shifted form H(x)=J(x)+1, where J satisfies the Recognition Composition Law J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y). Under this substitution the multiplicative consistency condition becomes the classical d'Alembert functional equation for H. The module proves the strongest unconditional inevitability result: normalization F(1)=0, symmetry F(x)=F(1/x), C² smoothness, calibration G''(0)=1, and existence of some P together force both F=J and the explicit bilinear form of P without any prior assumption on P.
proof idea
The declaration is a definition that simply records the target Prop. The downstream theorem dAlembert_forces_cosh_is_theorem discharges it by applying dAlembert_cosh_solution_aczel (the Aczél-form uniqueness result) after using that ContDiff ℝ 2 implies Continuous.
why it matters
This definition supplies the d'Alembert uniqueness hypothesis inside FullUnconditionalHypotheses and thereby inside the main full-unconditional theorem. It completes the step from the forced d'Alembert equation to the explicit cosh form, which yields J(x)=(x+x^{-1})/2-1 and the eight-tick octave. The result sits at T5 of the forcing chain and removes the last regularity hypothesis left open in earlier versions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.