cos_dAlembert_to_ODE
plain-language theorem explainer
Cosine satisfies the negative d'Alembert-to-ODE hypothesis, so that the functional equation together with continuity, normalization at zero, and second derivative minus one at zero imply the ODE second derivative equals negative the function. Analysts closing uniqueness arguments for angle coupling functions in Recognition Science cite the result to confirm the cosine branch meets derived regularity. The proof is a one-line wrapper that introduces the four hypotheses and applies the explicit second-derivative identity for cosine.
Claim. Let $H = $cos. If $H(0) = 1$, $H$ is continuous, $H$ obeys the d'Alembert equation $H(t+u) + H(t-u) = 2 H(t) H(u)$ for all real $t,u$, and $H''(0) = -1$, then $H''(t) = -H(t)$ for all real $t$.
background
The module isolates the cosine branch of the d'Alembert functional equation for angle coupling. The equation is $H(t+u) + H(t-u) = 2 H(t) H(u)$, with axioms of continuity, $H(0)=1$, and calibration $H''(0)=-1$ that select negative curvature and the trigonometric solution. This contrasts with the positive branch in Cost.FunctionalEquation, where the same equation plus $H''(0)=+1$ forces the J-cost functional $J(x) = (x + x^{-1})/2 - 1$ and the self-similar fixed point phi.
proof idea
The declaration is a one-line wrapper. It introduces the four antecedent hypotheses of dAlembert_to_ODE_hypothesis_neg and applies the upstream theorem cos_second_deriv_eq, which records the identity deriv (deriv (fun x => Real.cos x)) t = -Real.cos t.
why it matters
The result supplies the ODE verification step required by cos_satisfies_regularity, which packages the regularity conditions feeding the master theorem THEOREM_angle_coupling_rigidity. In the forcing chain this instance of T5 selects the cosine branch via negative calibration at zero, consistent with the eight-tick octave and the emergence of three spatial dimensions. It closes one regularity condition inside the Aθ1–Aθ4 axiom set for angle rigidity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.