excessBandwidth
plain-language theorem explainer
Excess bandwidth for a Schwarzschild black hole of mass M is the difference between horizon recognition bandwidth and gravitational demand on that bandwidth. Researchers studying black hole information or no-hair theorems in Recognition Science cite this quantity to bound the maximum distinguishable features a horizon can support. The definition is a direct subtraction of the two horizon quantities already established via area and entropy relations in the module.
Claim. For a black hole of mass $M$, the excess bandwidth is $R(M) - D(M)$, where $R(M)$ is the maximum recognition bandwidth supported by the horizon area $A = 16πM^2$ and $D(M)$ is the bandwidth consumed by the gravitational dynamics of the horizon.
background
In the Recognition Science treatment of black holes the horizon is a maximally saturated recognition surface. Bekenstein-Hawking entropy $S_{BH} = 4πM^2$ (natural units) fixes the total holographic bits; recognition bandwidth is then $R_{max} = S_{BH}/(k_R · 8τ_0)$, incorporating the eight-tick cadence. The module shows that gravitational demand exactly equals this bandwidth for any $M$, leaving zero excess capacity for additional structure. Upstream, entropy is defined as total defect (InitialCondition.entropy) and constants are calibrated through phi-forcing structures (PhiForcingDerived.of).
proof idea
One-line definition that subtracts horizonDemand M from horizonBandwidth M; both quantities are already constructed from the area-entropy relations and the eight-tick factor appearing in the module.
why it matters
The definition supplies the excess term that must vanish for maximal saturation, thereby furnishing the bandwidth account of the no-hair theorem stated in the module documentation. It supports downstream claims such as no_hair_from_saturation and entropy_is_bandwidth by quantifying remaining recognition capacity. In the framework it links directly to the eight-tick octave (T7) via the factor of 8 and to the identification of area with information with bandwidth.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.