pith. machine review for the scientific record. sign in
def definition def or abbrev high

maxInformation

show as:
view Lean formalization →

The maxInformation definition supplies the upper bound on bits contained inside a region whose boundary has area A, computed as A divided by four Planck areas. Quantum gravity and holographic principle researchers would cite this quantity when bounding entropy from discrete ledger models. The definition is a direct algebraic scaling that follows immediately from the imported Planck area constant.

claimThe maximum information content (in bits) storable in a region with positive boundary area $A$ is $I(A) = A / (4 A_P)$, where $A_P$ is the Planck area.

background

The HolographicBound module derives the holographic principle from Recognition Science ledger projection: ledger entries are fundamentally two-dimensional surfaces, volume is reconstructed from boundary data, and information is limited to one bit per Planck area. The active edge count per tick is fixed at 1 by the IntegrationGap.A and Masses.Anchor.A definitions. Planck area itself is imported from the BekensteinHawking submodule as the fundamental area unit in RS-native units.

proof idea

One-line definition that divides the supplied area by four times the planckArea constant.

why it matters in Recognition Science

This definition supplies the information bound used to prove black holes saturate the entropy limit (black_hole_maximal) and that information scales with area rather than volume (information_scales_as_area). It realizes the QG-006 target of obtaining S ≤ A/(4 l_P²) from ledger structure, consistent with the eight-tick octave and D = 3 spatial dimensions in the Recognition Science forcing chain.

scope and limits

formal statement (Lean)

  63noncomputable def maxInformation (area : ℝ) (ha : area > 0) : ℝ :=

proof body

Definition body.

  64  area / (4 * planckArea)
  65
  66/-- **THEOREM**: The holographic bound is S ≤ A/(4l_P²). -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (11)

Lean names referenced from this declaration's body.