info_cost_zero_iff_unit

formal source

  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).
  84    Recognizing x from 1 costs the same as recognizing 1/x from 1.
  85    This is the "ledger balance" principle — recognition is bidirectional. -/
  86theorem info_cost_symmetric (e : RecognitionEvent) :
  87    infoCost e = infoCost ⟨e.ratio⁻¹, inv_pos.mpr e.ratio_pos⟩ := by
  88  unfold infoCost
  89  exact Jcost_symm e.ratio_pos
  90
  91/-! ## §II. The Minimum-Information State -/
  92