`coronalLyapunovCert`

definition

show as: view math explainer →

module: IndisputableMonolith.Astrophysics.CoronalLyapunovTime
domain: Astrophysics
line: 77 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Astrophysics.CoronalLyapunovTime on GitHub at line 77.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

  74  adjacent_ratio_eq_phi : ∀ k, coronalTime (k + 1) / coronalTime k = phi
  75
  76/-- Coronal Lyapunov timescale certificate. -/
  77def coronalLyapunovCert : CoronalLyapunovCert where
  78  time_pos := coronalTime_pos
  79  one_step_ratio := coronalTime_succ_ratio
  80  strictly_increasing := coronalTime_strictly_increasing
  81  adjacent_ratio_eq_phi := coronal_adjacent_ratio
  82
  83end
  84end CoronalLyapunovTime
  85end Astrophysics
  86end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.