IsBoundary
plain-language theorem explainer
IsBoundary defines a vertex v as a boundary vertex of subregion S under adjacency adj when v lies inside S and shares an edge with at least one vertex outside S. Researchers deriving holographic encoding from graph rigidity in Recognition Science cite this predicate to formalize the interface between local caches and the global ledger. The definition is a direct logical conjunction of membership and external adjacency with no further conditions imposed.
Claim. Let $G=(V, E)$ be a graph with adjacency relation $E$. For a subset $Ssubseteq V$ and vertex $v in V$, $v$ is a boundary vertex of $S$ if $v in S$ and there exists $w notin S$ such that $v$ is adjacent to $w$.
background
In the Brain Holography from GCIC module, graphs represent ledger states at J-minimum. Here J is the unique cost function fixed by T5 as $J(x) = (x + x^{-1})/2 - 1$, with zero only at $x=1$. IsBoundary supplies the topological interface predicate between a local cache (subregion S) and its complement. Upstream results include GCIC graph rigidity (zero J-cost on connected graphs forces constant field) and the LocalCacheForcing structures that treat brains as J-optimal connected subgraphs. The module derivation chain runs T5 (J unique) to GCIC rigidity to local-global information to holographic cache to surface-area scaling in D=3.
proof idea
This is a direct definition. The predicate holds exactly when the vertex satisfies set membership in S together with the existence of an adjacent vertex outside S. No lemmas or tactics are invoked; the definition serves as the primitive boundary predicate for all downstream statements.
why it matters
The definition anchors the holographic principle inside the Recognition framework. It is invoked directly by boundary_encodes_bulk (any boundary vertex determines the global field at J-minimum), by info_scales_with_boundary (information channels equal boundary size), and by the master certificate brain_holography_inevitable. It completes the step from local cache to surface-area scaling (D=3) in the module chain and thereby links T5 J-uniqueness to the claim that brain holography is forced. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.