RSBH
plain-language theorem explainer
RSBH is the record type carrying a positive real mass for black holes in units where length, time, and c equal 1. Workers on ultramassive objects such as TON 618 cite it when deriving entropy scaling and Hawking temperature. The declaration is a direct structure definition with no lemmas or reductions.
Claim. An RSBH consists of a real number $M$ together with a witness that $M>0$, expressed in units where the fundamental length, time, and speed of light are all unity.
background
Recognition Science adopts native units with fundamental length, time, and $c$ set to 1. The module treats ultramassive black holes ($M$ ≳ $10^{10} M_☉$), taking TON 618 as the running example. It records the mass together with its positivity proof so that downstream constructions can invoke the J-cost finiteness result and the recognition Boltzmann constant $k_R = ln φ$. Upstream, the radius definition from cellular automata supplies the local neighborhood size used in discrete models, while mass_pos from the phi-ladder supplies the positivity convention for real numbers that is reused here.
proof idea
The declaration is a direct structure definition introducing the two fields mass and mass_pos. No tactics or lemmas are invoked; the type simply packages the data required by every later black-hole construction in the module.
why it matters
RSBH supplies the carrier type for the entire ultramassive-BH development. It is used by horizonArea, horizonCells, rs_entropy, rs_hawkingTemp, and the entropy-quadruples theorem. The structure thereby implements the paper claim that entropy scales as $M^2$ and that J-cost remains finite on the interior, closing the interface between the general J-cost machinery and concrete gravitational objects. It touches the open question of whether the Hamiltonian approximation bound remains valid beyond the small-strain regime.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.