bhEntropy_pos
plain-language theorem explainer
Black hole entropy in the Recognition Science model is strictly positive for any positive real mass M. Researchers deriving holographic bounds or information saturation at horizons cite this to confirm the entropy expression never vanishes. The proof is a one-line term reduction that rewrites via the defining equality and applies repeated multiplication-positivity lemmas together with the positivity of π and of M squared.
Claim. For every real number $M > 0$, the black-hole entropy $4πM^2$ (in natural units) satisfies $0 < 4πM^2$.
background
The module treats a Schwarzschild black hole as the limiting case of maximal recognition-bandwidth saturation: every holographic bit on the horizon is consumed by gravitational dynamics, leaving no excess capacity. In this setting the Bekenstein-Hawking entropy reduces to $S_{BH} = 4πM^2$ (area $A = 16πM^2$ divided by $4ℓ_P^2$). The auxiliary constant $k_R = ln φ$ (from Constants.BoltzmannConstant) supplies the information cost per recognition bit and appears in the bandwidth formula that follows from this entropy.
proof idea
The term proof first rewrites the target via bhEntropy_eq to obtain an explicit product containing a positive numerical factor, π, and $M^2$. It then applies mul_pos twice, using the known positivity of π together with sq_pos_of_pos on the hypothesis $0 < M$.
why it matters
The result feeds directly into horizonBandwidth_pos, which establishes that horizon bandwidth itself is positive. It thereby supports the module claim that entropy equals bandwidth under maximal saturation and is consistent with the eight-tick cadence appearing in the Hawking-temperature derivation. The positivity closes a basic non-negativity requirement before any further saturation or no-hair arguments are built.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.