info_scales_with_boundary
plain-language theorem explainer
In a J-cost minimal local cache on a connected graph, all boundary vertices carry identical field values. Neuroscientists modeling brain as holographic cache and physicists deriving surface-area scaling of information would cite this. The proof is a one-line application of ratio_rigidity to any pair of boundary nodes using connectedness, positivity, and J-minimum.
Claim. Let $C$ be a local cache: a nonempty connected subgraph with positive field $f: V → ℝ$ at J-minimum. For any two boundary vertices $b_1, b_2$ (each in the cache set and adjacent to a vertex outside it), $f(b_1) = f(b_2)$.
background
LocalCache is a structure on vertex type V with adjacency relation, reflexive-transitive connectedness, positive real field, nonempty cache node set, and the at_J_minimum condition that Jcost(f(v)/f(w)) = 0 on every internal edge. IsBoundary selects vertices inside the cache set that touch the complement. The module derives brain holography from GCIC by chaining T5 J-uniqueness through graph rigidity to the local-global information theorem, where every connected subgraph vertex determines the global field.
proof idea
The proof introduces the two boundary nodes b1 and b2, then applies the ratio_rigidity lemma from GraphRigidity using the cache's graph_connected, field_positive, and at_J_minimum fields.
why it matters
This realizes the surface-area scaling step in the derivation chain to brain_holography_inevitable. It embeds the holographic principle (boundary encodes bulk) inside Recognition Science, tying directly to D=3 and the partial removal resilience result that predicts hemispherectomy preserves function. The declaration closes the information-scaling link between LocalCache and the eight-tick octave geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.