extractionSystemCost

formal source

  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