edge_cost_nonneg
plain-language theorem explainer
The theorem establishes nonnegativity of the J-cost on ratios of a positive real-valued function at any two vertices. Researchers studying rigidity of scale-invariant energies on graphs would cite it as the basic positivity fact enabling propagation arguments. The proof is a one-line wrapper applying the known Jcost nonnegativity lemma to the positive quotient of the two values.
Claim. Let $x: V → ℝ$ with $x(v) > 0$ and $x(w) > 0$ for vertices $v, w ∈ V$. Then $J(x(v)/x(w)) ≥ 0$, where $J$ is the cost function satisfying $J(y) ≥ 0$ for all $y > 0$.
background
The module develops machine-verified results on ratio energy $C_G[x] = ∑ J(x_v/x_w)$ for finite connected graphs, showing it vanishes if and only if the positive field $x$ is constant. This is Result 1 of the referenced Thapa–Washburn paper on rigidity and compact phase emergence in scale-invariant ratio-based energies. The J-cost is the Recognition Science cost function whose nonnegativity follows from the AM-GM inequality.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_nonneg (from the Cost module) to the positive quotient produced by div_pos hv hw.
why it matters
This positivity fact is the first step in the forward direction of the GCIC paper's rigidity theorem: zero edge costs imply equal values at adjacent vertices, which then propagate to constancy on connected graphs via the reflexive-transitive closure lemma. It rests on the upstream Jcost_nonneg result and supports the full iff characterization ratio_rigidity_iff. The setting aligns with the Recognition Science J-uniqueness property used throughout the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.