horizon_area_pos
plain-language theorem explainer
Positive Schwarzschild radius Rs implies strictly positive horizon area 4π Rs². Derivations of Bekenstein-Hawking entropy from recognition ledger capacity invoke this fact to ensure saturation bounds remain positive. The tactic proof unfolds the area definition then applies Real.pi_pos together with sq_pos_of_pos and nlinarith to obtain the product inequality.
Claim. If $Rs > 0$ then $4π Rs^2 > 0$.
background
The Black Hole Entropy module derives Bekenstein-Hawking entropy from the ledger capacity limit, where maximum recognition bits on a surface equal A / ℓ₀² in RS units. HorizonArea is the sibling definition 4 * Real.pi * Rs² that supplies the geometric input A. The module objective is to recover S_BH = A / 4 ℓ_p² from maximum recognition flux.
proof idea
The proof unfolds HorizonArea to expose 4 * Real.pi * Rs^2. It obtains 0 < Real.pi from Real.pi_pos and 0 < Rs^2 from sq_pos_of_pos applied to the hypothesis 0 < Rs. nlinarith then combines the three strict inequalities to conclude the product is positive.
why it matters
This lemma is invoked directly by sbh_saturation_positive, which asserts that HorizonArea Rs / (4 * ell0^2) > 0 for Rs > 0 and thereby confirms positive entropy saturation. It supplies the elementary positivity step required by the module's derivation of S_BH from ledger capacity. The result sits inside the Recognition Science treatment of compact objects, where the eight-tick octave and D = 3 underlie the discrete ledger structure that bounds information on the horizon.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.