volume
plain-language theorem explainer
Volume of a finite vertex set S is defined as its cardinality. In the GCIC brain holography derivation, this counting function lets theorems contrast boundary node count against total nodes to establish surface-area scaling of information. The definition is the standard Finset cardinality operation and requires no additional lemmas.
Claim. For a finite set $S$ of vertices, the volume is the cardinality $|S|$.
background
The Brain Holography module derives that brains function as holographic caches under Recognition Science principles. Local regions are finite sets of vertices in the ledger graph, with volume counting all vertices and surface area counting only boundary vertices. Upstream, J-cost minimization from PhiForcingDerived and LedgerFactorization forces global constancy on connected components, making boundary encoding possible. The module doc states that information scales with boundary size in D=3, following from T5 J-uniqueness through graph rigidity.
proof idea
The definition is a direct abbreviation: volume S equals the cardinality of S. It applies the built-in Finset.card without invoking any Recognition Science lemmas.
why it matters
This definition supports the parent results local_determines_global and info_scales_with_boundary in the same module, which establish the holographic property and boundary scaling. It fills the counting step in the derivation chain from GCIC to surface-area scaling in three dimensions. Downstream uses appear in action convexity and observability limits to handle volume terms in physical bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.