forecastCost

formal source

  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