`restoring_force_negative`

proved

show as: view math explainer →

module: IndisputableMonolith.Ethics.ThermodynamicInstabilityOfExtraction
domain: Ethics
line: 277 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Ethics.ThermodynamicInstabilityOfExtraction on GitHub at line 277.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 274  simp only [Real.sinh_zero] at this; linarith
 275
 276/-- Negative extraction → negative marginal cost. -/
 277theorem restoring_force_negative (σ : ℝ) (hσ : σ < 0) :
 278    deriv extractionSystemCost σ < 0 := by
 279  rw [deriv_extraction_cost]
 280  have : Real.sinh σ < Real.sinh 0 := Real.sinh_strictMono hσ
 281  simp only [Real.sinh_zero] at this; linarith
 282
 283/-- **Theorem (Universal Restoring Force)**: For any σ ≠ 0, the product
 284    σ · C'(σ) > 0, meaning the cost gradient always opposes the extraction.
 285    The universe structurally resists imbalance. -/
 286theorem force_always_toward_balance (σ : ℝ) (hσ : σ ≠ 0) :
 287    0 < σ * deriv extractionSystemCost σ := by
 288  rw [deriv_extraction_cost]
 289  rcases lt_or_gt_of_ne hσ with h_neg | h_pos
 290  · have h_sinh : Real.sinh σ < 0 := by
 291      have := Real.sinh_strictMono h_neg; simp only [Real.sinh_zero] at this; linarith
 292    nlinarith
 293  · have h_sinh : 0 < Real.sinh σ := by
 294      have := Real.sinh_strictMono h_pos; simp only [Real.sinh_zero] at this; linarith
 295    nlinarith
 296
 297end
 298
 299end IndisputableMonolith.Ethics.Extraction

papers checked against this theorem

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