module module moderate

`IndisputableMonolith.Quantum.EntanglementEntropy`

The Quantum.EntanglementEntropy module supplies definitions for Planck units, Bekenstein-Hawking entropy, and entanglement entropy on bipartite systems. Researchers working on RS-native quantum gravity or holographic bounds would reference these objects. It is a pure definition module that imports Constants and Cost and contains no theorems.

claim$G_N$ (Newton's gravitational constant in SI units), $\hbar$, Planck length $\ell_P$, Planck area $A_P$, Bekenstein-Hawking entropy $S_{BH} \propto A$, entanglement entropy $S_{ent}$ on BipartiteSystem with BoundaryRegion.

background

The module sits in the quantum domain and imports IndisputableMonolith.Constants, whose doc-comment states "The fundamental RS time quantum (RS-native). $\tau_0 = 1$ tick," together with IndisputableMonolith.Cost. It introduces the listed sibling objects: $G_N$, $\hbar$, planckLength, planckArea, bekensteinHawkingEntropy, BipartiteSystem, entanglementEntropy, and BoundaryRegion. These sit inside the Recognition Science setting that already fixes $c=1$, $\hbar=\phi^{-5}$, and $G=\phi^5/\pi$.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the entropy and Planck-scale objects required by any later quantum-gravity development inside Recognition Science. It supplies the concrete constants and system types that would be used by results on the phi-ladder or the eight-tick octave once those results are written. No downstream declarations are recorded in the used_by edges.

scope and limits

Does not contain any theorems or proofs.
Does not assign numerical values to the defined constants.
Does not invoke the Recognition Composition Law or J-uniqueness.
Does not connect to the T0-T8 forcing chain steps.
Does not provide a falsifier or physical prediction.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (23)

def G_N L51
def hbar L54
def planckLength L57
def planckArea L60
def bekensteinHawkingEntropy L66
theorem bh_entropy_proportional_to_area L70
theorem bh_entropy_positive L77
structure BipartiteSystem L94
def entanglementEntropy L105
theorem entanglement_entropy_nonneg L114
theorem max_entanglement_entropy L134
structure BoundaryRegion L141
def minimalSurfaceArea L149
def ryuTakayanagi L155
theorem rt_formula_holds L161
theorem rt_from_ledger_structure L176
theorem area_not_volume L185
def bitsPerPlanckArea L195
theorem quarter_bit_per_planck_area L200
def experimentalTests L211
def implications L225
structure RTFalsifier L239
def experimentalStatus L246