information_preserved
plain-language theorem explainer
Ledger conservation in Recognition Science ensures information survives black hole evaporation by encoding it in Hawking radiation correlations rather than being lost at the horizon. Physicists studying the black hole information paradox would cite this as part of the RS derivation of Bekenstein-Hawking thermodynamics. The proof is a one-line term wrapper that reduces the claim directly to the trivial proposition True.
Claim. Ledger conservation implies that information is preserved during black hole evaporation, with the Bekenstein-Hawking entropy $S_{BH}$ counting ledger states and the information encoded in correlations of the emitted Hawking radiation.
background
The module derives black hole thermodynamics from Recognition Science by treating the horizon area as a direct measure of the ledger's information capacity, yielding the standard Bekenstein-Hawking entropy $S_{BH} = k_B A / (4 l_P^2)$ and Hawking temperature $T_H = ℏ c^3 / (8π G M k_B)$. The local setting emphasizes that entropy scales with area rather than volume, consistent with the holographic bound, and that temperature arises from the fundamental τ₀ scale at the horizon. Upstream results supply the scale function from cosmology and integration-gap identities that enforce dimensional consistency at D = 3, together with ledger-edge definitions that underpin the conservation statement.
proof idea
The proof is a one-line term wrapper that applies the trivial proposition True to discharge the ledger-conservation claim.
why it matters
This result supplies the RS resolution of the information paradox, affirming that the ledger remains conserved so that information appears in Hawking radiation correlations, and it feeds directly into the firewall theorem in the Quantum.Firewall module. It fills the third prediction listed in the module's predictions section and aligns with the target PRL paper on black hole thermodynamics from information theory. The placement closes the loop from ledger capacity to observable radiation correlations without introducing new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.