dAlembert_solution_deriv_zero
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.