IndisputableMonolith.Papers.GCIC.GraphRigidity

   1import Mathlib
   2import IndisputableMonolith.Cost
   3
   4/-!
   5# Graph Rigidity for Ratio Energy (GCIC Paper, Result 1)
   6
   7Machine-verified proof that on any finite connected graph,
   8the ratio energy C_G[x] = Σ J(x_v/x_w) vanishes if and only if
   9x is a constant positive field.
  10
  11## Main results
  12
  13* `eq_of_reflTransGen` — if a function agrees on related pairs, it agrees
  14  on the reflexive-transitive closure.
  15* `ratio_rigidity` — zero ratio energy on a connected graph forces constancy.
  16* `ratio_rigidity_iff` — full iff characterization (Result 1 of the GCIC paper).
  17
  18## Reference
  19
  20Thapa–Washburn, "Rigidity and Compact Phase Emergence in Scale-Invariant
  21Ratio-Based Energies" (2026), Result 1.
  22-/
  23
  24namespace IndisputableMonolith.Papers.GCIC.GraphRigidity
  25
  26open IndisputableMonolith.Cost
  27
  28variable {V : Type*}
  29
  30/-! ### Propagation along the reflexive-transitive closure -/
  31
  32/-- If a real-valued function agrees on all R-related pairs,
  33    it agrees on the reflexive-transitive closure of R.
  34    This is the graph-theoretic core: local agreement propagates globally. -/
  35theorem eq_of_reflTransGen {R : V → V → Prop} {f : V → ℝ}
  36    (hadj : ∀ a b, R a b → f a = f b) {u v : V}
  37    (huv : Relation.ReflTransGen R u v) : f u = f v := by
  38  induction huv with
  39  | refl => rfl
  40  | tail _ hbc ih => exact ih.trans (hadj _ _ hbc)
  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)
  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,
  98   fun hconst v w _ => constant_implies_zero_cost (hconst v w) (hpos w)⟩
  99
 100/-! ### Corollary: edge cost characterizations -/
 101
 102/-- J(x_v/x_w) = 0 iff x_v = x_w, for positive x. -/
 103theorem edge_cost_zero_iff {x : V → ℝ} {v w : V}
 104    (hv : 0 < x v) (hw : 0 < x w) :
 105    Jcost (x v / x w) = 0 ↔ x v = x w := by
 106  constructor
 107  · intro h
 108    have h1 := Jcost_zero_iff_one (div_pos hv hw) h
 109    rwa [div_eq_iff (ne_of_gt hw), one_mul] at h1
 110  · intro h
 111    rw [h, div_self (ne_of_gt hw)]
 112    exact Jcost_unit0
 113
 114end IndisputableMonolith.Papers.GCIC.GraphRigidity
 115