horizonDemand
plain-language theorem explainer
Horizon demand defines the recognition rate consumed at a Schwarzschild horizon as mass M divided by the light-crossing dynamical time 4πM. Researchers deriving holographic saturation or no-hair results cite this when establishing that every bit at the horizon is occupied by gravitational dynamics. The definition cancels algebraically to the universal constant 1/(4π) with no residual mass dependence.
Claim. The gravitational recognition demand at the horizon for Schwarzschild mass $M$ equals $M/(4πM)$, which simplifies to the constant $1/(4π)$.
background
BlackHoleBandwidth treats a black hole as the case of full recognition saturation where the operator is maximally busy at every scale. The module sets horizon area to $16πM^2$ and Bekenstein-Hawking entropy to $4πM^2$ in natural units, with dynamical time $T_{dyn}=4πM$ as the light-crossing interval. Each Planck-mass unit then requires one update per cycle, so demand is total mass divided by that interval. Upstream RecognitionStructure M supplies the base universe and recognition function that the bandwidth calculations rest on.
proof idea
The definition is a direct one-line expression that divides M by the product of 4, π, and M. It is invoked verbatim by the downstream equality theorem that cancels the mass terms under the assumption M>0.
why it matters
This definition supplies the demand term for excessBandwidth, which formalizes the no-hair theorem by showing zero remaining capacity for additional structure. It also feeds horizonDemand_eq and saturationRatio, confirming mass-independent saturation at the horizon. The 4π factor aligns with the eight-tick cadence in the Recognition framework and supports the identification of area with entropy with bandwidth. The result closes one step in the maximal-saturation argument without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.