IndisputableMonolith.Climate.PredictabilityFromJCost

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.Constants
   4
   5/-!
   6# Climate Predictability Horizon from J-Cost on Initial-Condition Ratio
   7
   8The forecast skill of a chaotic dynamical system decays with lead time.
   9The climate predictability horizon is the lead time at which initial-
  10condition uncertainty has grown by a factor `r := σ_forecast / σ_initial`
  11that crosses a recognition threshold. In RS terms, the horizon
  12corresponds to the lead time at which the J-cost on the uncertainty
  13ratio reaches the canonical golden-section quantum `J(φ) ∈ (0.11, 0.13)`.
  14
  15The structural prediction: deterministic forecast skill is structurally
  16permitted while `J(r) < J(φ)` and structurally lost once `J(r) ≥ J(φ)`,
  17giving a sharp horizon as one-φ-step uncertainty growth rather than
  18the soft "useful skill cutoff" used by present operational centers.
  19
  20This places climate predictability alongside the universal RS quantum:
  21the same band gates plaque vulnerability, infarction, dysbiosis,
  22combustion ignition, accretion-disk transition, magnetic reconnection,
  23materials fatigue, Haber-Bosch acceptance, and now climate forecast
  24skill.
  25
  26Lean status: 0 sorry, 0 axiom.
  27-/
  28
  29namespace IndisputableMonolith
  30namespace Climate
  31namespace PredictabilityFromJCost
  32
  33open Constants Cost
  34
  35noncomputable section
  36
  37/-- Forecast J-cost on the uncertainty growth ratio. -/
  38def forecastCost (r : ℝ) : ℝ := Cost.Jcost r
  39
  40theorem forecastCost_zero_at_unit : forecastCost 1 = 0 := Cost.Jcost_unit0
  41
  42theorem forecastCost_reciprocal_symm {r : ℝ} (hr : 0 < r) :
  43    forecastCost r = forecastCost r⁻¹ := Cost.Jcost_symm hr
  44
  45theorem forecastCost_nonneg {r : ℝ} (hr : 0 < r) :
  46    0 ≤ forecastCost r := Cost.Jcost_nonneg hr
  47
  48theorem forecastCost_pos_off_unit {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
  49    0 < forecastCost r := Cost.Jcost_pos_of_ne_one r hr hne
  50
  51/-- Predictability-horizon threshold = canonical golden-section quantum. -/
  52def PredictabilityThreshold : ℝ := Cost.Jcost phi
  53
  54/-- Forecast is past the horizon iff its J-cost meets or exceeds threshold. -/
  55def IsPastHorizon (r : ℝ) : Prop := PredictabilityThreshold ≤ forecastCost r
  56
  57/-- Forecast is within the horizon iff its J-cost is strictly below. -/
  58def IsWithinHorizon (r : ℝ) : Prop := forecastCost r < PredictabilityThreshold
  59
  60theorem horizon_states_exclusive {r : ℝ} :
  61    ¬ (IsWithinHorizon r ∧ IsPastHorizon r) := by
  62  rintro ⟨h_lt, h_ge⟩
  63  exact (lt_irrefl _) (lt_of_lt_of_le h_lt h_ge)
  64
  65theorem predictability_threshold_band :
  66    0.11 < PredictabilityThreshold ∧ PredictabilityThreshold < 0.13 := by
  67  unfold PredictabilityThreshold
  68  have hphi_ne : phi ≠ 0 := Constants.phi_ne_zero
  69  rw [Cost.Jcost_eq_sq hphi_ne]
  70  have h_lo : (1.61 : ℝ) < phi := Constants.phi_gt_onePointSixOne
  71  have h_hi : phi < (1.62 : ℝ) := Constants.phi_lt_onePointSixTwo
  72  have hpos : (0 : ℝ) < 2 * phi := by
  73    have : (0 : ℝ) < phi := Constants.phi_pos
  74    linarith
  75  refine ⟨?lo, ?hi⟩
  76  · rw [lt_div_iff₀ hpos]
  77    nlinarith [h_lo, h_hi]
  78  · rw [div_lt_iff₀ hpos]
  79    nlinarith [h_lo, h_hi]
  80
  81structure ClimatePredictabilityCert where
  82  unit_zero : forecastCost 1 = 0
  83  reciprocal_symm :
  84    ∀ {r : ℝ}, 0 < r → forecastCost r = forecastCost r⁻¹
  85  cost_nonneg : ∀ {r : ℝ}, 0 < r → 0 ≤ forecastCost r
  86  threshold_band :
  87    0.11 < PredictabilityThreshold ∧ PredictabilityThreshold < 0.13
  88  states_exclusive :
  89    ∀ {r : ℝ}, ¬ (IsWithinHorizon r ∧ IsPastHorizon r)
  90
  91/-- Climate-predictability-horizon certificate. -/
  92def climatePredictabilityCert : ClimatePredictabilityCert where
  93  unit_zero := forecastCost_zero_at_unit
  94  reciprocal_symm := forecastCost_reciprocal_symm
  95  cost_nonneg := forecastCost_nonneg
  96  threshold_band := predictability_threshold_band
  97  states_exclusive := horizon_states_exclusive
  98
  99end
 100end PredictabilityFromJCost
 101end Climate
 102end IndisputableMonolith
 103