J_zero_iff_one

formal source

  92lemma J_at_one : J 1 = 0 := by unfold J; norm_num
  93
  94/-- J(x) = 0 iff x = 1 (for positive x). -/
  95lemma J_zero_iff_one {x : ℝ} (hx : 0 < x) : J x = 0 ↔ x = 1 := by
  96  constructor
  97  · intro h
  98    unfold J at h
  99    have hx_ne : x ≠ 0 := hx.ne'
 100    have h1 : x + x⁻¹ = 2 := by linarith
 101    have h2 : x * (x + x⁻¹) = x * 2 := by rw [h1]
 102    have h3 : x^2 + 1 = 2 * x := by field_simp at h2; linarith
 103    nlinarith [sq_nonneg (x - 1)]
 104  · intro h; rw [h]; exact J_at_one
 105
 106/-- J is positive for x ≠ 1. -/
 107lemma J_pos_of_ne_one {x : ℝ} (hx : 0 < x) (hne : x ≠ 1) : 0 < J x := by
 108  have h := J_nonneg hx
 109  cases' h.lt_or_eq with hlt heq
 110  · exact hlt
 111  · exfalso; exact hne ((J_zero_iff_one hx).mp heq.symm)
 112
 113/-! ## Transition Cost -/
 114
 115/-- The cost of transitioning from configuration x to configuration y.
 116
 117    This is the "action" for a direct transition, defined as the average
 118    cost along the transition weighted by the magnitude of change.
 119
 120    J_transition(x,y) = |ln(y/x)| · (J(x) + J(y)) / 2
 121
 122    Key properties:
 123    - J_transition(x,x) = 0 (no change = no cost)
 124    - J_transition(x,y) = J_transition(y,x) (symmetric)
 125    - J_transition(x,1) = |ln x| · J(x) / 2 (approaching identity is cheap for x ≈ 1) -/