pith. machine review for the scientific record. sign in
def definition def or abbrev

volume

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 178def volume {V : Type*} (S : Finset V) : ℕ := S.card

proof body

Definition body.

 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. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (13)

Lean names referenced from this declaration's body.