horizon_area_pos
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.
claimIf $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 in Recognition Science
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.
scope and limits
- Does not derive the Schwarzschild radius or metric from field equations.
- Does not extend positivity to Kerr or Reissner-Nordström horizons.
- Does not produce numerical entropy values or flux bounds.
- Does not incorporate quantum or higher-curvature corrections to area.
Lean usage
have hA : 0 < HorizonArea Rs := horizon_area_pos Rs h_Rsformal statement (Lean)
22theorem horizon_area_pos (Rs : ℝ) (h_Rs : 0 < Rs) : 0 < HorizonArea Rs := by
proof body
Tactic-mode proof.
23 unfold HorizonArea
24 have hpi : 0 < Real.pi := Real.pi_pos
25 have hsq : 0 < Rs ^ 2 := by
26 nlinarith [sq_pos_of_pos h_Rs]
27 nlinarith
28
29/-- **DEFINITION: Ledger Capacity Limit**
30 The maximum number of recognition bits that can be stored on a surface of area A.
31 $N_{bits} = A / \ell_0^2$ in RS natural units. -/