local_determines_global
plain-language theorem explainer
On a connected graph where J-cost vanishes on every edge, any positive real field x must be constant, so the value at one vertex fixes the value at all others. Researchers deriving holographic properties for brain models from GCIC would cite this as the local-global information step. The proof is a direct one-line application of the ratio_rigidity result that converts zero edge costs plus connectivity into global constancy.
Claim. Let $G=(V,E)$ be a connected graph with adjacency relation adj. Let $x:V→ℝ$ be a positive function such that $J(x(v)/x(w))=0$ for every adjacent pair $(v,w)$. Then for any vertices $v_0,v∈V$, $x(v)=x(v_0)$.
background
J-cost is the Recognition Science cost function whose unique zero occurs at argument 1, forcing equal field values across edges when the cost vanishes. The module derives brain holography from GCIC by chaining T5 (J-uniqueness) through graph rigidity to local-global information transfer. ratio_rigidity states: on a connected graph, if the ratio cost J(x_v/x_w) vanishes on every edge, then the positive field x is constant. Its proof sketch notes that J=0 implies x_v/x_w=1 and connectivity propagates the equality to all pairs.
proof idea
This is a one-line wrapper that applies ratio_rigidity, supplying the connectivity hypothesis, positivity condition, and zero-cost edge condition to obtain x(v)=x(v₀) for the chosen vertices.
why it matters
The declaration occupies the Local-Global Information Theorem position in the GCIC-to-holography chain. It follows directly from T5 via GCIC Graph Rigidity and supplies the premise for boundary_encodes_bulk and holographic_cache_from_gcic. Within the Recognition framework it realizes the information-theoretic core of holography, where every connected subgraph encodes the global ledger state and thereby forces surface-area scaling in D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.