dAlembert_cos_solution
plain-language theorem explainer
The d'Alembert functional equation with normalization H(0)=1, continuity, and second derivative at zero equal to -1 forces H to equal the cosine function on the reals. Recognition Science researchers cite this as the Angle T5 result that selects the oscillatory branch for angle coupling, parallel to the cosh solution in the cost sector. The proof derives the ODE H''=-H from the functional equation, establishes evenness and vanishing first derivative at zero via upstream lemmas, then applies the ODE uniqueness theorem.
Claim. Let $H:ℝ→ℝ$ be continuous with $H(0)=1$, satisfying the d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$ for all real $t,u$, and with $H''(0)=-1$, together with the regularity hypotheses that bootstrap to twice continuous differentiability. Then $H(t)=cos(t)$ for all real $t$.
background
In the Angle Functional Equation module the d'Alembert equation admits two solution branches under standard regularity: the cosh branch tied to the cost functional and the cos branch for angle coupling. Here H denotes the angle coupling map, satisfying axioms Aθ1 (d'Alembert), Aθ2 (continuity), Aθ3 (normalization H(0)=1), and Aθ4 (calibration H''(0)=-1). Upstream, the lemma dAlembert_even from Cost.FunctionalEquation shows that the functional equation forces H to be even. The companion result even_deriv_at_zero then yields deriv H 0 =0 once differentiability at zero is available. The key uniqueness statement ode_cos_uniqueness (appearing in both AczelProof and AczelTheorem) asserts that the unique solution to f''=-f with f(0)=1 and f'(0)=0 is the cosine.
proof idea
The tactic proof first invokes the hypothesis dAlembert_to_ODE_hypothesis_neg to obtain the ODE ∀t, deriv(deriv H)t = -H t. It then calls Cost.FunctionalEquation.dAlembert_even to establish that H is even. The smoothness hypothesis supplies differentiability at zero, after which even_deriv_at_zero gives deriv H 0 =0. The proof concludes by applying ode_cos_uniqueness with the ODE, the two initial conditions, and the remaining regularity hypotheses.
why it matters
This theorem supplies the cosine uniqueness required by the downstream master result THEOREM_angle_coupling_rigidity, which packages axioms Aθ1–Aθ4 into the statement that any qualifying H equals cos. It completes the T5 step of the angle forcing chain, mirroring the cosh solution dAlembert_cosh_solution in the cost sector. The negative calibration H''(0)=-1 selects the oscillatory solution, in contrast to the positive curvature that yields the hyperbolic cosine for the shifted cost H(x)=J(x)+1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.