planckLength
plain-language theorem explainer
Planck length is introduced as the characteristic scale sqrt(hbar G_N / c^3) using the module's constants. Researchers deriving holographic bounds or entanglement entropy in Recognition Science would reference this definition to connect quantum information to geometry. It is realized as a direct noncomputable real expression without further reduction.
Claim. $l_P = √(ℏ G_N / c³)$ where ℏ denotes the reduced Planck constant and G_N Newton's gravitational constant.
background
The module QG-008 derives the Ryu-Takayanagi formula from Recognition Science ledger structure, where entanglement entropy equals boundary area over 4 G_N ℏ because ledger entries are fundamentally two-dimensional. G_N is defined as Newton's constant in SI units and hbar as the reduced Planck constant in SI units, both imported from Constants. Upstream results supply hbar in RS-native units as φ^{-5} and in CODATA form, together with sibling planckLength definitions that use the same algebraic pattern.
proof idea
One-line definition that applies the real square root to the product of hbar, G_N and the reciprocal of c cubed.
why it matters
This definition supplies the length scale for the Planck area used in Bekenstein-Hawking entropy and holographic bounds. It fills the geometric foundation for the Ryu-Takayanagi formula in the QG-008 paper proposition. In the Recognition framework it anchors the area-law emergence from 2D ledger entries.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.