saturationRatio_pos
plain-language theorem explainer
For any positive real mass M the saturation ratio at a Schwarzschild horizon is strictly positive. Researchers modeling holographic saturation or information bounds in gravity cite the result to confirm that every black hole with M > 0 operates at full recognition capacity. The proof is a one-line term wrapper that unfolds the ratio definition and invokes positivity of division after rewriting the demand term and quoting the known positivity of bandwidth.
Claim. For every real number $M > 0$, the saturation ratio $D(M)/B(M) > 0$, where $D(M)$ denotes horizon demand and $B(M)$ denotes horizon bandwidth.
background
In the Black Hole Bandwidth module a Schwarzschild horizon is treated as the limiting case of maximal recognition saturation. Horizon area is $16πM²$, Bekenstein-Hawking entropy is $4πM²$, and recognition bandwidth is entropy divided by the product of the recognition constant and the eight-tick period. The saturation ratio is the quotient of horizon demand and this bandwidth; the module states that the ratio scales as $1/M²$ and that any $M > 0$ places the horizon in saturation. Upstream constants supply the fundamental tick $τ₀ = 1$ and the eight-tick octave that appears in the temperature formula.
proof idea
The term proof unfolds the saturation-ratio definition, then applies the lemma that the quotient of two positive reals is positive. The numerator is rewritten via the horizon-demand equality lemma and shown positive by multiplying the unit by a positive real and $π$; the denominator is supplied directly by the horizon-bandwidth positivity lemma.
why it matters
The result anchors the claim that every positive-mass black hole is maximally saturated, which the module uses to derive the absence of hair, the Hawking temperature $T_H = 1/(8πM)$, and the identification of entropy with bandwidth. It sits inside the eight-tick cadence (T7) and the D = 3 spatial setting of the forcing chain, and directly precedes the Hawking-temperature section. No open scaffolding remains for this specific positivity statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.