sbh_saturation_positive
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not compute the explicit numerical value of the entropy saturation.
- Does not extend to Kerr or charged black hole metrics.
- Does not derive the horizon area formula from ledger axioms.
- Does not address quantum or higher-order corrections.
Lean usage
theorem sbh_example (Rs : ℝ) (h : Rs > 0) : 0 < HorizonArea Rs / (4 * ell0^2) := sbh_saturation_positive Rs hformal statement (Lean)
68theorem sbh_saturation_positive (Rs : ℝ) (h_Rs : Rs > 0) :
69 0 < HorizonArea Rs / (4 * ell0^2) := by
proof body
Tactic-mode proof.
70 have hA : 0 < HorizonArea Rs := horizon_area_pos Rs h_Rs
71 have hden : 0 < 4 * ell0 ^ 2 := by
72 nlinarith [sq_pos_of_pos ell0_pos]
73 exact div_pos hA hden
74
75/-- The BH entropy saturation value is nonzero for `Rs > 0`. -/