horizonCells
plain-language theorem explainer
horizonCells counts the number of Planck-area cells on the horizon of an RSBH black hole in RS-native units. Researchers deriving black hole thermodynamics from recognition events cite it to discretize the Bekenstein-Hawking area law. The definition is a direct division of the horizon area by four times the square of the base length ell0.
Claim. For a black hole $bh$ with positive mass in RS-native units, the number of Planck-area cells on the horizon is $A(bh)/(4 ell_0^2)$, where $A(bh)$ is the horizon area and $ell_0$ is the fundamental length unit.
background
RSBH is the structure for a black hole in RS-native units with length, time, and speed of light all set to 1 and mass strictly positive. ell0 is the fundamental length (voxel) set to 1 in the Constants module. horizonArea is the sibling definition that returns the surface area of the event horizon from the Schwarzschild radius in these units.
proof idea
One-line definition that divides the horizon area by the area of one fundamental cell using the constant ell0.
why it matters
This definition supplies the cell count that enters rs_entropy = k_R * horizonCells, realizing the RS Bekenstein-Hawking formula S_BH = (ln φ) · A/(4ℓ₀²). It is invoked by the theorems entropy_quadruples_on_double and rs_entropy_pos. The construction aligns with the module's no-singularity result and the recognition cost k_R = ln φ from the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.