module module moderate

`IndisputableMonolith.Quantum.BekensteinHawking`

Module Quantum.BekensteinHawking supplies definitions for the Boltzmann constant, Planck scales, black-hole geometry, and Bekenstein-Hawking entropy expressed via RS constants and cost. Quantum-gravity and holographic-information researchers cite these objects when working in discrete or ledger-based frameworks. The module is a pure definition collection that imports Constants and Cost and builds the listed sibling declarations without theorems.

claim$k_B = 1.380649 imes 10^{-23} \, \mathrm{J/K}$, $\ell_p$ Planck length, $A$ horizon area, $S_{BH} = k_B A / (4 \ell_p^2)$, with entropy also expressed in bits and from ledger capacity.

background

The module lives in the quantum domain and imports Constants (whose doc states "The fundamental RS time quantum (RS-native). $\tau_0 = 1$ tick.") together with Cost. It introduces $k_B$, the Planck quantities, the BlackHole structure, schwarzschildRadius, horizonArea, bekensteinHawkingEntropy, entropy_proportional_to_area, entropyInBits, and entropy_from_ledger_capacity. These rest on the J-cost and defectDist machinery supplied by the Cost import.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the entropy objects that feed any later quantum or holographic results in the Recognition Science derivation of physics from the single functional equation. It supplies the concrete link between area and information count that appears in the T5–T8 forcing chain and the Recognition Composition Law.

scope and limits

Does not derive the area law from the J-cost equation.
Does not include quantum corrections or higher-curvature terms.
Does not connect explicitly to the phi-ladder mass formula.
Does not prove numerical agreement with observed black-hole entropies.

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