module module moderate

`IndisputableMonolith.Quantum.BlackHoleInformation`

This module defines black hole objects and their geometric, thermodynamic, and information properties inside the Recognition Science framework. It introduces BlackHole parameterized by mass together with derived quantities such as Schwarzschild radius, horizon area, Bekenstein-Hawking entropy, Hawking temperature, information capacity, and the holographic bound. Researchers working on quantum gravity and the black-hole information paradox would cite these definitions to place classical solutions inside RS-native units. The module consists of a

claimLet $M$ be the mass of a black hole. Define the Schwarzschild radius $r_s = 2GM$, horizon area $A = 4π r_s^2$, Bekenstein-Hawking entropy $S_{BH} = A/4$, Hawking temperature $T_H$, information capacity, and the statement that black holes saturate the holographic bound.

background

The module sits in the quantum domain of Recognition Science and imports the fundamental RS time quantum τ₀ = 1 tick from Constants. It introduces BlackHole as the central structure characterized by its mass. Key definitions include schwarzschildRadius, horizonArea, bekensteinHawkingEntropy, entropy_proportional_to_mass_squared, hawkingTemperature, informationCapacity, holographicBound, bh_saturates_holographic, FallingEntry, and BlackHoleLedger. These objects supply the geometric and ledger structures needed to discuss information flow at horizons.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

This module supplies the core objects for black-hole information accounting in Recognition Science. It provides the base layer that later theorems on quantum information preservation and holographic principles will reference, connecting mass scaling on the phi-ladder to entropy and capacity bounds.

scope and limits

Does not derive the Hawking radiation spectrum.
Does not address the information paradox resolution.
Does not compute explicit numerical entropy values in RS units.
Does not prove unitarity of evaporation.

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (25)

structure BlackHole L51
def schwarzschildRadius L58
def horizonArea L61
def bekensteinHawkingEntropy L65
theorem entropy_proportional_to_mass_squared L69
def hawkingTemperature L75
theorem hawking_temperature_pos L79
def informationCapacity L91
def holographicBound L95
theorem bh_saturates_holographic L98
structure FallingEntry L106
structure BlackHoleLedger L115
def addEntry L124
theorem information_preserved_on_infall L130
structure HawkingQuantum L136
structure EvaporationProcess L145
theorem information_conservation L156
theorem page_curve L163
theorem no_information_paradox L189
theorem no_firewall L205
theorem er_equals_epr L214
structure BlackHolePredictions L227
def rsPredictions L236
structure BlackHoleFalsifier L249
theorem current_understanding_consistent L258