HorizonArea
plain-language theorem explainer
HorizonArea supplies the event horizon area of a Schwarzschild black hole as four pi times the square of the Schwarzschild radius. Researchers deriving Bekenstein-Hawking entropy from ledger capacity limits cite this when converting radius to area in recognition-based calculations. The definition is introduced as a direct algebraic expression matching the standard spherical surface area formula.
Claim. The horizon area $A$ for a Schwarzschild black hole of radius $R_s$ is given by $A = 4 pi R_s^2$.
background
This definition sits in the module that derives Bekenstein-Hawking entropy from the ledger capacity limit, with the stated objective to prove that $S_{BH} = A / 4 ell_p^2$ arises from maximum recognition flux. The upstream radius definition from CellularAutomata supplies the discrete neighborhood size used in the broader recognition model, though HorizonArea itself employs the continuous Euclidean surface formula. In the local setting, black hole horizons function as saturation points for information recognition under the Recognition Composition Law.
proof idea
The definition is a one-line algebraic expression that directly implements the standard formula for the surface area of a sphere.
why it matters
HorizonArea is invoked by bh_entropy_from_ledger to equate Bekenstein-Hawking entropy with the ledger capacity limit and by the positivity and uniqueness results horizon_area_pos, sbh_saturation_positive, sbh_saturation_nonzero, and sbh_saturation_uniqueness. It supplies the geometric input required to close the chain from recognition flux to black hole thermodynamics, consistent with the framework's forcing chain that fixes D=3 and the phi-ladder constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.