BHInformationCert
plain-language theorem explainer
Defines a structure certifying that the finite set of black hole information paradox resolutions has cardinality exactly five. Quantum gravity researchers would cite it to record the canonical count inside the Recognition Science ledger. The declaration is a bare structure with a single field that directly invokes Fintype.card on the enumerated resolution type.
Claim. A structure certifying that the set of black hole information paradox resolutions has cardinality five, where the resolutions comprise information loss, remnants, AdS/CFT restoration, soft-hair BMS symmetries, and ER=EPR wormhole recovery.
background
The module treats the black hole information paradox inside Recognition Science by enumerating five canonical resolutions that correspond to configuration dimension D=5. The resolutions are information loss, remnants, AdS/CFT restoration, soft-hair via BMS symmetries, and ER=EPR wormhole recovery. Recognition Science asserts that the recognition ledger preserves information while Hawking radiation carries Z-complexity.
proof idea
This is a structure definition with no proof body. It directly encodes the cardinality assertion by referencing Fintype.card applied to the inductive BHResolution type that lists the five cases.
why it matters
The structure supplies the formal certificate for the five resolutions listed in the module. It is instantiated by the downstream definition bhInformationCert. The module doc-comment records that RS places the recognition ledger as the information-preserving mechanism, aligning with the framework's discrete treatment of physical paradoxes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.