`vacuum_climate_zero_cost`

proved

show as: view math explainer →

module: IndisputableMonolith.Climate.AttractorStructure
domain: Climate
line: 47 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Climate.AttractorStructure on GitHub at line 47.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  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
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.