entropy_nonneg
plain-language theorem explainer
The declaration establishes that Bekenstein-Hawking entropy, given by horizon area divided by four in Planck units, is non-negative for any non-negative area. Physicists deriving black-hole thermodynamics from J-cost minimization in the Recognition Science framework cite it to confirm consistency with the second law. The proof is a direct term application of division non-negativity to the area hypothesis and the positive constant four.
Claim. For any real number $A$ with $A ≥ 0$, the Bekenstein-Hawking entropy $S_{BH}(A) = A/4$ satisfies $S_{BH}(A) ≥ 0$.
background
The No-Hair Theorem module treats stationary black-hole states as unique J-cost minimizers under the three conserved charges (M, Q, J) forced by the RS voxel lattice. Bekenstein-Hawking entropy is defined as area divided by four, counting ledger J-bits crossing the horizon per unit area. This non-negativity imports the general result that Shannon entropy is non-negative for any probability distribution, as stated in the InformationIsLedger and ShannonEntropy modules.
proof idea
The proof is a one-line term wrapper that applies div_nonneg to the hypothesis 0 ≤ area together with the normalization that the denominator four is positive.
why it matters
This result supplies the non-negativity leg required by the Bekenstein-Hawking formula inside the no-hair theorem, feeding the IC-001 certificate that information equals the ledger. It aligns with the holographic principle in the BrainHolography volume definition, where information content scales with surface area rather than volume. The parent no-hair results rely on it to maintain thermodynamic consistency with J-cost minimization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.