horizonArea
plain-language theorem explainer
Black hole horizon area is expressed as sixteen pi times mass squared in units where gravitational constant and speed of light equal one. Researchers deriving holographic entropy bounds or recognition saturation limits cite this when linking geometry to Bekenstein-Hawking entropy and bandwidth consumption. The definition is a direct algebraic substitution of the Schwarzschild radius into the spherical area formula.
Claim. The horizon area of a Schwarzschild black hole with mass $M$ (in natural units) is $A = 16 pi M^2$.
background
In the Black Hole Bandwidth module a black hole is defined as the limiting case of full recognition bandwidth consumption, where the recognition operator is maximally busy at every scale. Horizon area supplies the geometric input for entropy and bandwidth: the module states that Bekenstein-Hawking entropy equals four pi M squared and recognition bandwidth at the horizon is entropy divided by the product of the recognition Boltzmann constant and the eight-tick period. Upstream definitions in Gravity.UltramassiveBH and Quantum.BekensteinHawking compute the same area from the Schwarzschild radius via four pi r_s squared, confirming the reduction to sixteen pi M squared when r_s equals two M.
proof idea
The definition is a direct closed-form expression obtained by substituting the Schwarzschild radius into the spherical area formula. No lemmas or tactics are applied; the body is the algebraic identity 16 * pi * M^2.
why it matters
This definition supplies the geometric factor for downstream entropy results including entropy_quadruples_on_double, rs_entropy_eq, horizonCells, and bekensteinHawkingEntropy. It supports the module claim that black holes are maximally saturated, with area directly proportional to entropy and no excess bandwidth for additional structure, consistent with the eight-tick octave and the forcing-chain derivation of three spatial dimensions. It closes the input needed for Hawking temperature and information-conservation arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.