module module moderate

`IndisputableMonolith.Quantum.BlackHoleInformation`

This module supplies the core definitions for black-hole mass, radius, area, entropy, temperature and information capacity inside the Recognition Science framework. A physicist working on holographic bounds or black-hole thermodynamics in RS-native units would cite these objects. The module is a pure definition block that imports only the RS time quantum and assembles the listed sibling declarations without proofs.

claimA black hole is characterized by its mass $M$. The Schwarzschild radius, horizon area, Bekenstein-Hawking entropy, Hawking temperature and information capacity are then defined from $M$ together with the RS constants $ au_0$, $ au_0 = 1$ tick.

background

The module sits inside the Quantum domain and imports only IndisputableMonolith.Constants, whose sole documented object is the fundamental RS time quantum $ au_0 = 1$ tick. All subsequent definitions (BlackHole, schwarzschildRadius, horizonArea, bekensteinHawkingEntropy, hawkingTemperature, informationCapacity, holographicBound) are therefore expressed in RS-native units where $c=1$, $ar h = au_0^{-5}$ and $G = au_0^5/ au_0$. The single sentence supplied for the module states that a black hole is characterized by its mass, which fixes the entire ladder of derived quantities.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The declarations supply the concrete objects required by any later treatment of black-hole information or the holographic principle inside Recognition Science. They sit downstream of the Constants module and upstream of any quantum-information or entropy-balance arguments that would close the information paradox in the RS setting.

scope and limits

Does not resolve the black-hole information paradox.
Does not derive the listed quantities from the J-functional equation.
Does not import or use the phi-ladder or eight-tick octave.
Does not contain any theorem or sorry.
Does not address quantum fields or Hawking radiation spectra.

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