theorem proved term proof

`cosh_at_zero`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  81theorem cosh_at_zero : Real.cosh 0 = 1 := by

proof body

Term-mode proof.

  82  simp [Real.cosh_zero]
  83
  84/-- The J-cost G(t) = cosh(t) - 1 has its unique real zero at t = 0.
  85    In log coordinates, t = 0 means x = e⁰ = 1: the RS balance point. -/

depends on (8)

Lean names referenced from this declaration's body.

G in IndisputableMonolith.Constants decl_use
G in IndisputableMonolith.Constants.Codata decl_use
G in IndisputableMonolith.Cost.FunctionalEquation decl_use
has in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
G in IndisputableMonolith.Gravity.JCostInflaton decl_use
point in IndisputableMonolith.Numerics.Interval.Basic decl_use