No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
154theorem extraction_cost_minimum_at_zero :
155 ∀ σ : ℝ, extractionSystemCost 0 ≤ extractionSystemCost σ := by
proof body
Term-mode proof.
156 intro σ
157 rw [show extractionSystemCost 0 = 0 from (extraction_cost_eq_zero_iff 0).mpr rfl]
158 exact extraction_cost_nonneg σ
159
160/-- σ = 0 is the STRICT global minimum for σ ≠ 0. -/
depends on (9)
Lean names referenced from this declaration's body.
-
extraction_cost_eq_zero_iff
in IndisputableMonolith.Ethics.ThermodynamicInstabilityOfExtraction
decl_use
-
extraction_cost_nonneg
in IndisputableMonolith.Ethics.ThermodynamicInstabilityOfExtraction
decl_use
-
extractionSystemCost
in IndisputableMonolith.Ethics.ThermodynamicInstabilityOfExtraction
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
from
in IndisputableMonolith.Foundation.PrimitiveDistinction
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use