module module high

`IndisputableMonolith.Quantum.BekensteinHawking`

The Quantum.BekensteinHawking module supplies Recognition Science definitions for Planck units and black hole entropy quantities. Quantum gravity researchers cite these when connecting horizon area to entropy via ledger capacity. The module consists entirely of definitions with no proofs.

claim$k_B = 1.380649 × 10^{-23} J/K$, $l_p$ Planck length, $A$ horizon area, $S_{BH} = k_B A / (4 l_p^2)$, with an alternative form $S$ derived from ledger capacity.

background

Constants module fixes the RS time quantum as τ₀ = 1 tick. Cost module supplies the J-cost and defect functions used throughout. The module then defines Planck length, area, mass and temperature, followed by BlackHole, schwarzschildRadius, horizonArea, bekensteinHawkingEntropy and entropy_from_ledger_capacity.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

Supplies the quantum black hole objects that support derivations of entropy proportional to area and entropy from ledger capacity in the Recognition framework. It aligns with the phi-ladder and cost principles for thermodynamic quantities.

scope and limits

Does not derive the area law from dynamics.
Does not include quantum corrections to entropy.
Does not address the information paradox.

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