module module high

`IndisputableMonolith.Unification.BlackHoleBandwidth`

The BlackHoleBandwidth module defines Schwarzschild radius, horizon area, entropy, bandwidth, demand, and saturation ratio for black holes in Recognition Science native units. It extends the RecognitionBandwidth framework to gravitational horizons by applying the recognition cost per bit. The module consists of direct definitions that import constants and the holographic setup without internal proofs.

claim$r_s = 2M$, $A_h = 4π r_s^2$, $S_{BH} = A_h k_R/4$, $B_h = A_h ln(φ)/(4 τ_0)$, with horizonDemand and saturationRatio following from the same ledger cost.

background

Recognition Science sets the fundamental time quantum τ₀ = 1 tick and derives the Boltzmann analog k_R from the ledger bit cost. The upstream RecognitionBandwidth module states the holographic bound (maximum information proportional to boundary area over four Planck areas), sets k_R = ln(φ), introduces the ILG parameters C_lag = φ^{-5} and α = (1-1/φ)/2, and fixes the eight-tick cadence. This module applies those elements to black hole horizons.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the black hole horizon quantities that complete the holographic connection inside the RecognitionBandwidth unification. It places black hole entropy and bandwidth on the same recognition cost ledger used for the eight-tick octave and the α band.

scope and limits

Does not derive the Schwarzschild radius from field equations.
Does not prove the area law for entropy.
Does not compute numerical values for specific masses.
Does not include quantum corrections to the horizon.

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Constants.BoltzmannConstant module_import
IndisputableMonolith.Cost module_import
IndisputableMonolith.Unification.RecognitionBandwidth module_import

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