`volume`

definition

show as: view math explainer →

module: IndisputableMonolith.Papers.GCIC.BrainHolography
domain: Papers
line: 178 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Papers.GCIC.BrainHolography on GitHub at line 178.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 175  (S.filter (fun v => ∃ w ∈ Sᶜ, adj v w)).card
 176
 177/-- Volume of a region: number of vertices. -/
 178def volume {V : Type*} (S : Finset V) : ℕ := S.card
 179
 180/-- In any cache, every boundary node determines the global field.
 181    Therefore, the number of independent "information channels" to the
 182    global state equals the surface area (boundary node count), not
 183    the volume (total node count).
 184
 185    This theorem proves information scales with boundary size. -/
 186theorem info_scales_with_boundary {V : Type*} (cache : LocalCache V) :
 187    ∀ (b₁ b₂ : V),
 188    IsBoundary cache.adj cache.cache_nodes b₁ →
 189    IsBoundary cache.adj cache.cache_nodes b₂ →
 190    cache.field b₁ = cache.field b₂ := by
 191  intro b₁ b₂ _ _
 192  exact ratio_rigidity cache.graph_connected cache.field_positive
 193    cache.at_J_minimum b₁ b₂
 194
 195/-! ## Part 5: Partial Removal Resilience (Hemispherectomy Prediction)
 196
 197The holographic property has a dramatic consequence: removing part of a
 198connected cache preserves full information access, as long as the remainder
 199stays connected. This is because any single remaining vertex determines the
 200entire global field.
 201
 202Empirically confirmed: hemispherectomy patients (half the brain removed)
 203retain consciousness and memories. RS predicts this is not surprising but
 204FORCED by the holographic structure of J-cost-optimal caches. -/
 205
 206/-- **PARTIAL REMOVAL PRESERVES INFORMATION**: If a subset of cache nodes
 207    is removed and the remainder is still connected and at J-minimum,
 208    then every remaining node still determines the full global field.

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.