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

coupling_identity

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  72theorem coupling_identity (t : ℝ) (ht : t ≠ 0) :
  73    exactCost t = coshEnhancement t * perturbativeCost t := by

proof body

Term-mode proof.

  74  simp only [exactCost, J_log, coshEnhancement, perturbativeCost, if_neg ht]
  75  have ht2 : t ^ 2 ≠ 0 := pow_ne_zero 2 ht
  76  field_simp [ht2]
  77
  78/-! ## §2. cosh(t) − 1 ≥ t²/2 -/
  79
  80/-- **cosh(t) − 1 ≥ t²/2** for all t.
  81
  82Standard real-analysis fact from the Taylor expansion:
  83  cosh(t) = 1 + t²/2 + t⁴/24 + t⁶/720 + ⋯
  84All higher-order terms are non-negative, so cosh(t) − 1 ≥ t²/2.
  85
  86Proof: let f(t) = cosh(t) − 1 − t²/2. Then f(0) = 0, f'(t) = sinh(t) − t,
  87f''(t) = cosh(t) − 1 ≥ 0 (convexity of cosh). So f' is non-decreasing,
  88f'(0) = 0, hence f'(t) ≥ 0 for t ≥ 0 and f'(t) ≤ 0 for t ≤ 0.
  89Therefore f achieves its minimum at t = 0 where f = 0, giving f ≥ 0. -/

used by (1)

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

depends on (21)

Lean names referenced from this declaration's body.