ratio_rigidity_iff
plain-language theorem explainer
The theorem states that on any connected graph a positive real-valued vertex function has vanishing J-cost on every edge if and only if the function is constant. Researchers citing the GCIC paper on ratio-energy rigidity would invoke this as the machine-verified form of Result 1. The proof is a one-line term wrapper that pairs the forward rigidity implication with the converse for constants.
Claim. Let $G=(V,E)$ be a graph whose adjacency relation has reflexive-transitive closure equal to the full relation on $V$. For any positive function $x:V→ℝ_{>0}$, the condition $J(x(v)/x(w))=0$ for every adjacent pair $(v,w)$ holds if and only if $x$ is constant on $V$.
background
The module develops graph rigidity for the ratio energy $C_G[x]=∑J(x_v/x_w)$ on finite connected graphs. Here $J$ denotes the J-cost function $J(r)=(r+r^{-1})/2-1$ that appears throughout Recognition Science as the unique cost satisfying the multiplicative composition law. The upstream lemma constant_implies_zero_cost shows that any constant positive field yields zero J-cost on edges; the sibling lemma ratio_rigidity supplies the converse direction under the connectivity hypothesis.
proof idea
The proof is a direct term-mode construction of the biconditional. It applies ratio_rigidity (under the given connectivity and positivity hypotheses) to obtain the forward implication, then uses constant_implies_zero_cost on the constant case to obtain the reverse implication, packaging both directions into a single ⟨·,·⟩ pair.
why it matters
This supplies the complete if-and-only-if statement that is Result 1 of the Thapa–Washburn GCIC paper. It anchors the analysis of scale-invariant ratio energies by showing that only constant fields achieve zero ratio cost on connected graphs, consistent with the J-uniqueness property (T5) and the self-similar fixed-point structure (T6) of the Recognition framework. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.