horizonDemand_eq
plain-language theorem explainer
Horizon demand for any positive-mass Schwarzschild black hole equals exactly 1/(4 pi) in natural units. Researchers deriving universal saturation properties or holographic bounds in Recognition Science cite this result to establish mass independence. The proof is a short algebraic reduction that unfolds the definition and cancels all M-dependent factors via field simplification after confirming M is nonzero.
Claim. For every real number $M > 0$, the horizon demand of a Schwarzschild black hole of mass $M$ equals $1/(4 pi)$.
background
The Black Hole Bandwidth module treats a Schwarzschild black hole as the limiting case of full recognition saturation, where the recognition operator consumes every available bit at the horizon. Horizon demand is the normalized recognition demand extracted from Bekenstein-Hawking entropy $S_{BH} = 4 pi M^2$ divided by the eight-tick processing interval. Upstream lemmas on spatial independence and coupled-axis primitives supply the ledger structure that lets the bandwidth calculation proceed without neighbor interactions or axis coupling.
proof idea
The term-mode proof first unfolds the definition of horizonDemand. It then records that $M$ is nonzero from the positivity hypothesis and applies field simplification to cancel every mass-dependent term, leaving the constant $1/(4 pi)$.
why it matters
This equality supplies the mass-independent value used directly by horizonDemand_universal (which equates demands for any two positive masses) and saturationRatio_pos (which shows the ratio is positive for every $M > 0$). It closes the maximal-saturation step in the module, confirming that full bandwidth consumption leaves no excess for additional structure and recovers the eight-tick factor in the Hawking temperature. The result sits inside the T7 eight-tick octave and the recognition-composition law that governs ledger redistribution.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.