planckArea
plain-language theorem explainer
Planck area is defined as the square of the Planck length, supplying the fundamental area scale of approximately 2.6 × 10^{-70} m². Black hole thermodynamics and holographic bound researchers cite it when writing entropy as proportional to horizon area. The definition is a direct algebraic squaring of the upstream Planck length expression.
Claim. The Planck area satisfies $l_P^2 = l_P^2$ where the Planck length is $l_P = √(ℏG/c³).
background
The module derives black hole thermodynamics from Recognition Science, targeting Bekenstein-Hawking entropy S_BH = k_B A / (4 l_P²) and Hawking temperature. Planck length is defined upstream as √(ℏG/c³) with G from Constants as λ_rec² c³ / (π ℏ). This sets the scale for holographic bounds where entropy scales with area rather than volume.
proof idea
One-line definition that squares the planckLength value from the same module.
why it matters
It supplies the denominator for bekensteinHawkingEntropy and entropy_proportional_to_area, which establish entropy proportional to area. This fills the QG-001 result in the module and supports the holographic principle in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.