coronalTimescaleCount

formal source

  26  | alfvenCrossing | granulation | chromosphericEvaporation | coronalLoop | activeRegion
  27  deriving DecidableEq, Repr, BEq, Fintype
  28
  29theorem coronalTimescaleCount : Fintype.card CoronalTimescale = 5 := by decide
  30
  31noncomputable def timescaleAtRung (k : ℕ) : ℝ := phi ^ k
  32
  33theorem timescaleRatioPhiRung (k : ℕ) :
  34    timescaleAtRung (k + 1) / timescaleAtRung k = phi := by
  35  unfold timescaleAtRung
  36  have hpos := pow_pos phi_pos k
  37  rw [pow_succ, div_eq_iff hpos.ne']
  38  ring
  39
  40structure CoronalTimescaleCert where
  41  five_timescales : Fintype.card CoronalTimescale = 5
  42  phi_ratio : ∀ k, timescaleAtRung (k + 1) / timescaleAtRung k = phi
  43
  44noncomputable def coronalTimescaleCert : CoronalTimescaleCert where
  45  five_timescales := coronalTimescaleCount
  46  phi_ratio := timescaleRatioPhiRung
  47
  48end IndisputableMonolith.Astrophysics.CoronalTimescaleFromPhiLadder