sphereVolume
plain-language theorem explainer
Sphere volume supplies the classical Euclidean formula V = (4/3)πr³ for use in holographic comparisons. Researchers deriving information bounds from ledger projections cite it to contrast naive interior scaling with boundary dominance. The definition is a direct noncomputable abbreviation of the standard expression with no further reduction or lemmas.
Claim. The volume of a sphere of radius $r$ is $V = (4/3) π r^3$.
background
The HolographicBound module derives the holographic principle from Recognition Science ledger structure, where entries live on surfaces and volume is reconstructed. Core setup contrasts volume V = (4/3)πR³ with surface area A = 4πR², yielding the bound S ≤ A/(4 l_P²). Upstream structures include PhiForcingDerived.of for J-cost calibration and SimplicialLedger.ContinuumBridge.as for Laplacian identification of ledger action with simplex volumes.
proof idea
The definition is a one-line noncomputable abbreviation that directly encodes the classical sphere volume formula.
why it matters
sphereVolume feeds holographicRatio and holographic_ratio_scales, which establish the area-to-volume ratio scaling as 3/R and thereby the surface dominance of ledger information. It fills the volume term in the QG-006 paper derivation of holography from ledger projection, linking to T8 forcing of D = 3 spatial dimensions and the eight-tick octave. It touches the open question of how 3D volume emerges from 2D ledger data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.