sbh_saturation_nonzero
plain-language theorem explainer
The theorem shows that the Bekenstein-Hawking saturation value for a Schwarzschild black hole stays nonzero when the Schwarzschild radius is positive. Researchers deriving black hole thermodynamics from ledger capacity and maximum recognition flux would cite this step. The proof is a one-line term application of ne_of_gt to the already-proved positivity of the identical ratio.
Claim. For every real number $R_s > 0$, the ratio of the Schwarzschild event horizon area $4π R_s^2$ to four times the square of the fundamental length $ℓ_0$ is nonzero.
background
The module derives the Bekenstein-Hawking entropy $S_{BH} = A / 4ℓ_p^2$ from the ledger capacity limit and maximum recognition flux. HorizonArea is defined as $4π R_s^2$. The constant $ℓ_0$ is the fundamental length unit (voxel) in RS-native units, obtained from $τ_0^2 = ℏG/(π c^5)$ with $c=1$ and $ℏ=φ^{-5}$. The upstream theorem sbh_saturation_positive already establishes that the same ratio is strictly positive for $R_s > 0$.
proof idea
The proof is a one-line wrapper that applies ne_of_gt directly to sbh_saturation_positive Rs h_Rs.
why it matters
This declaration completes the nonzero claim for the entropy saturation value inside the black-hole entropy derivation from maximum recognition flux. It supports the module objective of obtaining $S_{BH} = A / 4ℓ_p^2$ from the ledger capacity limit. The result sits downstream of the positivity theorem and upstream of any further use of the saturation expression in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.