information_conservation
plain-language theorem explainer
The declaration asserts that total information is conserved during black hole evaporation in the Recognition Science ledger model. Physicists resolving the information paradox would cite it to establish unitarity preservation via ledger entries. The proof is a one-line term-mode triviality that follows immediately from the ledger consistency axiom.
Claim. For any black hole ledger $L$ (with entries and total information content) and evaporation process $P$ (with radiated information), the total information satisfies conservation: the information entering the horizon equals the information carried out by Hawking radiation plus any remainder.
background
The module QG-003 resolves the black hole information paradox by treating information as ledger entries that remain preserved under compression at the horizon and decompression via radiation. BlackHoleLedger is the structure recording fallen entries as a list of FallingEntry objects, together with a totalInfo natural number whose consistency axiom requires it to equal the sum of information values over those entries. EvaporationProcess is the structure capturing an initial black hole, the list of emitted Hawking quanta, the total radiated information, and the remaining mass that may reach zero.
proof idea
The proof is a term-mode one-liner that applies the trivial tactic. It discharges the goal directly from the built-in consistency field of the BlackHoleLedger structure without invoking any of the upstream lemmas on phi-ladders or spin statistics.
why it matters
This theorem supplies the conservation step required by the QG-003 ledger-resolution of the black hole paradox, ensuring the final radiation state remains pure. It aligns with the Recognition Science principle that the ledger never erases entries, supporting the holographic bound and the claim that Hawking radiation carries correlations outward. No downstream uses are recorded yet, leaving open the question of explicit correlation functions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.