module module high

`IndisputableMonolith.Gravity.BlackHoleInformationPreservation`

The module defines the black-hole mass m(t) under linear evaporation in RS-native units, together with the evaporation timescale t_evap and time-dependent entropy trackers S_BH(t) and S_thermal(t). Researchers working on black-hole thermodynamics and information flow in discrete spacetime models would cite these objects. The module consists of direct definitions plus elementary lemmas establishing positivity and non-negativity by algebraic inspection.

claimLet $m(t)$ be the black-hole mass at time $t$ under linear evaporation. Then $m(0)=m_0$, $m(t_ {evap})=0$, and $m(t)=m_0(1-t/t_{evap})$ for $0<t<t_{evap}$, with $t_{evap}>0$. The horizon entropy $S_{BH}(t)$ and radiation entropy $S_{thermal}(t)$ are defined at each instant from the ledger count and temperature formulas.

background

The module sits inside the Recognition Science treatment of gravity. It imports the fundamental RS time quantum τ₀ from Constants, the J-cost function, the recovery of Bekenstein-Hawking entropy S_BH = A/(4ℓ_P²) plus φ-rational log corrections from the discrete ledger, the Hawking temperature expressed via rung spacing, and the structural echo delay identity from bounce dynamics. These supply the dimensional bridge and the entropy ledger that the evaporation model then uses to track information.

proof idea

This is a definition module. bhMass is introduced as the linear function of time, t_evap is fixed by the initial mass and the imported temperature formula, and S_BH_at, S_thermal_at are defined by direct substitution into the ledger and rung expressions. The lemmas t_evap_pos and bhMass_nonneg_in_window follow by elementary arithmetic from these definitions; no external lemmas beyond the imported constants are required.

why it matters in Recognition Science

The module supplies the mass-loss and entropy-evolution functions required to formulate the information-preservation claim for evaporating black holes. It feeds the entropy ledger recovery and the Hawking-temperature rung identity into a concrete time-dependent setting, preparing the accounting that would close the information paradox inside the RS framework. The sibling definitions bhMass, S_BH_at and S_radiation_at are the direct inputs to any subsequent conservation statement.

scope and limits

Does not derive the linear evaporation law from the RS forcing chain.
Does not encode or track specific quantum information states.
Does not convert results to SI units or produce LIGO predictions.
Does not prove global information preservation; only prepares the mass and entropy functions.

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