pith. machine review for the scientific record. sign in
structure definition def or abbrev

CoronalLyapunovCert

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)

  70structure CoronalLyapunovCert where
  71  time_pos : ∀ k, 0 < coronalTime k
  72  one_step_ratio : ∀ k, coronalTime (k + 1) = coronalTime k * phi
  73  strictly_increasing : ∀ k, coronalTime k < coronalTime (k + 1)
  74  adjacent_ratio_eq_phi : ∀ k, coronalTime (k + 1) / coronalTime k = phi
  75
  76/-- Coronal Lyapunov timescale certificate. -/

used by (1)

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

depends on (1)

Lean names referenced from this declaration's body.