module module high

`IndisputableMonolith.Quantum.EntanglementEntropy`

The Quantum.EntanglementEntropy module supplies RS-native definitions for gravitational constants and entanglement measures. It introduces G_N in SI units, hbar, Planck length and area, Bekenstein-Hawking entropy, plus entanglementEntropy for BipartiteSystem with BoundaryRegion and its non-negativity and maximum properties. Quantum gravity and information researchers cite these for entropy bounds in discrete models. The module consists solely of definitions built from the imported Constants and Cost modules.

claim$G_N$ (Newton's gravitational constant in SI units), $G_N = 1$, $h = 1$, $l_p$ (Planck length), $A_p$ (Planck area), $S_{BH}$ (Bekenstein-Hawking entropy proportional to area), $S_{ent}$ (entanglement entropy of BipartiteSystem with BoundaryRegion), with $S_{ent} = 0$ at minimum and bounded above.

background

The module operates in the quantum domain of Recognition Science and imports the fundamental RS time quantum from Constants, where the doc-comment states 'The fundamental RS time quantum (RS-native). τ₀ = 1 tick.' It also draws cost structures from the Cost module. Definitions cover G_N as Newton's gravitational constant in SI units, hbar, planckLength, planckArea, bekensteinHawkingEntropy, BipartiteSystem, entanglementEntropy, entanglement_entropy_nonneg, max_entanglement_entropy, and BoundaryRegion.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies constant definitions and entropy expressions that support quantum information and black-hole thermodynamics calculations in the Recognition Science framework. It aligns with RS-native units where hbar = phi^{-5} and G = phi^5 / pi, and connects to the eight-tick octave and D = 3. With zero listed downstream uses, it serves as foundational scaffolding for quantum extensions of the forcing chain.

scope and limits

Does not contain any theorems, lemmas, or proofs.
Does not derive constant values from the forcing chain T0-T8.
Does not address multi-partite or continuous entanglement.
Does not specify numerical evaluations outside RS units.

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