module module high

`IndisputableMonolith.Quantum.HolographicBound`

This module defines the holographic bound and supporting quantities such as Planck length and area in RS-native units. Quantum gravity and information theorists would cite it when embedding holographic principles inside Recognition Science. The module is purely definitional with no theorems or proofs.

claimPlanck length $l_P = 1$ (natural units); holographic bound states maximum information scales as boundary area divided by four Planck areas; related quantities include Planck area, bits per Planck area, Bekenstein bound, and sphere area/volume.

background

The module sits in the Quantum domain and imports Constants, whose sole documented content is the RS time quantum τ₀ = 1 tick. Its DOC_COMMENT anchors the central convention that Planck length equals unity in these units. Sibling definitions supply the geometric and informational objects needed for holographic statements.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the holographic bound definitions that feed the RecognitionBandwidth unification module. That downstream module explicitly lists the holographic bound (max information ∝ boundary area / 4 Planck areas) as the first of five elements to be connected to recognition cost per bit k_R = ln(φ), ILG parameters, and the 8-tick cadence.

scope and limits

Does not derive the bound from RS forcing chain or J-function.
Does not assign numerical values outside natural units.
Does not treat time evolution or dynamical bounds.
Does not connect to phi-ladder mass formulas or alpha band.

used by (1)

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

IndisputableMonolith.Unification.RecognitionBandwidth module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (23)

def planckLength L51
def planckArea L54
def bitsPerPlanckArea L57
def maxInformation L63
theorem holographic_bound L67
def bekensteinBound L74
def sphereArea L80
def sphereVolume L83
theorem information_scales_as_area L87
def holographicRatio L95
theorem holographic_ratio_scales L98
theorem holography_from_ledger L116
theorem bulk_from_boundary L122
def blackHoleEntropy L131
theorem black_hole_maximal L136
theorem exceed_bound_makes_black_hole L142
structure DegreeOfFreedomCounting L150
theorem no_lost_dof L163
structure AdSCFT L174
theorem ryu_takayanagi L185
def holographicPredictions L197
structure HolographicFalsifier L211
def experimentalStatus L218