module module moderate

`IndisputableMonolith.Quantum.BlackHoleInformation`

This module defines black hole objects in Recognition Science by mass and derives associated geometric and thermodynamic quantities in RS-native units. Quantum gravity researchers modeling discrete-time black hole thermodynamics would reference these constructions. The module is a collection of type and function definitions with no embedded proofs.

claimA black hole is an object $BH(M)$ characterized by mass $M$, equipped with maps $r_s(M)$ (Schwarzschild radius), $A(M)$ (horizon area), $S_{BH}(M)$ (Bekenstein-Hawking entropy), $T_H(M)$ (Hawking temperature), information capacity, and holographic bound saturation checks.

background

The module imports the RS time quantum $\tau_0 = 1$ tick from Constants and works in the quantum domain. It introduces BlackHole as a structure determined solely by mass, then defines derived quantities such as horizon area and entropy using the phi-ladder and constants from the forcing chain (T5 J-uniqueness through T8, $D=3$).

All quantities are expressed in RS units where $c=1$, $\hbar=\phi^{-5}$, and $G=\phi^5/\pi$. The module supplies the base objects for black hole information capacity and holographic bounds.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the black hole primitives required for any treatment of the information paradox or holographic bounds inside Recognition Science. It directly supports the quantum domain constructions that connect to the eight-tick octave and the alpha band constants.

scope and limits

Does not derive entropy or temperature from the Recognition Composition Law.
Does not model Hawking radiation or evaporation dynamics.
Does not place mass on the phi-ladder rungs.
Does not resolve the black hole information paradox.

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