planckLength
plain-language theorem explainer
The Planck length is defined as the square root of ħG over c cubed, the characteristic scale where quantum effects and gravity become comparable. Researchers in quantum gravity and black hole thermodynamics cite this when normalizing areas for entropy calculations and information bounds. The definition is a direct one-line encoding of the classical formula using the Recognition Science values for ħ and G.
Claim. $l_P := √(ℏ G / c³) ≈ 1.616 × 10^{-35}$ m
background
The module targets QG-009 and QG-010: deriving Planck length, mass, and time from Recognition Science principles. The Planck scale marks the intersection of quantum mechanics and gravity, with the length given by the supplied formula. In RS, this scale connects to the base time τ₀ and the self-similar fixed point φ via l_P = c τ₀ φ^{-n} for an appropriate rung n on the phi ladder. Upstream, ħ is defined as φ^{-5} in native units while G is obtained from the J-cost functional equation as λ_rec² c³ / (π ħ).
proof idea
One-line definition that directly transcribes the standard Planck length expression using the imported constants ħ and G.
why it matters
This supplies the base length for the Planck area used in Bekenstein-Hawking entropy S_BH = A / (4 l_P²) and holographic information bounds. It advances the module target of expressing Planck quantities through RS-native constants tied to J-uniqueness and the phi forcing chain. Downstream declarations in entanglement entropy and recognition bandwidth apply this scale directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.