BHResolution
plain-language theorem explainer
BHResolution enumerates five canonical resolutions to the black hole information paradox inside the Recognition Science ledger framework. Quantum gravity researchers would cite the enumeration when mapping ledger preservation to standard proposals such as information loss or ER=EPR recovery. The declaration is a direct inductive definition that introduces the five cases and derives Fintype for immediate cardinality use.
Claim. Let $R$ denote the set of resolutions to the black hole information paradox. Then $R$ consists of the five cases: information loss, remnant models, AdS/CFT restoration, soft-hair restoration via BMS symmetries, and ER=EPR wormhole recovery.
background
The module treats the black hole information paradox by observing that the recognition ledger preserves information while Hawking radiation carries Z-complexity. It lists five standard resolutions tied to configuration dimension D=5: information loss, remnants, AdS/CFT restoration, soft-hair (BMS symmetries), and ER=EPR wormhole recovery. No upstream lemmas are required; the definition stands alone to support downstream cardinality statements.
proof idea
The declaration is the inductive definition that directly introduces the five constructors informationLoss, remnants, adsCftRestoration, softHairBMS, and erEprWormhole, then derives DecidableEq, Repr, BEq, and Fintype in one step.
why it matters
BHResolution supplies the finite enumeration that BHInformationCert and bhResolution_count use to prove Fintype.card BHResolution = 5. It places the Recognition Science ledger preservation claim against the five literature proposals, with the count fixed at configDim D=5. The definition closes the enumeration step so that later theorems can assert information retention without enumerating cases again.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.