ratio_rigidity

formal source

  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)
  75  have h1 : x v / x w = 1 := Jcost_zero_iff_one hdiv_pos (hzero v w hvw)
  76  rwa [div_eq_iff (ne_of_gt (hpos w)), one_mul] at h1
  77
  78/-- **Converse:** constant positive fields have zero ratio cost on every edge. -/
  79theorem constant_implies_zero_cost {x : V → ℝ} {v w : V}
  80    (h : x v = x w) (hw : 0 < x w) :
  81    Jcost (x v / x w) = 0 := by
  82  rw [h, div_self (ne_of_gt hw)]
  83  exact Jcost_unit0
  84
  85/-- **RESULT 1 — Full characterization (iff).**
  86
  87On a connected graph with a positive field x : V → ℝ_{>0}:
  88
  89  (∀ edges, J(x_v/x_w) = 0)  ↔  x is constant.
  90
  91This is the machine-verified version of Result 1. -/
  92theorem ratio_rigidity_iff {adj : V → V → Prop}
  93    (hconn : ∀ u v : V, Relation.ReflTransGen adj u v)
  94    {x : V → ℝ} (hpos : ∀ v, 0 < x v) :
  95    (∀ v w, adj v w → Jcost (x v / x w) = 0) ↔
  96    (∀ v w : V, x v = x w) :=
  97  ⟨ratio_rigidity hconn hpos,