IndisputableMonolith.Shims.CountableEquiv
This module supplies classical shims that turn Mathlib Countable instances for inhabited types into explicit surjections from the naturals. Researchers building enumerations inside the Recognition Science monolith cite it when they must extract concrete sequences from mere existence statements. The definitions coerce the Prop-level witness via Nonempty.some and invert the injection classically.
claimFor an inhabited type $α$ that is Countable, the module yields a surjection $ℕ → α$ obtained by extracting an injection $α ↪ ℕ$ and inverting it.
background
Mathlib defines Countable α propositionally as the mere existence of an injection into ℕ. Recognition Science constructions frequently require explicit enumerations of countable defect sets or states on the phi-ladder, which demands Type-level functions rather than Prop-level existence. The module therefore provides shims that bridge this gap using Nonempty coercion to access the witness inside definitions.
proof idea
This is a definition module, no proofs. The sibling declarations implement the classical conversion by extracting the injection witness via Nonempty.some and building the surjection by inverting it.
why it matters in Recognition Science
The module feeds downstream Recognition Science theorems that enumerate countable collections of defects or forcing states. It closes the gap between Mathlib's Prop-level countability and the concrete sequences needed for the unified forcing chain and mass-ladder constructions.
scope and limits
- Does not produce constructive enumerations without classical choice.
- Does not apply to types lacking an Inhabited instance.
- Does not define countability notions beyond Mathlib.
- Does not guarantee decidability of the resulting enumeration.