theorem proved term proof

`defectIterate_zero_param`

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

formal statement (Lean)

  57@[simp] theorem defectIterate_zero_param (n : ℕ) : defectIterate 0 n = 0 := by

Term-mode proof.

  58  simp [defectIterate, Real.cosh_zero]
  59
  60/-- d₀(t) = cosh(t) − 1 = J_log(t). -/

Lean names referenced from this declaration's body.

J_log in IndisputableMonolith.Foundation.DiscretenessForcing decl_use
J_log in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
defectIterate in IndisputableMonolith.NumberTheory.ZeroCompositionLaw decl_use