edge_deviation_small

formal source

  65    _ = 4 * δ * (1 + δ) := by ring
  66
  67/-- For small δ (≤ 1), the edge deviation simplifies to (r-1)² ≤ 8δ. -/
  68theorem edge_deviation_small {r : ℝ} (hr : 0 < r) {δ : ℝ} (hδ : 0 ≤ δ)
  69    (hδ_small : δ ≤ 1) (hJ : Jcost r ≤ δ) : (r - 1) ^ 2 ≤ 8 * δ := by
  70  have h := edge_deviation_bound hr hδ hJ
  71  calc (r - 1) ^ 2 ≤ 4 * δ * (1 + δ) := h
  72    _ ≤ 4 * δ * (1 + 1) := by nlinarith
  73    _ = 8 * δ := by ring
  74
  75/-- Absolute deviation bound: |r - 1| ≤ √(8δ) for δ ≤ 1. -/
  76theorem abs_deviation_small {r : ℝ} (hr : 0 < r) {δ : ℝ} (hδ : 0 ≤ δ)
  77    (hδ_small : δ ≤ 1) (hJ : Jcost r ≤ δ) :
  78    |r - 1| ≤ Real.sqrt (8 * δ) := by
  79  have hsq := edge_deviation_small hr hδ hδ_small hJ
  80  have h8δ_nn : 0 ≤ 8 * δ := by nlinarith
  81  rw [← Real.sqrt_sq (abs_nonneg (r - 1))]
  82  apply Real.sqrt_le_sqrt
  83  rw [sq_abs]
  84  exact hsq
  85
  86/-! ## Part 2: Exact Case Recovery -/
  87
  88/-- **EXACT CASE RECOVERY**: When δ = 0, approximate holography recovers
  89    exact holography (GCIC rigidity). -/
  90theorem exact_case_recovery {V : Type*} {adj : V → V → Prop}
  91    (hconn : ∀ u v : V, Relation.ReflTransGen adj u v)
  92    {x : V → ℝ} (hpos : ∀ v, 0 < x v)
  93    (hcost : ∀ v w, adj v w → Jcost (x v / x w) ≤ 0)
  94    (v w : V) : x v = x w := by
  95  have h0 : ∀ v w, adj v w → Jcost (x v / x w) = 0 := by
  96    intro v w hvw
  97    have hle := hcost v w hvw
  98    have hge := Jcost_nonneg (div_pos (hpos v) (hpos w))