sphereArea
sphereArea supplies the Euclidean surface area of a sphere with radius r as 4πr². Researchers working on holographic bounds in Recognition Science cite this definition when converting volume-based counting into area-based information limits. The implementation is a direct one-line transcription of the classical formula with no additional lemmas or reductions.
claimThe surface area of a sphere of radius $r$ equals $4πr^2$.
background
The module derives the holographic bound from ledger projection, where ledger entries are fundamentally two-dimensional surfaces and three-dimensional volume emerges only as a reconstruction. Key supporting structures include the J-cost minimization from PhysicsComplexityStructure, the spectral emergence of gauge content and three generations from SpectralEmergence, and the ledger factorization from DAlembert.LedgerFactorization. The local setting states that information is bounded by boundary area rather than interior volume, with one bit per Planck area on the surface.
proof idea
This is a direct definition that transcribes the classical surface area formula without invoking any upstream lemmas or tactics.
why it matters in Recognition Science
The definition feeds holographicRatio, information_scales_as_area, and DegreeOfFreedomCounting in the same module. These establish that information scales with area (R²) rather than volume (R³), supporting the ledger-projection derivation of the bound S ≤ A/(4 l_P²). It aligns with the framework's T8 forcing of D=3 dimensions and the eight-tick octave, closing one step in the QG-006 holographic derivation from the 2D ledger structure.
scope and limits
- Does not incorporate curvature or general-relativistic corrections to the area formula.
- Does not define or compute the Planck area or Planck length.
- Does not prove the holographic bound itself or the ledger-projection mechanism.
- Does not address black-hole saturation cases or quantum corrections to the bound.
formal statement (Lean)
80noncomputable def sphereArea (radius : ℝ) : ℝ := 4 * π * radius^2
proof body
Definition body.
81
82/-- Volume of a sphere. -/