sbh_saturation_positive
plain-language theorem explainer
Positive Schwarzschild radius yields strictly positive Bekenstein-Hawking entropy saturation in Recognition Science units. Derivations of black hole thermodynamics from recognition ledger capacity cite this positivity result. The proof applies horizon_area_pos and ell0_pos via div_pos after a nlinarith step on the denominator.
Claim. For any real number $R_s > 0$, $0 < 4 pi R_s^2 / (4 ell_0^2)$, where the numerator is the event horizon area and $ell_0$ is the fundamental length unit.
background
This module derives the Bekenstein-Hawking entropy from the ledger capacity limit. The objective is to prove that $S_{BH} = A / 4 ell_p^2$ arises from maximum recognition flux. HorizonArea(Rs) is defined as 4 pi Rs^2, the area of the event horizon for a Schwarzschild black hole. ell0 is the fundamental length unit in RS-native units, set to 1 with ell0_pos proving 0 < ell0 from the constants derivation tau0^2 = hbar G / (pi c^5). Upstream, entropy is defined as total_defect of a configuration, with the initial state having minimum entropy.
proof idea
The tactic proof first obtains 0 < HorizonArea Rs from horizon_area_pos Rs h_Rs. It then establishes 0 < 4 * ell0^2 by nlinarith on ell0_pos. The final step applies div_pos to these two facts.
why it matters
This result feeds directly into sbh_saturation_nonzero, which establishes that the saturation value is nonzero. It fills the positivity step in the module's derivation of black hole entropy from maximum recognition flux. In the framework it connects to the entropy definition as proportional to total defect, supporting the information-theoretic origin of thermodynamic quantities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.