module module moderate

`IndisputableMonolith.Gravity.BlackHoleInformationPreservation`

This module defines the black-hole mass at time t under linear evaporation in RS-native units, together with evaporation time, entropy sums, and radiation entropy. Researchers working on the black-hole information paradox within Recognition Science would cite these quantities. The module is a collection of definitions and short lemmas with no complex proofs.

claimThe black-hole mass at time $t$ under linear evaporation is $M(t) = M_0 (1 - t/t_{ m evap})$ for $0 \le t \le t_{ m evap}$, with $t_{ m evap}$ the evaporation timescale, $S_{ m BH}(t)$ the horizon entropy from the ledger, and $S_{ m rad}(t)$ the radiated entropy.

background

The module imports the RS time quantum $ au_0 = 1$ tick from Constants. It relies on the ledger-derived Bekenstein-Hawking entropy $S_{ m BH} = A/(4 au_0^2)$ with $\phi$-rational log corrections from BlackHoleEntropyFromLedger, the Hawking temperature expressed via rung spacing from HawkingTemperatureFromRung, and the bounce-echo identity from BlackHoleEchoesFromBounce. The local setting is the discrete RS ledger applied to Schwarzschild horizons under the linear-evaporation ansatz.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The definitions supply the mass evolution and entropy accounting required for the black-hole information-preservation argument in the Recognition Science framework. They connect the entropy-from-ledger result and the temperature-from-rung result to the overall information accounting that closes the paradox via the bounce-echo mechanism.

scope and limits

Does not derive the linear evaporation law from the RS forcing chain.
Does not compute explicit numerical values in SI units.
Does not address the detailed quantum-state mapping beyond entropy counts.
Does not prove unitarity of the evaporation process.

depends on (5)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import
IndisputableMonolith.Gravity.BlackHoleEchoesFromBounce module_import
IndisputableMonolith.Gravity.BlackHoleEntropyFromLedger module_import
IndisputableMonolith.Gravity.HawkingTemperatureFromRung module_import

declarations in this module (31)

def bhMass L96
theorem bhMass_at_zero L98
def t_evap L102
theorem t_evap_pos L104
theorem bhMass_at_evap L109
theorem bhMass_nonneg_in_window L116
def S_BH_at L137
theorem S_BH_at_def L139
def S_thermal_at L145
theorem S_thermal_at_def L147
theorem naive_entropy_sum L151
def S_radiation_at L168
theorem S_radiation_le_S_thermal L172
theorem S_radiation_le_S_BH L177
def pageTime L188
theorem pageTime_pos L190
theorem pageTime_eq_half_t_evap L196
theorem page_time_at_half_evap L202
theorem S_R_at_page_eq_S_BH L210
def pageEntropy L219
theorem S_R_at_page_eq_page_entropy L222
theorem S_thermal_at_page L230
theorem S_thermal_mono L237
theorem S_BH_anti L247
theorem entropy_bound_by_initial_BH_half L259
def joint_VN_entropy L289
theorem joint_VN_entropy_zero L293
theorem joint_VN_entropy_conserved L299
structure BlackHoleInformationCert L321
def blackHoleInformationCert L339
theorem black_hole_information_one_statement L361