edge_cost_zero_iff
plain-language theorem explainer
The result states that for positive real values assigned to two vertices, the recognition cost J of their ratio vanishes precisely when the values are identical. Authors working on scale-invariant ratio energies on graphs cite it as a local building block. The proof is a direct bidirectional application of the zero-cost characterization for J together with algebraic cancellation of the ratio.
Claim. Let $x: V → ℝ$ be a vertex function with $x(v)>0$ and $x(w)>0$. Then $J(x(v)/x(w))=0$ if and only if $x(v)=x(w)$.
background
The J-cost is the recognition cost function $J(y)=(y-1)^2/(2y)$ for $y>0$, equivalently $J(e^t)=cosh(t)-1$. The module develops graph rigidity for the ratio energy $C_G[x]=∑ J(x_v/x_w)$ on finite connected graphs, showing that this energy vanishes if and only if $x$ is a positive constant field. This local equivalence is used to pass from edge-wise zero cost to global constancy. Upstream, Jcost_zero_iff_one asserts that $J(y)=0$ with $y>0$ forces $y=1$, while Jcost_unit0 records the base case $J(1)=0$.
proof idea
The proof constructs the two directions of the biconditional. Forward direction applies Jcost_zero_iff_one to the positive ratio $x(v)/x(w)$ and rewrites the resulting equality $x(v)/x(w)=1$ via div_eq_iff and one_mul. Reverse direction substitutes the equality $x(v)=x(w)$ into the ratio, obtains 1, and invokes Jcost_unit0.
why it matters
This local equivalence supplies the edge-wise step needed for the global rigidity theorems in the same module, including ratio_rigidity and ratio_rigidity_iff (Result 1 of Thapa–Washburn 2026). It directly instantiates the uniqueness property of J from the forcing chain (T5) inside the graph setting. The declaration closes a small but necessary gap between the algebraic definition of J and the geometric conclusion that zero ratio energy forces constancy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.