EvaporationProcess
plain-language theorem explainer
EvaporationProcess records a black hole evaporation event as an initial BlackHole of positive mass, a list of HawkingQuantum each carrying energy and information bits while entangled, a natural number for total radiated information, and a real number for remaining mass. Physicists modeling unitarity in quantum gravity via ledger preservation would cite this structure when proving information conservation. The declaration is a bare record type with four fields and no attached computation or proof.
Claim. An evaporation process consists of an initial black hole $B$ with mass $m > 0$, a list of Hawking quanta where each quantum has energy $E$, carries $k$ information bits in correlations, and satisfies entanglement, a natural number $N$ counting total radiated information, and a real number $m'$ for the remaining mass after emission.
background
Recognition Science treats all events as entries in a fundamental ledger that is never erased. A BlackHole is a structure whose only data is mass in Planck units together with the positivity condition mass > 0. HawkingQuantum is a structure carrying energy, an information-bit count, and the entanglement flag. The module sets the local setting as the ledger-based resolution of the black-hole information paradox: black holes compress ledger entries to the horizon while Hawking radiation decompresses them without loss of unitarity.
proof idea
The declaration is a structure definition with an empty proof body. It simply introduces the four fields initialBH : BlackHole, radiation : List HawkingQuantum, radiatedInfo : ℕ, and remainingMass : ℝ, each equipped with its one-line doc comment.
why it matters
EvaporationProcess supplies the data type required by the downstream information_conservation theorem, which asserts ledger preservation of total information. It implements the central mechanism step of the QG-003 resolution: black-hole compression followed by radiation decompression. The construction directly supports the Recognition Science claim that the ledger maintains unitarity throughout evaporation, consistent with the eight-tick octave and simplicial-ledger foundations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.