LocalCache
The LocalCache structure assembles a connected graph on vertices V together with a positive real field whose adjacent ratios lie at J-cost zero. Recognition Science researchers cite it when deriving that any local brain region encodes the full global ledger state. The definition directly packages connectivity, positivity, nonempty cache nodes, and the zero-cost edge condition to serve as the hypothesis carrier for rigidity results.
claimA structure on a type $V$ consisting of an adjacency relation $adj : V → V → Prop$, the connectedness condition that the reflexive-transitive closure of $adj$ relates every pair of vertices, a field map $f : V → ℝ$ satisfying $f(v) > 0$ for all $v$, a nonempty subset $C ⊆ V$ of cache nodes, and the J-minimum condition that $J(f(v)/f(w)) = 0$ whenever $adj(v,w)$ holds.
background
In Recognition Science, J-cost is the function $J(x) = ½(x + x^{-1}) - 1$ with unique zero at $x = 1$ (T5). The module models neural tissue as a local cache: a nonempty connected subgraph whose internal edges incur zero J-cost, forcing the field to be constant throughout the component. This encodes the Local Cache Theorem that every vertex inside the cache determines the global field value.
proof idea
The declaration is a structure definition that packages the six fields: adjacency, reflexive-transitive connectivity, positive field, nonempty cache nodes, and the at_J_minimum predicate on adjacent pairs. No proof body is present; the structure acts as the hypothesis carrier for downstream applications of ratio_rigidity.
why it matters in Recognition Science
LocalCache supplies the central carrier for the Local Cache Theorem and feeds brain_holography_inevitable, holographic_cache_from_gcic, cache_nodes_uniform, info_scales_with_boundary, and partial_removal_preserves_info. It closes the step from GCIC graph rigidity to surface-area scaling in D=3, confirming that accessible information equals boundary size rather than volume and thereby derives Bentov's holographic-brain claim from T5 plus connectedness.
scope and limits
- Does not assert existence of any nonempty connected cache at J-minimum.
- Does not specify the spatial dimension D of the underlying manifold.
- Does not quantify over possible field values beyond strict positivity.
- Does not address time evolution or dynamics of the cache field.
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. -/