saturationRatio
plain-language theorem explainer
The saturation ratio for a black hole of mass M is defined as the quotient of its horizon demand and horizon bandwidth. Researchers modeling holographic bounds or recognition saturation in gravity cite this when quantifying uniform maximal occupancy at the horizon across all masses. The definition is a direct division of the two quantities established earlier in the module.
Claim. For a Schwarzschild black hole of mass $M$, the saturation ratio is defined by $D(M)/B(M)$, where $D(M)$ is the horizon demand and $B(M)$ is the horizon bandwidth.
background
The module treats black holes as the limiting case of full recognition bandwidth consumption at every scale, with the recognition operator maximally occupied. Horizon area is $16πM²$, Bekenstein-Hawking entropy is $4πM²$, and recognition bandwidth equals entropy divided by $(k_R · 8τ_0)$. This rests on the Recognition structure $M$ supplying the core operator and on upstream identifications of simplicial ledgers with continuum geometry via Laplacian actions on edge lengths.
proof idea
One-line wrapper that divides horizonDemand M by horizonBandwidth M.
why it matters
The definition is invoked directly by saturationRatio_pos, which proves positivity for $M>0$ and the $1/M²$ scaling that places larger black holes deeper in saturation. It completes the module's central claim that black holes saturate the holographic bound uniformly, tying to the eight-tick cadence in Hawking temperature and the absence of excess bandwidth for hair. In the framework it reinforces T7 and the entropy-as-bandwidth identification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.