bhResolution_count
plain-language theorem explainer
The theorem establishes that the finite type enumerating black hole information paradox resolutions has cardinality five. Quantum gravity researchers examining information preservation would cite this to confirm the standard list of five resolutions inside the Recognition Science ledger. The proof is a one-line decision procedure that evaluates the Fintype.card instance on the inductive type with exactly five constructors.
Claim. The finite type of black hole information paradox resolutions has cardinality five: $ |BHResolution| = 5 $.
background
The module enumerates five canonical resolutions of the black hole information paradox, identified with configDim D = 5. These comprise 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
The proof is a one-line wrapper that applies the decide tactic to compute Fintype.card directly from the inductive definition of BHResolution, which derives the required Fintype instance from its five constructors.
why it matters
This supplies the cardinality field used by bhInformationCert to certify the five resolutions. It completes the enumeration step in the Black Hole Information Paradox from RS module and aligns with the framework claim that the recognition ledger resolves the paradox across five channels. It touches the open question of which resolution is physically realized.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.