identity_config

formal source

  71def ConfigSpace : Set Config := {c | 0 < c.value}
  72
  73/-- The identity configuration (value = 1, minimal cost) -/
  74def identity_config (t : ℕ) : Config := ⟨1, one_pos, t, by simp [Real.log_one]⟩
  75
  76/-! ## Cost Functions for Modal Logic -/
  77
  78/-- The fundamental cost J(x) = ½(x + 1/x) - 1.
  79
  80    This is the unique cost satisfying d'Alembert + normalization + calibration (T5). -/
  81noncomputable def J (x : ℝ) : ℝ := (1/2) * (x + x⁻¹) - 1
  82
  83/-- J is non-negative for positive arguments. -/
  84lemma J_nonneg {x : ℝ} (hx : 0 < x) : 0 ≤ J x := by
  85  unfold J
  86  have hx_ne : x ≠ 0 := hx.ne'
  87  have h_rewrite : (1:ℝ)/2 * (x + x⁻¹) - 1 = (x - 1)^2 / (2 * x) := by field_simp; ring
  88  rw [h_rewrite]
  89  apply div_nonneg (sq_nonneg _) (by linarith : 0 ≤ 2 * x)
  90
  91/-- J(1) = 0 (the identity has zero cost). -/
  92lemma J_at_one : J 1 = 0 := by unfold J; norm_num
  93
  94/-- J(x) = 0 iff x = 1 (for positive x). -/
  95lemma J_zero_iff_one {x : ℝ} (hx : 0 < x) : J x = 0 ↔ x = 1 := by
  96  constructor
  97  · intro h
  98    unfold J at h
  99    have hx_ne : x ≠ 0 := hx.ne'
 100    have h1 : x + x⁻¹ = 2 := by linarith
 101    have h2 : x * (x + x⁻¹) = x * 2 := by rw [h1]
 102    have h3 : x^2 + 1 = 2 * x := by field_simp at h2; linarith
 103    nlinarith [sq_nonneg (x - 1)]
 104  · intro h; rw [h]; exact J_at_one