IndisputableMonolith.Climate.OperationalForecastSkillFromJCost

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Operational Forecast Skill: Lyapunov Time on the Phi-Ladder
   6
   7Operational weather forecasting at ECMWF (IFS) and NOAA (GFS) shows a
   8characteristic skill-decay curve: 500-hPa anomaly correlation
   9coefficient (ACC) ≥ 0.6 ("useful skill") persists for ~10 days at
  10ECMWF, ~7 days at GFS in 2024. The recognition-Lyapunov-time prediction
  11is that adjacent forecast-skill horizons across operational centers
  12ratio by exactly φ per integer rung of model resolution.
  13
  14ECMWF / GFS / lower-resolution-NWP horizon ladder:
  15- ECMWF IFS HRES (rung 0): 10 days
  16- GFS (rung -1): 10/φ ≈ 6.2 days (matches empirical 6-7)
  17- earlier GFS pre-FV3 (rung -2): 10/φ² ≈ 3.8 days
  18
  19The φ-ratio between ECMWF and GFS skill-horizons is a structural
  20prediction; if a third operational center sits between them at a
  21non-φ-rational distance, the prediction would be falsified.
  22
  23Compounds with `Climate/PredictabilityFromJCost` (the canonical-band
  24predictability cutoff).
  25
  26Lean status: 0 sorry, 0 axiom.
  27-/
  28
  29namespace IndisputableMonolith
  30namespace Climate
  31namespace OperationalForecastSkillFromJCost
  32
  33open Constants
  34
  35noncomputable section
  36
  37/-- Reference forecast horizon (RS-native dimensionless 1, calibrated
  38at ECMWF rung 0). -/
  39def referenceHorizon : ℝ := 1
  40
  41/-- Forecast horizon at φ-ladder rung `k` (negative `k` for lower-
  42resolution model that loses skill earlier; we work with positive `k`
  43and flip sign in the bridge theorem below). -/
  44def horizonAtRung (k : ℕ) : ℝ := referenceHorizon * phi ^ (-(k : ℤ))
  45
  46theorem horizonAtRung_pos (k : ℕ) : 0 < horizonAtRung k := by
  47  unfold horizonAtRung referenceHorizon
  48  have : 0 < phi ^ (-(k : ℤ)) := zpow_pos Constants.phi_pos _
  49  linarith [this]
  50
  51theorem horizonAtRung_succ_ratio (k : ℕ) :
  52    horizonAtRung (k + 1) = horizonAtRung k * phi⁻¹ := by
  53  unfold horizonAtRung
  54  have hphi_ne : phi ≠ 0 := Constants.phi_ne_zero
  55  have hzpow : phi ^ (-((k : ℤ) + 1)) = phi ^ (-(k : ℤ)) * phi⁻¹ := by
  56    rw [show (-((k : ℤ) + 1)) = -(k : ℤ) + (-1 : ℤ) by ring]
  57    rw [zpow_add₀ hphi_ne]
  58    simp
  59  have hcast : ((k + 1 : ℕ) : ℤ) = (k : ℤ) + 1 := by push_cast; ring
  60  rw [hcast, hzpow]; ring
  61
  62theorem horizonAtRung_strictly_decreasing (k : ℕ) :
  63    horizonAtRung (k + 1) < horizonAtRung k := by
  64  rw [horizonAtRung_succ_ratio]
  65  have hk : 0 < horizonAtRung k := horizonAtRung_pos k
  66  have hphi_inv_lt_one : phi⁻¹ < 1 := by
  67    have hphi_gt_one : (1 : ℝ) < phi := by
  68      have := Constants.phi_gt_onePointFive; linarith
  69    exact inv_lt_one_of_one_lt₀ hphi_gt_one
  70  have : horizonAtRung k * phi⁻¹ < horizonAtRung k * 1 :=
  71    mul_lt_mul_of_pos_left hphi_inv_lt_one hk
  72  simpa using this
  73
  74theorem horizon_adjacent_ratio (k : ℕ) :
  75    horizonAtRung (k + 1) / horizonAtRung k = phi⁻¹ := by
  76  rw [horizonAtRung_succ_ratio]
  77  have hpos : 0 < horizonAtRung k := horizonAtRung_pos k
  78  field_simp [hpos.ne']
  79
  80structure OperationalForecastSkillCert where
  81  horizon_pos : ∀ k, 0 < horizonAtRung k
  82  one_step_ratio : ∀ k, horizonAtRung (k + 1) = horizonAtRung k * phi⁻¹
  83  strictly_decreasing : ∀ k, horizonAtRung (k + 1) < horizonAtRung k
  84  adjacent_ratio_eq_inv_phi :
  85    ∀ k, horizonAtRung (k + 1) / horizonAtRung k = phi⁻¹
  86
  87/-- Operational-forecast-skill certificate. -/
  88def operationalForecastSkillCert : OperationalForecastSkillCert where
  89  horizon_pos := horizonAtRung_pos
  90  one_step_ratio := horizonAtRung_succ_ratio
  91  strictly_decreasing := horizonAtRung_strictly_decreasing
  92  adjacent_ratio_eq_inv_phi := horizon_adjacent_ratio
  93
  94end
  95end OperationalForecastSkillFromJCost
  96end Climate
  97end IndisputableMonolith
  98