forecastTimescaleCount

formal source

  30  | shortRange | medium | extended | monthly | seasonal
  31  deriving DecidableEq, Repr, BEq, Fintype
  32
  33theorem forecastTimescaleCount : Fintype.card ForecastTimescale = 5 := by decide
  34
  35noncomputable def forecastSkill (k : ℕ) : ℝ := (phi ^ k)⁻¹
  36
  37theorem forecastSkill_pos (k : ℕ) : 0 < forecastSkill k :=
  38  inv_pos.mpr (pow_pos phi_pos k)
  39
  40theorem forecastSkill_decay (k : ℕ) :
  41    forecastSkill (k + 1) / forecastSkill k = phi⁻¹ := by
  42  unfold forecastSkill
  43  have hk := (pow_pos phi_pos k).ne'
  44  rw [pow_succ, mul_inv]
  45  field_simp [hk, phi_ne_zero]
  46
  47/-- Lorenz predictability limit ≈ gap-45/3 days. -/
  48def lorenzLimitDays : ℕ := 15  -- gap-45/3 = 15
  49
  50structure ClimateForecastCert where
  51  five_timescales : Fintype.card ForecastTimescale = 5
  52  skill_pos : ∀ k, 0 < forecastSkill k
  53  skill_decay : ∀ k, forecastSkill (k + 1) / forecastSkill k = phi⁻¹
  54  lorenz_limit : lorenzLimitDays = 15
  55
  56noncomputable def climateForecastCert : ClimateForecastCert where
  57  five_timescales := forecastTimescaleCount
  58  skill_pos := forecastSkill_pos
  59  skill_decay := forecastSkill_decay
  60  lorenz_limit := rfl
  61
  62end IndisputableMonolith.Climate.ClimateForecastSkillFromJCost