structure
definition
def or abbrev
LocalCache
show as:
view Lean formalization →
formal statement (Lean)
136structure LocalCache (V : Type*) where
137 adj : V → V → Prop
138 graph_connected : ∀ u v : V, Relation.ReflTransGen adj u v
139 field : V → ℝ
140 field_positive : ∀ v, 0 < field v
141 cache_nodes : Set V
142 cache_nonempty : cache_nodes.Nonempty
143 at_J_minimum : ∀ v w, adj v w → Jcost (field v / field w) = 0
144
145/-- **HOLOGRAPHIC CACHE FROM GCIC**: Any local cache on a connected graph
146 at J-minimum is holographic: every node in the cache determines the
147 entire global field, and in particular the boundary encodes the bulk.
148
149 This derives Bentov's claim that the brain is a hologram. -/