self_recognition_zero_cost

formal source

  22  LedgerForcing.J e.ratio
  23
  24/-- Recognition events with ratio = 1 are cost-free. -/
  25theorem self_recognition_zero_cost (e : LedgerForcing.RecognitionEvent) :
  26    e.ratio = 1 → recognition_cost e = 0 := by
  27  intro h
  28  simp only [recognition_cost, h, LedgerForcing.J]
  29  norm_num
  30
  31/-- Non-trivial recognition has positive cost.
  32    Uses the fact that J(x) = (x + 1/x)/2 - 1 ≥ 0, with = 0 iff x = 1. -/
  33theorem nontrivial_recognition_positive_cost (e : LedgerForcing.RecognitionEvent)
  34    (h : e.ratio ≠ 1) : recognition_cost e > 0 := by
  35  simp only [recognition_cost, LedgerForcing.J]
  36  have hpos := e.ratio_pos
  37  have h0 : e.ratio ≠ 0 := hpos.ne'
  38  -- (x - 1)² > 0 when x ≠ 1
  39  have hne : (e.ratio - 1)^2 > 0 := by
  40    have hsq : (e.ratio - 1)^2 ≥ 0 := sq_nonneg _
  41    have hne2 : (e.ratio - 1)^2 ≠ 0 := by
  42      intro heq
  43      have heq2 : e.ratio - 1 = 0 := sq_eq_zero_iff.mp heq
  44      have : e.ratio = 1 := by linarith
  45      exact h this
  46    exact lt_of_le_of_ne hsq (Ne.symm hne2)
  47  -- Expand: x² - 2x + 1 > 0
  48  -- So: x² + 1 > 2x
  49  -- So: (x² + 1)/x > 2 (since x > 0)
  50  -- So: x + 1/x > 2
  51  have h2 : e.ratio^2 + 1 > 2*e.ratio := by nlinarith [sq_nonneg (e.ratio - 1)]
  52  have h3 : e.ratio + e.ratio⁻¹ > 2 := by
  53    have heq : e.ratio + e.ratio⁻¹ = (e.ratio^2 + 1) / e.ratio := by field_simp
  54    rw [heq, gt_iff_lt, lt_div_iff₀ hpos]
  55    linarith