Jcost_zero_iff_one

formal source

  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
  64  have h1ε_ne : (1 + ε) ≠ 0 := ne_of_gt h1ε
  65  field_simp
  66  ring
  67
  68/-- For small ε, J(1+ε) ≈ ε²/2. Specifically, the ratio approaches 1. -/
  69theorem Jcost_quadratic_ratio (ε : ℝ) (hε_neg : -1 < ε) (hε_pos : 0 < ε) :
  70    Jcost (1 + ε) ≤ ε ^ 2 / 2 := by
  71  rw [Jcost_one_plus_exact ε hε_neg]
  72  apply div_le_div_of_nonneg_left (sq_nonneg ε) (by positivity) (by nlinarith)
  73
  74/-! ## 2. Energy Density = Processing Potential -/
  75