cos_second_deriv_eq
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 in Recognition Science
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.
scope and limits
- Does not prove uniqueness of solutions to the ODE.
- Does not derive the d'Alembert equation itself.
- Does not treat complex-valued or vector-valued functions.
- Does not supply initial conditions or boundary data.
formal statement (Lean)
118theorem cos_second_deriv_eq : ∀ t, deriv (deriv (fun x => Real.cos x)) t = -Real.cos t := by
proof body
Tactic-mode proof.
119 intro t
120 have h1 : deriv (fun x => Real.cos x) = (fun x => -Real.sin x) := by
121 funext x
122 simpa using (Real.deriv_cos x)
123 rw [h1]
124 have hneg : deriv (fun x => -Real.sin x) t = -(deriv Real.sin t) := by
125 simpa using (deriv_neg (f := Real.sin) (x := t))
126 rw [hneg]
127 simp [Real.deriv_sin]
128
129/-- cos has the correct initial conditions: cos(0) = 1, cos'(0) = 0. -/