BlackHole
plain-language theorem explainer
A structure defines a Schwarzschild black hole by a positive real mass M. Researchers deriving black hole thermodynamics from Recognition Science cite it as the input type for entropy and temperature formulas. The definition is a record type that pairs the mass with an explicit positivity constraint.
Claim. A Schwarzschild black hole is a pair $(M, p)$ where $M > 0$ is a real number representing the mass.
background
The module derives Bekenstein-Hawking entropy and Hawking temperature from Recognition Science, treating the horizon area as a measure of ledger information capacity and temperature as arising from the τ₀-scale at the horizon. The structure BlackHole supplies the minimal data needed for these derivations. It mirrors the upstream BlackHole structure in BlackHoleInformation, which likewise records a positive real mass, and reuses the positivity pattern from the meson spectrum theorem mass_pos that establishes 0 < mesonMass k via pow_pos phi_pos k.
proof idea
Structure definition introducing the type with fields mass : ℝ and mass_pos : mass > 0. No tactics or lemmas are applied; the declaration directly encodes the data and constraint.
why it matters
This supplies the input type for every downstream result in the module, including bekensteinHawkingEntropy (S_BH = k_B A / (4 l_P²)), entropy_proportional_to_area, hawkingTemperature, and evaporationTime. It realizes the QG-001 target stated in the module doc: entropy proportional to horizon area rather than volume, following the holographic bound that emerges from ledger capacity in Recognition Science. The structure therefore anchors the entire black-hole thermodynamics derivation before any formulas are applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.