  67  rw [coronalTime_succ_ratio]
  68  field_simp [(coronalTime_pos k).ne']
  69
  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. -/
  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.