planckLength
plain-language theorem explainer
planckLength supplies the Planck length l_P = sqrt(ħ G / c³) using RS-native constants. Workers on holographic entropy or black hole thermodynamics cite it to fix the area scale in S_BH = A / (4 l_P²). The definition is a direct one-line assignment from upstream constants without algebraic reduction.
Claim. $l_P := √(ℏ G / c³)$ where ℏ and G are the RS-native reduced Planck constant and gravitational constant.
background
The Bekenstein-Hawking module derives black hole thermodynamics from Recognition Science, with entropy proportional to horizon area rather than volume. Planck length enters as the yardstick that converts area into information capacity via the ledger. MODULE_DOC states the target: S_BH = k_B A / (4 l_P²) and T_H = ℏ c³ / (8π G M k_B).
proof idea
One-line definition that applies the standard Planck length formula using imported constants hbar and G.
why it matters
planckLength feeds planckArea, which is required for the entropy formula in EntanglementEntropy and the information bound in HolographicBound. It closes the step from RS constants (T5 J-uniqueness, T8 D=3, ħ = φ^{-5}, G = φ^5 / π) to the holographic principle. Downstream results quote the area scaling directly from this length.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.