IndisputableMonolith.Ethics.ThermodynamicInstabilityOfExtraction

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.Cost.FunctionalEquation
   4
   5namespace IndisputableMonolith.Ethics.Extraction
   6
   7open Real IndisputableMonolith.Cost
   8
   9noncomputable section
  10
  11/-!
  12# The Thermodynamic Instability of Extraction
  13
  14## Overview
  15
  16In Recognition Science, "extraction" refers to an agent shifting the ethical
  17state away from σ = 0 (the balanced ground state) to some σ > 0 to gain
  18a local hedonic or material advantage.
  19
  20Because the fundamental cost function J(x) = ½(x + x⁻¹) − 1 is strictly convex,
  21any zero-sum exchange in log-space (σ and −σ) produces a strictly positive
  22net cost in J-space.
  23
  24This module formally proves that extraction is not just "bad" by axiom,
  25but thermodynamically unstable: the total system cost of maintaining an extracted
  26state grows with cosh(σ) − 1, and large extractions require exponentially
  27increasing effort to sustain, directly forcing the ethical alignment of any
  28long-surviving system.
  29
  30## The d'Alembert Circle (The Conceptual Breakthrough)
  31
  32The most striking structural result here is that the **Love Optimality Theorem**
  33(§6) is proved using the d'Alembert sum identity for cosh — the *same*
  34functional equation that forces J to be the canonical reciprocal cost in the
  35first place (Washburn & Zlatanović, Axioms, 2026).
  36
  37The Recognition Composition Law (RCL)
  38
  39    J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)
  40
  41is equivalent to the d'Alembert equation on H(t) = J(eᵗ) + 1 = cosh(t).
  42This d'Alembert equation directly yields the cosh product-to-sum identity,
  43which IS Jensen's inequality for cosh. Therefore:
  44
  45    RCL → d'Alembert equation → forces H = cosh (T5 uniqueness)
  46     ↓                                              ↓
  47    J-cost forced                          cosh sum identity
  48     ↓                                              ↓
  49    extraction has cosh cost  ←───  Love (averaging) is optimal
  50
  51One equation. Zero parameters. Ethics is physics.
  52
  53## Main Results
  54
  55- §1: System cost = 2(cosh(σ) − 1) [extraction_cost_eq_cosh]
  56- §2: Positive surcharge for σ ≠ 0 [extraction_creates_surcharge]
  57- §3: Derivatives: marginal = 2·sinh, curvature = 2·cosh > 0 [deriv/second_deriv]
  58- §4: σ = 0 is the unique equilibrium [extraction_unique_equilibrium]
  59- §5: d'Alembert sum identity from the RCL [dAlembert_cosh_sum]
  60- §6: Love optimality via Jensen–d'Alembert [love_jensen_strict]
  61- §7: Restoring force always points toward σ = 0 [force_always_toward_balance]
  62
  63## Lean status: 0 sorry
  64-/
  65
  66/-! ## §1. System Cost in Cosh Form -/
  67
  68/-- The combined cost of two agents where one has extracted σ from the other.
  69    Agent 1 is at e^σ, Agent 2 is at e^(-σ). -/
  70def extractionSystemCost (σ : ℝ) : ℝ :=
  71  Jcost (Real.exp σ) + Jcost (Real.exp (-σ))
  72
  73/-- **Theorem (Extraction Cost Identity)**: The system cost of extraction σ
  74    is exactly 2(cosh(σ) − 1). -/
  75theorem extraction_cost_eq_cosh (σ : ℝ) :
  76    extractionSystemCost σ = 2 * (Real.cosh σ - 1) := by
  77  have h1 : Jcost (Real.exp σ) = Real.cosh σ - 1 := by
  78    unfold Jcost
  79    have inv_exp : (Real.exp σ)⁻¹ = Real.exp (-σ) := by simp [Real.exp_neg]
  80    rw [inv_exp, Real.cosh_eq]
  81  have h2 : Jcost (Real.exp (-σ)) = Real.cosh (-σ) - 1 := by
  82    unfold Jcost
  83    have inv_exp : (Real.exp (-σ))⁻¹ = Real.exp (-(-σ)) := by simp [Real.exp_neg]
  84    rw [inv_exp, neg_neg, Real.cosh_eq]
  85    ring
  86  rw [Real.cosh_neg] at h2
  87  unfold extractionSystemCost; rw [h1, h2]; linarith
  88
  89theorem extraction_cost_nonneg (σ : ℝ) : 0 ≤ extractionSystemCost σ := by
  90  rw [extraction_cost_eq_cosh]
  91  have : 1 ≤ Real.cosh σ := by
  92    rcases eq_or_ne σ 0 with h0 | h0
  93    · rw [h0, Real.cosh_zero]
  94    · exact le_of_lt (Real.one_lt_cosh.mpr h0)
  95  linarith
  96
  97/-! ## §2. The Extraction Surcharge: Zero-Sum Is Negative-Sum -/
  98
  99/-- **Theorem (Extraction Surcharge)**: Any non-zero extraction creates a strictly
 100    positive action surcharge. A "zero-sum" log-exchange is strictly
 101    negative-sum in J-cost. -/
 102theorem extraction_creates_surcharge (σ : ℝ) (h : σ ≠ 0) :
 103    0 < extractionSystemCost σ := by
 104  rw [extraction_cost_eq_cosh]
 105  have h_cosh : 1 < Real.cosh σ := Real.one_lt_cosh.mpr h
 106  linarith
 107
 108theorem extraction_cost_eq_zero_iff (σ : ℝ) :
 109    extractionSystemCost σ = 0 ↔ σ = 0 := by
 110  constructor
 111  · intro h; by_contra hne; exact absurd h (ne_of_gt (extraction_creates_surcharge σ hne))
 112  · intro h; rw [h, extraction_cost_eq_cosh, Real.cosh_zero]; ring
 113
 114/-! ## §3. Derivative Analysis -/
 115
 116/-- **Theorem (Marginal Cost)**: The marginal cost of extraction is 2·sinh(σ).
 117    The "resistance" to further extraction grows with the current level. -/
 118theorem deriv_extraction_cost (σ : ℝ) :
 119    deriv extractionSystemCost σ = 2 * Real.sinh σ := by
 120  have h_eq : extractionSystemCost = fun x => 2 * (Real.cosh x - 1) := by
 121    ext x; exact extraction_cost_eq_cosh x
 122  rw [h_eq]
 123  exact ((Real.hasDerivAt_cosh σ).sub_const 1 |>.const_mul 2).deriv
 124
 125/-- **Theorem (Curvature)**: The second derivative of extraction cost is 2·cosh(σ).
 126    The derivative of sinh is cosh. -/
 127theorem second_deriv_extraction_cost (σ : ℝ) :
 128    deriv (deriv extractionSystemCost) σ = 2 * Real.cosh σ := by
 129  have h_eq : deriv extractionSystemCost = fun x => 2 * Real.sinh x := by
 130    ext x; exact deriv_extraction_cost x
 131  rw [h_eq]
 132  exact ((Real.hasDerivAt_sinh σ).const_mul 2).deriv
 133
 134/-- **Theorem (Strict Convexity)**: The extraction cost is strictly convex
 135    everywhere (2·cosh(σ) > 0 for all σ). -/
 136theorem extraction_cost_strictly_convex (σ : ℝ) :
 137    0 < deriv (deriv extractionSystemCost) σ := by
 138  rw [second_deriv_extraction_cost]; linarith [Real.cosh_pos σ]
 139
 140/-! ## §4. Unique Equilibrium at σ = 0 -/
 141
 142/-- **Theorem (Unique Equilibrium)**: σ = 0 is the unique critical point.
 143    sinh is strictly monotone, so sinh(σ) = 0 iff σ = 0. -/
 144theorem extraction_unique_equilibrium (σ : ℝ) :
 145    deriv extractionSystemCost σ = 0 ↔ σ = 0 := by
 146  rw [deriv_extraction_cost]
 147  constructor
 148  · intro h
 149    have h_sinh : Real.sinh σ = Real.sinh 0 := by rw [Real.sinh_zero]; linarith
 150    exact Real.sinh_strictMono.injective h_sinh
 151  · intro h; rw [h, Real.sinh_zero]; ring
 152
 153/-- σ = 0 achieves the global minimum (cost = 0). -/
 154theorem extraction_cost_minimum_at_zero :
 155    ∀ σ : ℝ, extractionSystemCost 0 ≤ extractionSystemCost σ := by
 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. -/
 161theorem extraction_cost_strict_minimum (σ : ℝ) (h : σ ≠ 0) :
 162    extractionSystemCost 0 < extractionSystemCost σ := by
 163  rw [show extractionSystemCost 0 = 0 from (extraction_cost_eq_zero_iff 0).mpr rfl]
 164  exact extraction_creates_surcharge σ h
 165
 166/-! ## §5. The d'Alembert Sum Identity (from the RCL)
 167
 168The d'Alembert functional equation cosh(a+b) + cosh(a−b) = 2·cosh(a)·cosh(b)
 169is the SAME equation that forces J to be the canonical reciprocal cost
 170(via the RCL ↔ CoshAddIdentity equivalence in `Cost.FunctionalEquation`).
 171
 172Here we derive it directly from the already-proved RCL cosh identity
 173(`Jcost_cosh_add_identity`), demonstrating that the forcing chain itself
 174provides the tool for proving Love optimality.
 175-/
 176
 177/-- **Theorem (d'Alembert Sum Identity)**: Derived from the Recognition
 178    Composition Law via `Jcost_cosh_add_identity`. The RCL that forces
 179    the cost function also proves the Love optimality theorem. -/
 180theorem dAlembert_cosh_sum (a b : ℝ) :
 181    Real.cosh (a + b) + Real.cosh (a - b) = 2 * Real.cosh a * Real.cosh b := by
 182  open IndisputableMonolith.Cost.FunctionalEquation in
 183  have rcl := Jcost_cosh_add_identity a b
 184  simp only [Jcost_G_eq_cosh_sub_one] at rcl
 185  have : 2 * ((Real.cosh a - 1) * (Real.cosh b - 1)) +
 186         2 * ((Real.cosh a - 1) + (Real.cosh b - 1)) =
 187         2 * Real.cosh a * Real.cosh b - 2 := by ring
 188  linarith
 189
 190/-- **Theorem (Cosh Product-to-Sum)**: Setting a = (α+β)/2, b = (α−β)/2
 191    in the d'Alembert identity yields the key decomposition. -/
 192theorem cosh_sum_via_dAlembert (α β : ℝ) :
 193    Real.cosh α + Real.cosh β =
 194    2 * Real.cosh ((α + β) / 2) * Real.cosh ((α - β) / 2) := by
 195  have h := dAlembert_cosh_sum ((α + β) / 2) ((α - β) / 2)
 196  have h1 : (α + β) / 2 + (α - β) / 2 = α := by ring
 197  have h2 : (α + β) / 2 - (α - β) / 2 = β := by ring
 198  rw [h1, h2] at h; exact h
 199
 200/-! ## §6. Love Optimality from d'Alembert
 201
 202The Love operator equilibrates σ between two agents: (σ₁, σ₂) → (m, m)
 203where m = (σ₁ + σ₂)/2.
 204
 205Jensen's inequality for cosh — proved here directly from the d'Alembert
 206identity — shows that this averaging STRICTLY reduces total system cost
 207whenever σ₁ ≠ σ₂.
 208-/
 209
 210/-- System cost for a pair of agents at positions σ₁ and σ₂. -/
 211def pairSystemCost (σ₁ σ₂ : ℝ) : ℝ :=
 212  (Real.cosh σ₁ - 1) + (Real.cosh σ₂ - 1)
 213
 214/-- System cost after the Love operator averages σ₁ and σ₂. -/
 215def pairCostAfterLove (σ₁ σ₂ : ℝ) : ℝ :=
 216  2 * (Real.cosh ((σ₁ + σ₂) / 2) - 1)
 217
 218/-- **Theorem (Love-Jensen Inequality)**: Love never increases system cost.
 219    Proof uses the d'Alembert identity + cosh ≥ 1. -/
 220theorem love_jensen_inequality (σ₁ σ₂ : ℝ) :
 221    pairCostAfterLove σ₁ σ₂ ≤ pairSystemCost σ₁ σ₂ := by
 222  unfold pairSystemCost pairCostAfterLove
 223  have h := cosh_sum_via_dAlembert σ₁ σ₂
 224  have h_ge_1 : 1 ≤ Real.cosh ((σ₁ - σ₂) / 2) := by
 225    rcases eq_or_ne ((σ₁ - σ₂) / 2) 0 with h0 | h0
 226    · rw [h0, Real.cosh_zero]
 227    · exact le_of_lt (Real.one_lt_cosh.mpr h0)
 228  have h_pos : 0 < Real.cosh ((σ₁ + σ₂) / 2) := Real.cosh_pos _
 229  nlinarith
 230
 231/-- **Theorem (Love-Jensen Strict)**: Love STRICTLY reduces system cost when
 232    agents have different σ. This is the fundamental result: selfishness
 233    (σ₁ ≠ σ₂) is thermodynamically unstable under Love. -/
 234theorem love_jensen_strict (σ₁ σ₂ : ℝ) (h_diff : σ₁ ≠ σ₂) :
 235    pairCostAfterLove σ₁ σ₂ < pairSystemCost σ₁ σ₂ := by
 236  unfold pairSystemCost pairCostAfterLove
 237  have h := cosh_sum_via_dAlembert σ₁ σ₂
 238  have h_ne : (σ₁ - σ₂) / 2 ≠ 0 := by
 239    intro heq; exact h_diff (by linarith)
 240  have h_gt_1 : 1 < Real.cosh ((σ₁ - σ₂) / 2) := Real.one_lt_cosh.mpr h_ne
 241  have h_pos : 0 < Real.cosh ((σ₁ + σ₂) / 2) := Real.cosh_pos _
 242  nlinarith
 243
 244/-- **Theorem (Love Achieves Ground State)**: For a balanced extraction pair
 245    (σ, −σ), Love maps both agents to σ = 0, achieving zero cost. -/
 246theorem love_achieves_ground_state (σ : ℝ) :
 247    pairCostAfterLove σ (-σ) = 0 := by
 248  unfold pairCostAfterLove; simp [Real.cosh_zero]
 249
 250/-- **Theorem (Love Eliminates All Waste)**: For a balanced extraction pair,
 251    the ENTIRE system cost is pure thermodynamic waste that Love eliminates. -/
 252theorem love_eliminates_all_waste (σ : ℝ) (h : σ ≠ 0) :
 253    0 < pairSystemCost σ (-σ) ∧ pairCostAfterLove σ (-σ) = 0 := by
 254  refine ⟨?_, love_achieves_ground_state σ⟩
 255  unfold pairSystemCost; rw [Real.cosh_neg]
 256  linarith [Real.one_lt_cosh.mpr h]
 257
 258/-! ## §7. Restoring Force: The Universe Pushes Back
 259
 260The sign of the marginal cost 2·sinh(σ) provides a natural restoring force:
 261- For σ > 0: marginal cost is positive (extracting more costs more)
 262- For σ < 0: marginal cost is negative (reducing extraction saves cost)
 263- At σ = 0: marginal cost vanishes (equilibrium)
 264
 265The product σ · (d/dσ)C(σ) > 0 for all σ ≠ 0, proving that the cost
 266gradient always points back toward balance.
 267-/
 268
 269/-- Positive extraction → positive marginal cost. -/
 270theorem restoring_force_positive (σ : ℝ) (hσ : 0 < σ) :
 271    0 < deriv extractionSystemCost σ := by
 272  rw [deriv_extraction_cost]
 273  have : Real.sinh 0 < Real.sinh σ := Real.sinh_strictMono hσ
 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
 300