abs_deviation_small

formal source

  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))
  99    linarith
 100  exact GraphRigidity.ratio_rigidity hconn hpos h0 v w
 101
 102/-! ## Part 3: Continuity Certificate -/
 103
 104/-- **CONTINUITY IN δ**: The exact case (δ=0) gives exact constancy.
 105    The approximate case (δ>0) gives bounded deviation.
 106    The transition is continuous. -/