HawkingQuantum
plain-language theorem explainer
Hawking radiation quanta are modeled as triples consisting of a real energy, a natural number of information bits encoded in correlations, and an entanglement flag set to true. Researchers constructing evaporation models that maintain information via ledger decompression in Recognition Science would cite this object. The declaration introduces the type directly as a structure with no proof obligations or computational steps.
Claim. A Hawking radiation quantum is specified by an energy value $E$ in the reals, an information content $n$ as a natural number carried through correlations, and the proposition that the quantum remains entangled with the black hole interior.
background
The module resolves the black hole information paradox by positing that the ledger records all events without erasure. Black holes compress ledger entries to the horizon under the holographic bound, while Hawking radiation decompresses them. Energy is defined as an alias for the reals in native units. Upstream results include the LedgerFactorization structure, which calibrates the J-cost on the positive reals under multiplication, and the PhiForcingDerived structure for J-cost.
proof idea
The declaration is a structure definition introducing three fields for the quantum: its energy as a real number, its information bits as a natural number, and an entanglement marker fixed to the true proposition. No upstream lemmas are invoked; it functions purely as a type constructor for downstream use in process definitions.
why it matters
This supplies the radiation component for the EvaporationProcess structure that tracks initial black holes and emitted quanta. It advances the ledger-based resolution of the information paradox by providing the carrier for information in radiation, aligning with the framework's emphasis on unitarity through ledger preservation. It touches the open question of explicit information encoding in correlations but closes the basic object definition needed for the evaporation model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.