J

formal source

  50
  51/-- J(x) = (1/2)(x + x⁻¹) − 1: the recognition cost functional.
  52    Defined for all reals (returns junk for x ≤ 0, but we only use x > 0). -/
  53noncomputable def J (x : ℝ) : ℝ := (1/2) * (x + x⁻¹) - 1
  54
  55theorem J_at_one : J 1 = 0 := by unfold J; norm_num
  56
  57/-- J(x) ≥ 0 for all x > 0 (AM-GM). -/
  58theorem J_nonneg (x : ℝ) (hx : 0 < x) : J x ≥ 0 := by
  59  unfold J
  60  have hxne : x ≠ 0 := ne_of_gt hx
  61  have hxx : x * x⁻¹ = 1 := mul_inv_cancel₀ hxne
  62  have hsq : 0 ≤ (x - x⁻¹) ^ 2 := sq_nonneg _
  63  have hexpand : (x - x⁻¹) ^ 2 = x ^ 2 - 2 + x⁻¹ ^ 2 := by
  64    have : (x - x⁻¹) ^ 2 = x ^ 2 - 2 * (x * x⁻¹) + x⁻¹ ^ 2 := by ring
  65    rw [hxx] at this; linarith
  66  have hge : x ^ 2 + x⁻¹ ^ 2 ≥ 2 := by nlinarith
  67  have hfactor : x + x⁻¹ ≥ 2 := by
  68    nlinarith [sq_nonneg (x + x⁻¹), sq_nonneg (x - x⁻¹)]
  69  linarith
  70
  71/-- J(x) = 0 ⟹ x = 1 (for x > 0). -/
  72theorem J_eq_zero_imp_one (x : ℝ) (hx : 0 < x) (hJ : J x = 0) : x = 1 := by
  73  unfold J at hJ
  74  have hsum : x + x⁻¹ = 2 := by linarith
  75  have hxx : x * x⁻¹ = 1 := mul_inv_cancel₀ (ne_of_gt hx)
  76  have hinv : x⁻¹ = 2 - x := by linarith
  77  have : x * x⁻¹ = x * (2 - x) := by rw [hinv]
  78  rw [hxx] at this
  79  nlinarith [this]
  80
  81/-- **B-20 DERIVED**: Non-triviality is a consequence of T1 + T5.
  82    Any transition with x = 1 has zero cost and leaves no ledger record.
  83    Therefore identity transitions are excluded from the physical event count. -/