subgraph_determines_global
plain-language theorem explainer
On a connected graph with positive vertex weights x where adjacent ratios have vanishing J-cost, any vertex inside a nonempty connected subgraph fixes the value of x everywhere. Researchers deriving holographic properties of local caches or brain models from GCIC would cite the result to show local ledger regions encode global state. The proof is a one-line wrapper applying the ratio-rigidity lemma to the representative vertex inside the subgraph.
Claim. Let $(V, adj)$ be a graph whose reflexive-transitive closure connects every pair of vertices. Let $x: V → ℝ_{>0}$ satisfy $J(x(v)/x(w)) = 0$ whenever $adj(v,w)$ holds. Then for any nonempty $S ⊆ V$, any $v_{in} ∈ S$, and any $w ∈ V$, one has $x(w) = x(v_{in})$.
background
J-cost is the function $J(r) = (r + r^{-1})/2 - 1$, which vanishes precisely when $r = 1$ (T5 J-uniqueness). The local setting is the GCIC derivation of brain holography: graph rigidity at J-minimum forces constancy on connected components, so every local region encodes the global ledger state. The module imports GraphRigidity and states the chain T5 → GCIC Graph Rigidity → Local-Global Information Theorem → boundary encodes bulk.
proof idea
The proof is a one-line wrapper that applies the ratio_rigidity lemma to the connectivity hypothesis, positivity, and zero J-cost condition, using the chosen representative $v_{in}$ inside $S$.
why it matters
This fills the Local-Global Information Theorem step in the GCIC-to-holography chain (T5 J-uniqueness → GCIC Graph Rigidity → subgraph constancy → holographic cache). It feeds boundary_encodes_bulk and holographic_cache_from_gcic, which establish that accessible information scales with surface area in D=3 rather than volume. The result touches the open question of how partial removal of vertices (hemispherectomy) preserves function while the remainder stays connected.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.