IndisputableMonolith.Unification.BlackHoleBandwidth

declarations in this module (19)

• def schwarzschildRadius L48
• def horizonArea L51
• theorem horizonArea_pos L53
• def bhEntropy L58
• theorem bhEntropy_eq L60
• theorem bhEntropy_pos L64
• def horizonBandwidth L71
• theorem horizonBandwidth_pos L74
• def horizonDemand L85
• theorem horizonDemand_eq L88
• theorem horizonDemand_universal L95
• def saturationRatio L112
• theorem saturationRatio_pos L117
• def hawkingTemp L133
• theorem hawkingTemp_pos L135
• theorem hawkingTemp_inv_mass L140
• theorem hawking_contains_eight_tick L154
• def excessBandwidth L170
• theorem entropy_is_bandwidth_capacity L175