Jcost

formal source

  30
  31/-- The J-cost function: J(x) = ½(x + 1/x) - 1 for x > 0.
  32    This is the unique cost functional forced by the Recognition Composition Law. -/
  33def Jcost (x : ℝ) : ℝ := (x + x⁻¹) / 2 - 1
  34
  35theorem Jcost_nonneg (x : ℝ) (hx : 0 < x) : 0 ≤ Jcost x := by
  36  unfold Jcost
  37  have hx_ne : x ≠ 0 := ne_of_gt hx
  38  suffices h : x + x⁻¹ ≥ 2 by linarith
  39  rw [ge_iff_le, ← sub_nonneg]
  40  have : x + x⁻¹ - 2 = (x ^ 2 - 2 * x + 1) / x := by field_simp; ring
  41  rw [this]
  42  apply div_nonneg _ (le_of_lt hx)
  43  nlinarith [sq_nonneg (x - 1)]
  44
  45theorem Jcost_zero_iff_one (x : ℝ) (hx : 0 < x) : Jcost x = 0 ↔ x = 1 := by
  46  constructor
  47  · intro h
  48    unfold Jcost at h
  49    have : x + x⁻¹ = 2 := by linarith
  50    have hx_ne : x ≠ 0 := ne_of_gt hx
  51    have : x ^ 2 - 2 * x + 1 = 0 := by
  52      field_simp at this ⊢; nlinarith
  53    have : (x - 1) ^ 2 = 0 := by nlinarith
  54    have : x - 1 = 0 := by nlinarith [sq_nonneg (x - 1)]
  55    linarith
  56  · intro h; subst h; unfold Jcost; simp
  57
  58/-- J-cost exact identity: J(1 + ε) = ε²/(2(1+ε)) for ε > -1.
  59    This is the bridge between J-cost and the Hamiltonian (kinetic energy ≈ ε²/2). -/
  60theorem Jcost_one_plus_exact (ε : ℝ) (hε : -1 < ε) :
  61    Jcost (1 + ε) = ε ^ 2 / (2 * (1 + ε)) := by
  62  unfold Jcost
  63  have h1ε : (0 : ℝ) < 1 + ε := by linarith