bitsPerPlanckArea
plain-language theorem explainer
The declaration sets the information density to one bit per Planck area in the Recognition Science ledger model. Physicists deriving holographic entropy bounds from boundary projections would cite this constant when linking area to information content. It is supplied as a direct noncomputable definition without intermediate lemmas or reductions.
Claim. The information density is one bit per Planck area: $b = 1$.
background
The module Quantum.HolographicBound derives the holographic principle from ledger projection in Recognition Science. Ledger entries reside on 2D surfaces, so volume is reconstructed from boundary data and information scales with area A rather than volume V. This yields the bound S ≤ A / (4 l_P²) in native units where c = 1 and ħ = φ^{-5}.
proof idea
This is a direct definition that assigns the constant value 1. No lemmas from upstream structures such as LedgerFactorization or SpectralEmergence are invoked; the assignment stands alone as the base density for subsequent holographic statements.
why it matters
The constant anchors the QG-006 holographic bound derived from ledger structure and supplies the unit density used in the downstream EntanglementEntropy module to obtain the coefficient 1/4 in S = A / (4 l_P²). It realizes the 2D ledger insight at D = 3 and connects to the eight-tick octave via the 8/2 = 4 relation noted in the downstream documentation. The precise mapping from 8-tick dynamics to the entropy factor remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.