balanced_has_minimum_cost

formal source

  95
  96/-- **THEOREM IC-001.5**: The balanced state (x = 1) has the minimum information cost.
  97    J(1) = 0 ≤ J(x) for all x > 0. -/
  98theorem balanced_has_minimum_cost (e : RecognitionEvent) :
  99    infoCost balancedEvent ≤ infoCost e := by
 100  unfold infoCost balancedEvent
 101  rw [Jcost_unit0]
 102  exact Jcost_nonneg e.ratio_pos
 103
 104/-- **THEOREM IC-001.6**: The balanced state is the unique minimum.
 105    It is the only state where no additional information is encoded. -/
 106theorem balanced_is_unique_minimum (e : RecognitionEvent) (h : infoCost e = infoCost balancedEvent) :
 107    e.ratio = 1 := by
 108  unfold infoCost balancedEvent at h
 109  rw [Jcost_unit0] at h
 110  exact (info_cost_zero_iff_unit e).mp h
 111
 112/-! ## §III. Nothingness is Infinitely Costly -/
 113
 114/-- **THEOREM IC-001.7**: For any bound M, there exist recognition events with cost > M.
 115    More specifically: the event with ratio x = 1/(2(|M|+2)) has cost > M.
 116    This proves J(x) → ∞ as x → 0⁺, i.e., "nothingness" is infinitely expensive. -/
 117theorem nothingness_infinite_cost :
 118    ∀ M : ℝ, ∃ x : ℝ, 0 < x ∧ Jcost x > M := by
 119  intro M
 120  have hK_pos : (0 : ℝ) < |M| + 2 := by linarith [abs_nonneg M]
 121  have hK_ne : |M| + 2 ≠ 0 := hK_pos.ne'
 122  refine ⟨1 / (2 * (|M| + 2)), div_pos one_pos (by linarith), ?_⟩
 123  unfold Jcost
 124  have hinv : (1 / (2 * (|M| + 2)))⁻¹ = 2 * (|M| + 2) := by
 125    field_simp [hK_ne]
 126  rw [hinv]
 127  have h_expand : (1 / (2 * (|M| + 2)) + 2 * (|M| + 2)) / 2 - 1 =
 128                  1 / (4 * (|M| + 2)) + |M| + 1 := by