pith. machine review for the scientific record. sign in
theorem proved term proof high

cosh_second_deriv_eq

show as:
view Lean formalization →

The declaration establishes that the second derivative of the real hyperbolic cosine equals the function itself. Researchers working on uniqueness proofs for functional equations in Recognition Science would cite it when reducing the d'Alembert equation to an ODE. The proof is a direct term-mode application of the known derivatives of cosh and sinh.

claim$forall t in R, d^2/dt^2 cosh(t) = cosh(t)$

background

This lemma sits in the module providing functional equation helpers for the T5 cost uniqueness proof. The local theoretical setting consists of lemmas supporting derivation of the cost functional equation that identifies the J-cost with an expression involving cosh. It draws on standard calculus facts imported from Mathlib for derivatives of hyperbolic functions.

proof idea

The term proof first rewrites the first derivative of cosh via the known identity deriv (fun x => Real.cosh x) = Real.sinh, then applies the identity deriv Real.sinh = Real.cosh, and concludes by function congruence at the point t.

why it matters in Recognition Science

It directly supports the theorem establishing that cosh satisfies the d'Alembert to ODE hypothesis and feeds into the ODE uniqueness result showing that the unique solution to H'' = H with H(0)=1, H'(0)=0 is cosh. This step is key for T5 J-uniqueness in the Recognition Science forcing chain, where J is identified with cosh(log x) - 1.

scope and limits

Lean usage

intro _ _ _ _; exact cosh_second_deriv_eq

formal statement (Lean)

 400theorem cosh_second_deriv_eq : ∀ t, deriv (deriv (fun x => Real.cosh x)) t = Real.cosh t := by

proof body

Term-mode proof.

 401  intro t
 402  have h1 : deriv (fun x => Real.cosh x) = Real.sinh := Real.deriv_cosh
 403  rw [h1]
 404  have h2 : deriv Real.sinh = Real.cosh := Real.deriv_sinh
 405  exact congrFun h2 t
 406

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.