module module high

`IndisputableMonolith.Quantum.HolographicBound`

Quantum.HolographicBound supplies the core definitions for the holographic principle inside Recognition Science, fixing the Planck length to unity in natural units and deriving Planck area, bits per Planck area, maximum information, and the Bekenstein bound. Researchers linking quantum information bounds to the RS forcing chain and RecognitionBandwidth unification cite these objects. The module is a pure collection of definitions with no theorems or proofs.

claim$l_P = 1$ (Planck length), $A_P = 4 l_P^2$ (Planck area), bits per Planck area, max information $\propto$ boundary area / (4 Planck areas), holographic bound, and Bekenstein bound.

background

The module sits in the Quantum domain and imports only Mathlib and IndisputableMonolith.Constants, where the fundamental RS time quantum is defined as $\tau_0 = 1$ tick. It introduces the holographic bound as max information proportional to boundary area divided by four Planck areas, together with the listed sibling definitions (planckLength, planckArea, bitsPerPlanckArea, maxInformation, holographic_bound, bekensteinBound, sphereArea, information_scales_as_area, etc.). The setting is the natural-unit framework in which $c=1$ and lengths are expressed relative to the RS time quantum.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The definitions feed directly into IndisputableMonolith.Unification.RecognitionBandwidth, which lists the holographic bound as the first of five elements of Recognition Science that have never been formally connected and links it to recognition cost per bit $k_R = \ln(\phi)$, ILG parameters $C_{\rm lag} = \phi^{-5}$, and the 8-tick cadence. The module therefore supplies the concrete objects required for that unification step.

scope and limits

Does not derive the holographic bound from the J-function or Recognition Composition Law.
Does not assign numerical values to constants beyond the choice of natural units.
Does not reference the phi-ladder, mass formula, or T0-T8 forcing chain.
Does not contain any theorems or proofs.

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