BlackHolePredictions
plain-language theorem explainer
Recognition Science packages its black hole information predictions into a three-field boolean structure asserting Page curve recovery in Hawking radiation, absence of a horizon firewall, and unitarity of the final evaporated state. A researcher comparing ledger models to the information paradox would cite this record when stating the concrete outcomes of the RS resolution. The declaration is a plain record type with no computation or lemmas.
Claim. Let $P$ be the record whose fields are a boolean asserting information recovery via the Page curve, a boolean asserting no firewall at the horizon, and a boolean asserting that the final state after evaporation remains pure.
background
The module resolves the black hole information paradox by treating information as ledger entries that remain preserved under compression at the horizon. Black holes act as ledger compression points obeying the holographic bound, while Hawking radiation decompresses entries through correlations without erasure. The structure collects the resulting predictions that follow from this ledger preservation mechanism.
proof idea
The declaration is a structure definition that introduces three named boolean fields with no proof body, tactics, or upstream lemmas applied.
why it matters
This structure supplies the type instantiated by the downstream rsPredictions, which sets page curve recovery to true, firewall presence to false, and final purity to true. It supports the QG-003 target of resolving the paradox through ledger preservation, aligning with the framework's core claim that information is never lost. The module documentation notes soft hair as a possible experimental channel, though it is omitted from the structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.