eq_of_reflTransGen
plain-language theorem explainer
The theorem shows that if a real-valued function on vertices agrees on every pair related by a binary relation R, then the function takes the same value on any pair connected by the reflexive-transitive closure of R. Researchers proving rigidity of ratio energies on graphs cite it to convert local constancy into global constancy. The proof is by induction on the ReflTransGen relation, with the base case immediate and the successor step combining the inductive hypothesis with the adjacency agreement via transitivity of equality.
Claim. Let $R$ be a binary relation on a set $V$ and let $f:V→ℝ$ be a function such that $f(a)=f(b)$ whenever $R(a,b)$. Then $f(u)=f(v)$ for all $u,v$ related by the reflexive-transitive closure of $R$.
background
The GCIC module establishes that the ratio energy $C_G[x]=∑J(x_v/x_w)$ on a graph vanishes if and only if the positive field $x$ is constant, provided the graph is connected. Here $J$ is the recognition cost function from the Cost module, and $V$ is the abstract vertex set (the vantage type from the RRF glossary). The local theoretical setting is the machine-verified proof of Result 1 in Thapa–Washburn 2026 on rigidity and compact phase emergence in scale-invariant ratio-based energies.
proof idea
The proof is by induction on the hypothesis $huv$ that $u$ and $v$ are related by Relation.ReflTransGen $R$. The reflexive base case is discharged by reflexivity of equality. The tail case applies the inductive hypothesis to reach the intermediate vertex and then uses the given adjacency condition $hadj$ to equate the final step, combining the two equalities by transitivity.
why it matters
This lemma supplies the propagation step that lets local edge agreement imply global constancy, directly feeding the theorem constant_of_preconnected which states that every pair of vertices has equal function values under the preconnectedness assumption. It therefore underpins the main iff characterization ratio_rigidity_iff of the GCIC paper (Result 1). In the Recognition framework the lemma supports the emergence of compact phases by guaranteeing that zero ratio energy forces a constant field on connected components.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.