coronalTime_pos

formal source

  43/-- Coronal timescale at φ-ladder rung `k`. -/
  44def coronalTime (k : ℕ) : ℝ := referenceTime * phi ^ k
  45
  46theorem coronalTime_pos (k : ℕ) : 0 < coronalTime k := by
  47  unfold coronalTime referenceTime
  48  have : 0 < phi ^ k := pow_pos Constants.phi_pos k
  49  linarith [this]
  50
  51theorem coronalTime_succ_ratio (k : ℕ) :
  52    coronalTime (k + 1) = coronalTime k * phi := by
  53  unfold coronalTime; rw [pow_succ]; ring
  54
  55theorem coronalTime_strictly_increasing (k : ℕ) :
  56    coronalTime k < coronalTime (k + 1) := by
  57  rw [coronalTime_succ_ratio]
  58  have hk : 0 < coronalTime k := coronalTime_pos k
  59  have hphi_gt_one : (1 : ℝ) < phi := by
  60    have := Constants.phi_gt_onePointFive; linarith
  61  have : coronalTime k * 1 < coronalTime k * phi :=
  62    mul_lt_mul_of_pos_left hphi_gt_one hk
  63  simpa using this
  64
  65theorem coronal_adjacent_ratio (k : ℕ) :
  66    coronalTime (k + 1) / coronalTime k = phi := by
  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. -/