OperationalForecastSkillCert

formal source

  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