boundary_encodes_bulk
plain-language theorem explainer
On a connected graph at J-minimum, the field value at any boundary vertex of a subregion fixes the value at every vertex in the graph. This is the core statement of the holographic principle extracted from GCIC rigidity. Researchers deriving holographic properties of local caches or brains from first principles would cite it. The proof applies the ratio rigidity lemma in one step.
Claim. Let $(V, adj)$ be a connected graph. Let $x: V → ℝ_{>0}$ satisfy $J(x(v)/x(w)) = 0$ for every adjacent pair. For any subset $S ⊆ V$ and boundary vertex $b ∈ S$ (adjacent to some vertex outside $S$), $x(w) = x(b)$ for all $w ∈ V$.
background
The module derives brain holography from RS principles via the chain T5 (J-uniqueness) to GCIC graph rigidity to local-global information theorems. A local cache is a nonempty connected subgraph where internal J-costs vanish. The IsBoundary predicate marks vertices in S adjacent to the complement. Upstream graph rigidity results establish that zero J-cost plus connectedness forces the field x to be constant.
proof idea
This is a one-line wrapper that applies the ratio_rigidity lemma to the connectedness, positivity, and zero-cost hypotheses, equating the value at the boundary vertex b to that at arbitrary w.
why it matters
It supplies the boundary-encodes-bulk step in the derivation chain leading to brain_holography_inevitable. The result realizes the holographic principle as a direct consequence of J-cost zero on connected graphs, feeding into surface-area scaling for D=3. It closes part of the local-to-global information flow in the GCIC framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.