planckLength
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the numerical value from hbar, G or c.
- Does not place the length in natural units where l_P = 1.
- Does not carry uncertainty intervals or approximation provenance.
- Does not reference Recognition Science constants such as phi or the forcing chain.
formal statement (Lean)
51noncomputable def planckLength : ℝ := 1.6e-35 -- meters
proof body
Definition body.
52
53/-- Planck area = l_P². -/