IndisputableMonolith.Gravity.BlackHoleInformationPreservation

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