ratio_rigidity
plain-language theorem explainer
On a connected graph, vanishing J-cost on every edge forces any positive vertex field to be constant. Holography derivations in the GCIC paper and brain models cite this to obtain global uniformity from local zero-cost conditions. The term-mode proof invokes the preconnected constancy lemma after reducing each adjacent ratio to unity via the unique zero of J.
Claim. Let $G=(V,adj)$ be a graph such that the reflexive-transitive closure of $adj$ relates every pair of vertices. Suppose $x:V→ℝ$ satisfies $0<x(v)$ for all $v$ and $J(x(v)/x(w))=0$ whenever $adj(v,w)$. Then $x(v)=x(w)$ for all $v,w∈V$.
background
The module establishes graph rigidity for ratio-based energies in the GCIC framework. The J-cost function satisfies $J(y)=0$ if and only if $y=1$ for $y>0$, as stated in Jcost_zero_iff_one. Connectivity is expressed via Relation.ReflTransGen adj, the smallest reflexive transitive relation containing adj. Upstream results include the definition of Jcost from the multiplicative recognizer and its equivalence to the hyperbolic cosine form.
proof idea
The proof is a one-line wrapper applying constant_of_preconnected to the connectivity hypothesis. For each adjacent pair, positivity of the ratio allows Jcost_zero_iff_one to conclude the ratio equals 1, after which algebraic rearrangement via div_eq_iff and one_mul yields equality of the field values.
why it matters
This theorem is Result 1 of the GCIC paper and supplies the rigidity step in multiple downstream derivations, including boundary_encodes_bulk and brain_holography_inevitable. It closes the gap from local J-minima to global constancy, enabling the holographic principle that boundary data determines the bulk. In the Recognition Science chain it rests on T5 uniqueness of J and feeds the eight-tick octave and D=3 emergence by ensuring uniform fields on connected structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.