planckArea
plain-language theorem explainer
planckArea supplies the fundamental surface scale l_P² used throughout Recognition Science derivations of black-hole and entanglement entropy. Researchers working on holographic bounds or the Ryu-Takayanagi formula cite it when converting geometric area into information counts. The definition is a direct one-line abbreviation that squares the Planck length imported from the Constants module.
Claim. The Planck area is defined by $l_P^2$, where $l_P$ is the Planck length in RS-native units with $c=1$ and $G_N = phi^5 / pi$.
background
The module Quantum.EntanglementEntropy develops QG-008, the derivation of the Ryu-Takayanagi formula from ledger projection. Ledger entries are treated as fundamentally two-dimensional; entanglement entropy counts shared entries across a boundary and therefore scales with area rather than volume. Upstream results supply the necessary scales: InitialCondition.entropy defines entropy as total defect, PhiForcingDerived.of and SpectralEmergence.of fix the phi-ladder and D=3 geometry, while Constants and Cost calibrate G_N and hbar in RS units.
proof idea
one-line wrapper that squares the imported planckLength value from the Constants module.
why it matters
This definition is the common unit that lets bekensteinHawkingEntropy, blackHoleEntropy, and minimalSurfaceArea realize the area-law entropy S = A / (4 l_P²). It directly supports the module's claim that both Bekenstein-Hawking and Ryu-Takayanagi entropies emerge from the same ledger-surface counting. The placement closes the geometric side of the holographic bound before the entropy theorems are stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.