planckLength
plain-language theorem explainer
The declaration supplies the numerical Planck length 1.6e-35 m for scaling holographic information bounds in the ledger-projection setting. Quantum-gravity researchers deriving area-law entropy or entanglement bounds cite it to normalize surface data. Implementation is a direct constant assignment with no algebraic reduction or lemma calls.
Claim. The Planck length is the constant $l_P = 1.6times 10^{-35}$ meters.
background
The module derives the holographic bound S ≤ A/(4 l_P²) from Recognition Science ledger structure: ledger entries are fundamentally two-dimensional, three-dimensional volume is reconstructed from boundary data, and information is limited to one bit per Planck area. Planck length sets the absolute scale separating ledger bits from emergent geometry. Upstream definitions in BekensteinHawking, EntanglementEntropy and PlanckScale compute the same quantity as sqrt(hbar G / c³) or sqrt(hbar G_N / c³); this module instead records the accepted numerical value in SI units for immediate use in area and entropy expressions.
proof idea
One-line definition that directly assigns the floating-point constant 1.6e-35 to the real number planckLength.
why it matters
Provides the length unit required by every downstream area and entropy definition inside the module (planckArea, bitsPerPlanckArea, holographic_bound). It anchors the QG-006 derivation of the holographic principle from ledger projection and supplies the normalization used by Bekenstein-Hawking and entanglement-entropy results. The choice of numerical value rather than symbolic expression keeps the holographic bound statements concrete while remaining consistent with the RS constants imported from the Constants module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.