infoCost

formal source

  50  ratio_pos : ratio > 0
  51
  52/-- The information cost of a recognition event = J(x). -/
  53noncomputable def infoCost (e : RecognitionEvent) : ℝ := Jcost e.ratio
  54
  55/-- **THEOREM IC-001.1**: Every recognition event has non-negative information cost.
  56    J(x) ≥ 0 for all x > 0. This follows from AM-GM: (x + 1/x)/2 ≥ 1. -/
  57theorem info_cost_nonneg (e : RecognitionEvent) : infoCost e ≥ 0 :=
  58  Jcost_nonneg e.ratio_pos
  59
  60/-- **THEOREM IC-001.2**: Information cost is zero iff the ratio is 1.
  61    J(x) = 0 ↔ x = 1 — the unique balanced/zero-defect state. -/
  62theorem info_cost_zero_iff_unit (e : RecognitionEvent) :
  63    infoCost e = 0 ↔ e.ratio = 1 := by
  64  unfold infoCost
  65  constructor
  66  · intro h
  67    rw [Jcost_eq_sq e.ratio_pos.ne'] at h
  68    have hden_pos : 0 < 2 * e.ratio := by linarith [e.ratio_pos]
  69    have hden_ne : (2 * e.ratio) ≠ 0 := ne_of_gt hden_pos
  70    have hsq : (e.ratio - 1) ^ 2 = 0 := by
  71      rwa [div_eq_zero_iff, or_iff_left hden_ne] at h
  72    nlinarith [sq_nonneg (e.ratio - 1)]
  73  · intro h; rw [h]; exact Jcost_unit0
  74
  75/-- **THEOREM IC-001.3**: Any ratio x ≠ 1 carries strictly positive information cost.
  76    J(x) > 0 for all x > 0, x ≠ 1. -/
  77theorem info_cost_pos_of_ne_one (e : RecognitionEvent) (hne : e.ratio ≠ 1) :
  78    infoCost e > 0 := by
  79  have hzero := (info_cost_zero_iff_unit e).not.mpr hne
  80  have hnn := info_cost_nonneg e
  81  exact lt_of_le_of_ne hnn (Ne.symm hzero)
  82
  83/-- **THEOREM IC-001.4**: Information cost is symmetric: J(x) = J(1/x).