horizonArea
plain-language theorem explainer
The horizon area of a Schwarzschild black hole equals four pi times the square of its Schwarzschild radius. Workers deriving black hole thermodynamics from the Recognition Science ledger cite this when establishing the area law for entropy. The declaration is a one-line algebraic definition in terms of the Schwarzschild radius.
Claim. For a Schwarzschild black hole with positive mass, the horizon area $A$ satisfies $A = 4 pi r_s^2$, where $r_s$ is the Schwarzschild radius.
background
The module derives black hole thermodynamics from Recognition Science, with the horizon area measuring the ledger's information capacity and supporting the holographic bound. A black hole is a structure consisting of a positive real mass. This definition builds directly on the Schwarzschild radius and supplies the area input to the entropy formula. Upstream, the entropy definition from InitialCondition states that entropy of a configuration is proportional to its total defect, with zero defect yielding minimum entropy.
proof idea
The declaration is a one-line definition that computes the horizon area by multiplying four pi by the square of the Schwarzschild radius of the input black hole.
why it matters
This supplies the area term required by the Bekenstein-Hawking entropy definition and by scaling theorems such as entropy quadruples on double mass in the UltramassiveBH module. It implements the holographic principle by making entropy proportional to horizon area rather than volume, consistent with the ledger capacity at the horizon. The module documentation positions it within the derivation of black hole thermodynamics from information theory.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.