theorem proved wrapper

`coronalTime_succ_ratio`

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

formal statement (Lean)

  51theorem coronalTime_succ_ratio (k : ℕ) :
  52    coronalTime (k + 1) = coronalTime k * phi := by

One-line wrapper that applies unfold.

  53  unfold coronalTime; rw [pow_succ]; ring
  54

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

coronal_adjacent_ratio in IndisputableMonolith.Astrophysics.CoronalLyapunovTime decl_use
coronalLyapunovCert in IndisputableMonolith.Astrophysics.CoronalLyapunovTime decl_use
coronalTime_strictly_increasing in IndisputableMonolith.Astrophysics.CoronalLyapunovTime decl_use

Lean names referenced from this declaration's body.

coronalTime in IndisputableMonolith.Astrophysics.CoronalLyapunovTime decl_use