  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

papers checked against this theorem

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