constant_of_preconnected
plain-language theorem explainer
If a real-valued function on vertices agrees on every pair related by R and the reflexive-transitive closure of R connects every pair of vertices, then the function is constant on the whole vertex set. Authors proving rigidity for ratio energies on graphs cite this step when showing that vanishing edge costs force global constancy. The proof is a one-line term application of the auxiliary lemma eq_of_reflTransGen to the adjacency agreement and connectivity hypotheses.
Claim. Let $V$ be a vertex set and $R$ a binary relation on $V$. If the reflexive-transitive closure of $R$ relates every pair of vertices and a map $f: V → ℝ$ satisfies $f(a) = f(b)$ whenever $R(a,b)$, then $f(v) = f(w)$ for all $v,w ∈ V$.
background
The module establishes graph rigidity for ratio energy, defined as the sum of J-costs J(x_v/x_w) over edges of a graph. Preconnectivity means the reflexive-transitive closure of the adjacency relation relates every vertex pair. The auxiliary result eq_of_reflTransGen states that agreement on R-related pairs extends to agreement on the full reflexive-transitive closure.
proof idea
The proof is a one-line term-mode wrapper. It introduces the target vertices v and w, then applies eq_of_reflTransGen directly to the adjacency agreement hypothesis and the connectivity witness from the reflexive-transitive closure.
why it matters
This supplies the propagation step for the forward direction of ratio_rigidity, which is Result 1 of the GCIC paper (Thapa–Washburn 2026) showing zero ratio energy on a connected graph forces a constant positive field. It feeds the iff characterization in ratio_rigidity_iff and aligns with J-uniqueness in the Recognition Science forcing chain, where J(r) = 0 only at r = 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.