dAlembert_cosh_solution_of_contDiff
A twice continuously differentiable real function satisfying the d'Alembert equation, normalized to value 1 at zero with second derivative 1 at zero, must equal the hyperbolic cosine. Researchers closing the T5 regularity seam in Recognition Science cite this to derive the canonical reciprocal cost from normalization and the composition law alone. The argument first converts the functional equation to the ODE H'' = H, establishes evenness together with vanishing first derivative at the origin, then invokes the cosh initial-value uniqueness.
claimLet $H : ℝ → ℝ$ be twice continuously differentiable. Suppose $H(0) = 1$, $H(t + u) + H(t - u) = 2 H(t) H(u)$ for all real $t, u$, and the second derivative of $H$ at zero equals 1. Then $H(t) = cosh(t)$ for every real $t$.
background
The module ContDiff Reduction for T5 removes a central portion of the explicit T5 regularity seam. It establishes that a ContDiff ℝ 2 d'Alembert solution satisfies the ODE H'' = H. The Recognition Composition Law plus normalization already force reciprocity, so that on the ContDiff surface the canonical reciprocal cost follows from normalization, composition, and calibration alone. The shifted cost is defined by H(x) = J(x) + 1, under which the composition law takes the standard d'Alembert form H(xy) + H(x/y) = 2 H(x) H(y).
proof idea
The term proof first applies dAlembert_to_ODE_of_contDiff to obtain the ODE ∀ t, (Hf)''(t) = Hf(t). It then invokes dAlembert_even to obtain that Hf is even. Differentiability at zero follows from contDiffTwo_differentiable. The first derivative at zero is shown to vanish by even_deriv_at_zero. The conclusion is obtained by applying ode_cosh_uniqueness_contdiff to the resulting initial-value problem.
why it matters in Recognition Science
This result closes part of the T5 regularity seam inside the ContDiffReduction module and feeds directly into washburn_uniqueness_of_contDiff. The latter asserts that normalization, the composition law, calibration, and C² regularity of H = G + 1 already force the canonical reciprocal cost, with reciprocal symmetry derived rather than assumed. In the framework it supports the sharpened T5 surface that aligns with J-uniqueness from the forcing chain (T5).
scope and limits
- Does not establish the result for merely continuous or once-differentiable functions.
- Does not extend to non-real domains or complex-valued functions.
- Does not incorporate the phi-ladder or discrete rung structure.
- Does not address the Berry creation threshold or Z_cf calibration.
formal statement (Lean)
170theorem dAlembert_cosh_solution_of_contDiff
171 (Hf : ℝ → ℝ)
172 (h_one : Hf 0 = 1)
173 (h_dAlembert : ∀ t u, Hf (t + u) + Hf (t - u) = 2 * Hf t * Hf u)
174 (h_diff : ContDiff ℝ 2 Hf)
175 (h_deriv2_zero : deriv (deriv Hf) 0 = 1) :
176 ∀ t, Hf t = Real.cosh t := by
proof body
Term-mode proof.
177 have h_ode : ∀ t, deriv (deriv Hf) t = Hf t :=
178 dAlembert_to_ODE_of_contDiff Hf h_dAlembert h_diff h_deriv2_zero
179 have h_even : Function.Even Hf := dAlembert_even Hf h_one h_dAlembert
180 have h_diff0 : DifferentiableAt ℝ Hf 0 :=
181 (contDiffTwo_differentiable h_diff).differentiableAt
182 have h_deriv_zero : deriv Hf 0 = 0 :=
183 even_deriv_at_zero Hf h_even h_diff0
184 exact ode_cosh_uniqueness_contdiff Hf h_diff h_ode h_one h_deriv_zero
185
186/-- Sharpened T5 surface:
187normalization, the composition law, calibration, and `C²` regularity of `H = G + 1`
188already force the canonical reciprocal cost. Reciprocal symmetry is derived, not assumed. -/