cos_second_deriv_eq
plain-language theorem explainer
The second derivative of cosine equals its negative for every real argument. Researchers on the cosine branch of the d'Alembert equation in Recognition Science cite this identity to confirm the negative-curvature calibration that selects the oscillatory solution. The proof is a direct differentiation that rewrites the first derivative via the standard cosine rule, pulls out a negation, and simplifies the sine derivative.
Claim. $forall t in mathbb{R}, frac{d^2}{dt^2} cos(t) = -cos(t)$
background
This theorem belongs to the module developing the cosine branch of the d'Alembert functional equation H(t+u) + H(t-u) = 2 H(t) H(u). The module mirrors the cosh branch from the cost functional equation but uses negative curvature at zero to select the trigonometric solution instead. Axioms include d'Alembert (Aθ1), continuity (Aθ2), normalization H(0)=1 (Aθ3), and calibration H''(0)=-1 (Aθ4). The module document states that this supplies the Angle T5 theorem for angle coupling rigidity, complementary to the J-uniqueness result for the cost functional.
proof idea
The tactic proof introduces t, proves the first derivative of cosine equals negative sine by funext and the library rule Real.deriv_cos, rewrites, applies the derivative-of-negation rule to extract the outer minus sign, then simplifies the sine derivative to obtain negative cosine.
why it matters
The identity is invoked by cos_dAlembert_to_ODE to discharge the ODE hypothesis, by cos_satisfies_axioms to verify the calibration axiom at zero, and by ode_cos_uniqueness_contdiff to close the uniqueness argument under C^2 regularity. It supplies the concrete calibration step that forces the cosine branch once H''(0)=-1 is imposed, completing the angle counterpart to T5 J-uniqueness in the forcing chain and supporting the geometric necessity of recognition angle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.