dAlembert_solution_deriv_zero
Differentiable solutions to the d'Alembert functional equation have vanishing derivative at the origin. Recognition Science invokes this to constrain the low-order expansion of the shifted cost functional before ascending the phi-ladder. The proof reduces the claim to evenness of solutions followed by the general fact that even functions have zero derivative at zero.
claimLet $H : ℝ → ℝ$ satisfy $H(0) = 1$ and $H(t+u) + H(t-u) = 2 H(t) H(u)$ for all real $t,u$. If $H$ is differentiable at $0$, then $H'(0) = 0$.
background
Recognition Science begins with a cost functional $J$ obeying the Recognition Composition Law and symmetry $J(x) = J(1/x)$. The shifted form $H(x) = J(x) + 1$ converts the law into the d'Alembert equation $H(xy) + H(x/y) = 2 H(x) H(y)$. In logarithmic coordinates $G(t) = J(e^t)$ the same equation becomes $G(t+u) + G(t-u) = Φ(G(t), G(u))$ with $G$ even and $G(0) = 0$; adding 1 yields the normalized $H$ used here. The definition IsDAlembertSolution encodes exactly this normalization together with the functional equation. The module shows that symmetry plus a quadratic combiner force this equation as the unique low-complexity form.
proof idea
The term proof first calls dAlembert_solution_even to obtain that $H$ is even. It then applies the upstream lemma even_deriv_at_zero, which equates the derivative at zero to the derivative of the negated argument and concludes the result is zero.
why it matters in Recognition Science
This step belongs to the classification of d'Alembert solutions inside Foundation.DAlembert.Proof and supplies the first derivative constraint needed before imposing the calibration $H''(0) = 1$. The surviving cosh form then forces the self-similar fixed point phi (T5-T6) and the eight-tick octave (T7) in the UnifiedForcingChain. It therefore anchors the low-energy expansion of the cost functional before the phi-ladder mass formula is applied.
scope and limits
- Does not prove existence of non-constant solutions.
- Does not apply to solutions lacking differentiability at zero.
- Does not derive the second derivative or higher Taylor terms.
- Does not address the full Aczél classification of continuous solutions.
formal statement (Lean)
121theorem dAlembert_solution_deriv_zero (H : ℝ → ℝ) (h : IsDAlembertSolution H)
122 (hDiff : DifferentiableAt ℝ H 0) :
123 deriv H 0 = 0 := by
proof body
Term-mode proof.
124 have hEven := dAlembert_solution_even H h
125 exact even_deriv_at_zero H hEven hDiff
126
127/-! ## Classification of Solutions -/
128
129/-- The classification theorem for d'Alembert equation (Aczél).
130
131Continuous solutions to H(t+u) + H(t-u) = 2·H(t)·H(u) with H(0) = 1 are:
1321. H(t) = 1 (constant)
1332. H(t) = cos(αt) for some α ∈ ℂ
1343. H(t) = cosh(αt) for some α ∈ ℝ
135
136With the calibration H''(0) = 1, only H = cosh survives. -/