planckArea
plain-language theorem explainer
The Planck area is introduced as the square of the Planck length to serve as the fundamental area scale in Recognition Science. Holographic principle derivations and black hole entropy calculations cite this when bounding information by boundary area. The definition proceeds by direct algebraic squaring of the Planck length constant.
Claim. The Planck area is given by $l_P^2$, where $l_P$ denotes the Planck length.
background
The HolographicBound module derives the holographic principle from Recognition Science ledger projection, where ledger entries are fundamentally two-dimensional and volume emerges from boundary data. The Planck length is the fundamental length scale imported from Constants, and this definition sets the area unit for entropy calculations. Upstream results include the structure of J-cost minimization from PhiForcingDerived, the ledger factorization from DAlembert, and the gauge content plus three generations from SpectralEmergence.
proof idea
The definition is a one-line wrapper that squares the Planck length imported from the BekensteinHawking module.
why it matters
This supplies the area unit for the Bekenstein-Hawking entropy theorem and the entanglement entropy minimal surface calculations. It fills the holographic bound step in the QG-006 derivation, linking to the ledger factorization and the area-proportional entropy result. The framework landmark is the emergence of D=3 spatial dimensions from the eight-tick octave in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.