ClimatePhasePoint

formal source

  27
  28/-- A point in climate phase space (idealized as a real-valued
  29    state vector with N components). -/
  30abbrev ClimatePhasePoint (N : ℕ) := Fin N → ℝ
  31
  32/-- The J-cost of a climate state (sum of per-component costs). -/
  33def climateJCost {N : ℕ} (s : ClimatePhasePoint N) : ℝ :=
  34  Finset.univ.sum fun i => Cost.Jcost (1 + (s i)^2)
  35
  36/-- The climate cost is non-negative. -/
  37theorem climateJCost_nonneg {N : ℕ} (s : ClimatePhasePoint N) :
  38    0 ≤ climateJCost s := by
  39  unfold climateJCost
  40  apply Finset.sum_nonneg
  41  intro i _
  42  apply Cost.Jcost_nonneg
  43  positivity
  44
  45/-- The vacuum climate state (all components zero) has J-cost zero
  46    (the unforced equilibrium). -/
  47theorem vacuum_climate_zero_cost {N : ℕ} :
  48    climateJCost (fun _ : Fin N => (0 : ℝ)) = 0 := by
  49  unfold climateJCost
  50  apply Finset.sum_eq_zero
  51  intro i _
  52  simp [Cost.Jcost_unit0]
  53
  54/-- **MASTER THEOREM**: the vacuum state is the global J-cost
  55    minimum of climate phase space. -/
  56theorem vacuum_is_global_minimum {N : ℕ} (s : ClimatePhasePoint N) :
  57    climateJCost (fun _ : Fin N => (0 : ℝ)) ≤ climateJCost s := by
  58  rw [vacuum_climate_zero_cost]
  59  exact climateJCost_nonneg s
  60