BlackHole
plain-language theorem explainer
A record structure that parameterizes a black hole by its positive real mass in Planck units. Workers on holographic entropy or ledger-based unitarity cite it when instantiating horizon models inside Recognition Science. The declaration is a direct two-field record with an embedded positivity constraint.
Claim. A black hole is a pair $(M, p)$ where $M$ is a real number (mass in Planck units) and $p$ is a proof that $M > 0$.
background
The module sets the local setting for QG-003: black-hole information is preserved because every event is a ledger entry; the horizon compresses entries without erasure while Hawking radiation decompresses them. Mass is imported as the alias ℝ from RSNativeUnits. The structure supplies the common input type for all subsequent black-hole functions in the same file and in the sibling BekensteinHawking module.
proof idea
Direct structure definition; two fields are declared and the positivity guard is attached as a field. No tactics or lemmas are applied.
why it matters
Supplies the input type for bekensteinHawkingEntropy, entropyInBits, hawkingTemperature, evaporationTime and horizonArea in the BekensteinHawking module. It realizes the module-doc claim that a black hole equals ledger compression and thereby supports the unitarity argument that closes the information paradox. It sits inside the quantum domain and feeds the holographic-bound statements that appear downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.