constant_implies_zero_cost
plain-language theorem explainer
If a positive scalar field takes the same value at two vertices, its ratio cost on the edge between them vanishes. This fact is cited in the full iff characterization of Result 1 from the GCIC paper on graph rigidity for ratio energies. The argument reduces the ratio argument to unity via substitution and applies the unit lemma for the cost function.
Claim. Let $x : V → ℝ_{>0}$ be a positive real-valued function on the vertices of a graph. If $x(v) = x(w)$ and $x(w) > 0$, then $J_{cost}(x(v)/x(w)) = 0$, where $J_{cost}$ is the ratio cost function satisfying $J_{cost}(1) = 0$.
background
The ratio energy on a finite graph is the sum over edges of $J_{cost}(x_v / x_w)$, with $J_{cost}(r) = (r-1)^2/(2r)$ for $r > 0$. This module proves that the energy vanishes if and only if the positive field $x$ is constant, on the assumption that the graph is connected via the reflexive-transitive closure of the adjacency relation. The local setting is therefore a finite connected graph equipped with a strictly positive vertex function.
proof idea
The proof is a one-line term-mode wrapper. It rewrites the ratio $x(v)/x(w)$ to 1 by substituting the equality hypothesis $x(v) = x(w)$, using positivity of $x(w)$ to justify the division, then applies the lemma Jcost_unit0 which states that $J_{cost}(1) = 0$.
why it matters
This supplies the converse direction for Result 1 of the GCIC paper (Thapa–Washburn 2026). It is invoked directly by the downstream theorem ratio_rigidity_iff to obtain the full equivalence between vanishing ratio energy on every edge and constancy of $x$. In the Recognition Science framework the result reinforces that J-cost measures deviation from the self-similar fixed point, here realized discretely on graphs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.