sphereArea
plain-language theorem explainer
Sphere area supplies the Euclidean surface formula 4πr² for spherical regions inside the holographic bound module. Researchers deriving the area-law information bound from ledger projection cite it to convert boundary measure into maximum bit count. The definition is a direct noncomputable transcription of the classical formula with no lemmas or reductions.
Claim. The surface area of a sphere of radius $r$ is given by $A = 4\pi r^2$.
background
The module derives the holographic principle S ≤ A/(4 l_P²) from the claim that ledger entries are fundamentally two-dimensional while three-dimensional volume is reconstructed. Sphere area supplies the boundary measure A that appears in the information bound and in the sibling definitions planckArea and maxInformation. Upstream structures from SpectralEmergence and PhysicsComplexityStructure establish the emergence of three spatial dimensions and the convexity of J-cost, but the present definition remains the standard Euclidean expression.
proof idea
One-line definition that directly transcribes the classical sphere surface area formula.
why it matters
The definition is invoked by holographicRatio, information_scales_as_area, and DegreeOfFreedomCounting to establish that information capacity scales with R² rather than R³. It supplies the geometric ingredient for the ledger-projection argument in the PRD paper on holography. It touches the open question of how the two-dimensional ledger projects to an emergent three-dimensional interior.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.