module module moderate

`IndisputableMonolith.Quantum.BekensteinHawking`

The module Quantum.BekensteinHawking supplies definitions for the Boltzmann constant, Planck units, BlackHole structures, horizon area, and Bekenstein-Hawking entropy expressed via ledger capacity in Recognition Science units. Quantum gravity researchers would cite these to link RS cost functions to thermodynamic area laws. The module consists entirely of definitions with no theorems or proofs.

claim$k_B = 1.380649 \times 10^{-23} \, \mathrm{J/K}$, $\ell_p$ the Planck length, $A$ the horizon area, and $S_{BH} = k_B A / (4 \ell_p^2)$ together with its bit-count form from ledger capacity.

background

The module sits in the quantum domain and imports the RS time quantum $\tau_0 = 1$ tick from Constants plus cost primitives from Cost. It defines Planck length, area, mass, and temperature from RS-native units ($c=1$, $\hbar = \phi^{-5}$), then introduces the BlackHole type with schwarzschildRadius and horizonArea. Entropy definitions follow, including proportionality to area and conversion to bits via ledger capacity.

The setting uses the Recognition Composition Law to express information capacity at the horizon. No upstream theorems beyond the imported modules are invoked.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the entropy and area primitives that support later Recognition Science results on quantum information bounds and black hole thermodynamics. It fills the interface between Cost ledger accounting and horizon geometry, consistent with the eight-tick octave and $D=3$ spatial dimensions. No downstream theorems are recorded in the current graph.

scope and limits

Does not derive the area law from the Recognition Composition Law.
Does not compute numerical entropy for concrete black hole masses.
Does not include quantum corrections or higher-order terms.
Does not reference the J-uniqueness or T5-T8 forcing chain.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (28)

def k_B L42
def planckLength L47
def planckArea L50
def planckMass L53
def planckTemperature L56
structure BlackHole L61
def schwarzschildRadius L66
def horizonArea L70
def bekensteinHawkingEntropy L79
theorem entropy_proportional_to_area L83
def entropyInBits L87
theorem entropy_from_ledger_capacity L99
def informationContent L106
def hawkingTemperature L115
theorem temperature_inverse_mass L119
def solarMassTemperature L127
theorem planck_mass_temperature L131
theorem temperature_from_tau0 L144
def surfaceGravity L150
theorem temperature_from_surface_gravity L153
theorem first_law L179
theorem second_law_classical L190
def hawkingPower L203
def evaporationTime L208
theorem solar_mass_lives_forever L212
theorem information_preserved L228
def predictions L242
structure BHThermodynamicsFalsifier L256