vacuum_is_global_minimum

formal source

  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
  61/-- **MASTER CERTIFICATE.** -/
  62structure AttractorStructureCert where
  63  cost_nonneg : ∀ {N : ℕ} (s : ClimatePhasePoint N), 0 ≤ climateJCost s
  64  vacuum_zero : ∀ {N : ℕ}, climateJCost (fun _ : Fin N => (0 : ℝ)) = 0
  65  vacuum_minimum :
  66    ∀ {N : ℕ} (s : ClimatePhasePoint N),
  67      climateJCost (fun _ : Fin N => (0 : ℝ)) ≤ climateJCost s
  68
  69def attractorStructureCert : AttractorStructureCert where
  70  cost_nonneg := @climateJCost_nonneg
  71  vacuum_zero := @vacuum_climate_zero_cost
  72  vacuum_minimum := @vacuum_is_global_minimum
  73
  74end
  75
  76end AttractorStructure
  77end Climate
  78end IndisputableMonolith