planckLength
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 in Recognition Science
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.
scope and limits
- Does not derive the Planck length from the forcing chain axioms.
- Does not prove minimality of this scale inside Recognition Science.
- Does not extend the formula to higher dimensions or modified gravity.
formal statement (Lean)
47noncomputable def planckLength : ℝ := Real.sqrt (hbar * G / c^3)
proof body
Definition body.
48
49/-- The Planck area l_P² ≈ 2.6 × 10⁻⁷⁰ m². -/