dAlembert_to_ODE_of_contDiff
A twice continuously differentiable function satisfying the d'Alembert functional equation with second derivative at zero equal to one obeys the ODE H''(t) = H(t) for all t. Researchers reducing T5 J-uniqueness in Recognition Science cite this to close the regularity seam between the functional equation and the hyperbolic cosine solution. The argument applies the second-derivative identity at the origin, substitutes the calibration hypothesis, and concludes via linear arithmetic.
claimLet $H : ℝ → ℝ$ be twice continuously differentiable and satisfy $H(t+u) + H(t-u) = 2 H(t) H(u)$ for all real $t,u$, with $H''(0) = 1$. Then $H''(t) = H(t)$ for all real $t$.
background
The module removes an explicit regularity seam in the T5 reduction. It shows that any C² solution of the d'Alembert equation with H''(0)=1 obeys the ODE H''=H. The upstream lemma states that differentiation of the first-derivative identity at u=0 yields 2 H''(t) = 2 H(t) H''(0) for all t. The PrimitiveDistinction theorem supplies the seven-axiom reduction to four structural conditions, while the Bridge structure encodes ledger equivalence used throughout the framework.
proof idea
The proof is a one-line wrapper. It applies the lemma dAlembert_second_deriv_at_zero_of_contDiff to obtain the relation 2 H''(t) = 2 H(t) H''(0), substitutes the given H''(0)=1, and concludes H''(t)=H(t) by linear arithmetic.
why it matters in Recognition Science
This supplies the ODE step required by dAlembert_cosh_solution_of_contDiff, which identifies C² solutions with cosh. It advances the T5 reduction by eliminating the regularity seam between the functional equation and the differential equation. The parent chain is the forcing sequence T5 to T8, where J-uniqueness forces the self-similar fixed point phi and the eight-tick octave.
scope and limits
- Does not prove existence of nontrivial solutions.
- Does not extend to functions with regularity below C².
- Does not address normalization H(0)=1 separately.
- Does not derive the composition law itself.
Lean usage
exact dAlembert_to_ODE_of_contDiff Hf h_dAlembert h_diff h_deriv2_zeroformal statement (Lean)
120theorem dAlembert_to_ODE_of_contDiff
121 (Hf : ℝ → ℝ)
122 (h_dAlembert : ∀ t u, Hf (t + u) + Hf (t - u) = 2 * Hf t * Hf u)
123 (h_diff : ContDiff ℝ 2 Hf)
124 (h_deriv2_zero : deriv (deriv Hf) 0 = 1) :
125 ∀ t, deriv (deriv Hf) t = Hf t := by
proof body
Term-mode proof.
126 intro t
127 have h_rel := dAlembert_second_deriv_at_zero_of_contDiff Hf h_dAlembert h_diff t
128 rw [h_deriv2_zero] at h_rel
129 linarith
130
131/-- Bridge from an explicit `ContDiff ℝ 2` hypothesis to the legacy ODE hypothesis. -/