faithful_cover_into_countable_iff_countable
plain-language theorem explainer
A type W admits an injective map into the naturals if and only if W is countable. This is the cardinality dividing line in the primitive recognition calculus: uncountable witness types cannot carry a faithful certificate assignment into any countable certificate system, while countable ones always can. The proof is a two-line iff by the two one-sided lemmas already in the module.
Claim. For any type $W$, there exists an injective assignment $W \to \mathbb{N}$ if and only if $W$ is countable. (Injectivity is the faithfulness condition: distinct witnesses receive distinct certificates.)
background
In the RealLineNonNativity module of the primitive recognition calculus, a certificate assignment assign : D → Cert is called faithful when it is injective: distinct certified data get distinct certificates. That is the minimal soundness condition a genuine witness must satisfy; the vacuous layer drops exactly this injectivity.
One direction is already proved: any faithful cover into a countable certificate system forces the covered type to be countable (via the cardinal comparison $\lvert W\rvert \le \lvert\mathrm{Cert}\rvert \le \aleph_0$). The converse is the honest refinement that countable witnesses escape the cardinality weapon: any countable $W$ admits an injective map into $\mathbb{N}$, so cardinality alone gives no obstruction when the true witnesses are countable (as for algebraic cycles and rational Hodge classes).
This theorem packages both directions as a single equivalence, marking the boundary where the cardinality form of the doctrine stops biting.
proof idea
Term-mode constructor on the biconditional. Left-to-right: unpack the existential witness assign and the faithfulness hypothesis, then apply faithful_cover_into_countable_imp_countable (injective map into a countable type implies countable). Right-to-left: from [Countable W], apply countable_witness_has_faithful_cover, which itself is a one-line use of Mathlib's exists_injective_nat. No new cardinal arithmetic is done here.
why it matters
This is the clean dividing line stated in the module doc-comment: a faithful cover into a countable system exists iff the witness type is countable. Upstream, it closes the pair faithful_cover_into_countable_imp_countable and countable_witness_has_faithful_cover. Downstream siblings such as no_faithful_cover_of_uncountable and real_not_faithfully_certifiable use the negative half to rule out the real line (and other uncountable types) as faithfully certifiable witnesses under a countable certificate system.
In the Recognition Science foundation layer this separates two obstruction regimes. Uncountable witnesses are killed by pure cardinality. Countable witnesses (algebraic cycles, rational Hodge classes, discrete ledger data) survive cardinality and need a finer geometric obstruction, such as a diffuse residual. The theorem itself is pure set theory; its place in the framework is to make that regime split explicit and reusable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.