ClimatePredictabilityCert

formal source

  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