boundaryArea
plain-language theorem explainer
The declaration supplies the spherical boundary area A(L) = 4πL² used to bound holographic information capacity for a conscious extent. Workers deriving maintenance budgets or critical extents in the Consciousness Bandwidth setting cite it when converting area into event counts. The definition is a direct one-line expression of the standard surface-area formula in three dimensions.
Claim. The boundary area for a spherical extent of radius $L$ is given by $A(L) = 4πL^2$.
background
The Consciousness Bandwidth module models a conscious boundary of spatial extent L that persists for a fixed barrier period of 360 ticks. Its information budget is set by the holographic capacity S_holo = L² / (4ℓ_P²), while maintenance demand scales with the J-cost integrated over that period. The present definition supplies the L² factor that converts extent into available recognition events via N_budget(L) = boundaryArea(L) / (4ℓ_P² · k_R).
proof idea
Direct definition implementing the classical surface-area formula for a sphere. No lemmas or tactics are invoked; the expression is primitive and is unfolded by the three downstream results that establish positivity, monotonicity, and the budget function.
why it matters
boundaryArea supplies the area term required by maintenanceBudget and by the monotonicity and positivity theorems that support existence of a critical extent L_crit. It realizes the L² scaling of holographic capacity on a three-dimensional boundary, consistent with the forced D = 3 that follows from the eight-tick octave in the Unified Forcing Chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.