horizonArea
plain-language theorem explainer
The horizon area definition computes the event horizon surface area for a black hole with positive mass in RS-native units as four pi times the square of its Schwarzschild radius. Astrophysicists working on ultramassive objects such as TON 618 would cite it when linking geometry to the recognition entropy formula. The definition is a direct algebraic substitution of the classical sphere area formula.
Claim. For a black hole with positive mass $M$ in units where the fundamental length scale is unity, the horizon area $A$ satisfies $A = 4π r_s^2$ where $r_s = 2GM$ is the Schwarzschild radius, equivalently $A = 16π G^2 M^2$.
background
In the Recognition Science treatment of ultramassive black holes, an RSBH consists of a positive real mass in units with Planck length and time set to one. The Schwarzschild radius is the standard expression $2GM$ in these units. The module formalizes the RS view that the black hole interior is a maximal J-cost state rather than a curvature singularity, and it introduces the recognition Boltzmann constant $k_R = ln φ$ as the cost per recognition event.
proof idea
The definition is a one-line wrapper that applies the classical surface area formula for a sphere directly to the Schwarzschild radius of the given black hole.
why it matters
This supplies the geometric input required by downstream results such as rs_entropy_eq, rs_entropy_pos, entropy_quadruples_on_double, and the Bekenstein-Hawking entropy definitions in the Quantum module. It realizes the module's RS entropy formula $S_{BH} = k_R · A/(4ℓ_0^2)$ and connects the phi-forcing chain to black hole thermodynamics, replacing $k_B$ with $k_R = ln φ$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.