planckArea
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the numerical value of the Planck length in SI units.
- Does not address curvature corrections or higher-genus surfaces.
- Does not encode the full Ryu-Takayanagi minimal-surface construction.
- Does not specify the conversion factor between RS-native and laboratory units.
Lean usage
theorem entropy_proportional_to_area (bh : BlackHole) : bekensteinHawkingEntropy bh = k_B * horizonArea bh / (4 * planckArea) := rflformal statement (Lean)
60noncomputable def planckArea : ℝ := planckLength^2
proof body
Definition body.
61
62/-! ## The Bekenstein-Hawking Entropy -/
63
64/-- The Bekenstein-Hawking entropy of a black hole.
65 S_BH = A / (4 × l_p²) = A / (4 G_N ℏ / c³) -/