constant_of_preconnected

formal source

  41
  42/-- On a preconnected graph (every pair related by ReflTransGen),
  43    agreement on edges implies global constancy. -/
  44theorem constant_of_preconnected {R : V → V → Prop}
  45    (hconn : ∀ u v : V, Relation.ReflTransGen R u v) {f : V → ℝ}
  46    (hadj : ∀ a b, R a b → f a = f b) :
  47    ∀ v w : V, f v = f w := by
  48  intro v w
  49  exact eq_of_reflTransGen hadj (hconn v w)
  50
  51/-! ### Ratio rigidity (Result 1) -/
  52
  53/-- Edge cost is nonneg for positive fields. -/
  54theorem edge_cost_nonneg {x : V → ℝ} {v w : V}
  55    (hv : 0 < x v) (hw : 0 < x w) :
  56    0 ≤ Jcost (x v / x w) :=
  57  Jcost_nonneg (div_pos hv hw)
  58
  59/-- **RESULT 1 — Forward direction (Finite-Volume Rigidity).**
  60
  61On a connected graph, if the ratio cost J(x_v/x_w) vanishes on every edge,
  62then the positive field x is constant.
  63
  64Proof sketch:
  651. J(x_v/x_w) = 0 implies x_v/x_w = 1, i.e. x_v = x_w (unique zero of J).
  662. Connectivity propagates edge-wise agreement to all vertex pairs. -/
  67theorem ratio_rigidity {adj : V → V → Prop}
  68    (hconn : ∀ u v : V, Relation.ReflTransGen adj u v)
  69    {x : V → ℝ} (hpos : ∀ v, 0 < x v)
  70    (hzero : ∀ v w, adj v w → Jcost (x v / x w) = 0) :
  71    ∀ v w : V, x v = x w := by
  72  apply constant_of_preconnected hconn
  73  intro v w hvw
  74  have hdiv_pos : 0 < x v / x w := div_pos (hpos v) (hpos w)