faithful_cover_into_countable_imp_countable
plain-language theorem explainer
A faithful (injective) assignment from a witness type W into a countable certificate type forces W itself to be countable. Anyone arguing the cardinality obstruction to real-line nativity cites this direction. The proof is a short cardinal comparison: injectivity gives |W| ≤ |Cert| ≤ ℵ₀, hence Countable W.
Claim. Let $W$ and $\mathrm{Cert}$ be types, with $\mathrm{Cert}$ countable. If $\mathrm{assign}: W \to \mathrm{Cert}$ is faithful (i.e., injective), then $W$ is countable.
background
In the Primitive Recognition Calculus, a certificate assignment is a map from a display or witness type into a certificate type. Faithfulness means the assignment is injective: distinct certified data receive distinct certificates. The module treats this as the minimal soundness condition a genuine witness must satisfy; the vacuous layer drops exactly that condition.
The local setting is RealLineNonNativity: the claim that the continuum cannot arise as a natively certified display under a countable certificate system. Countability of the certificate type is the standing hypothesis; the question is what that forces on the covered type.
Upstream, Mathlib supplies the cardinal toolkit used here (Cardinal.mk_le_of_injective, Cardinal.mk_le_aleph0, and the equivalence of countability with cardinality at most $\aleph_0$). The in-module definition of Faithful is literally injectivity of the assignment.
proof idea
Unpack Faithful as injectivity of assign. Rewrite the goal via Cardinal.mk_le_aleph0_iff so that Countable W becomes $|W| \le \aleph_0$. Injectivity yields $|W| \le |\mathrm{Cert}|$ by Cardinal.mk_le_of_injective. Countability of Cert yields $|\mathrm{Cert}| \le \aleph_0$ by Cardinal.mk_le_aleph0. Transitivity of $\le$ on cardinals closes the proof. Pure term-mode cardinal arithmetic; no Recognition-specific lemmas beyond the Faithful unpacking.
why it matters
This is the positive half of the cardinality obstruction in RealLineNonNativity. Downstream, no_faithful_cover_of_uncountable contraposes it: if D is uncountable and Cert is countable, no assignment D → Cert can be Faithful. The sibling faithful_cover_into_countable_iff_countable packages both directions as the dividing line: a faithful cover into a countable system exists iff the witness type is countable.
That boundary is exactly where the cardinality form of the doctrine bites (uncountable witnesses such as ℝ) versus where a finer geometric obstruction is still needed (countable witnesses). In the Recognition framework this supports the claim that the real line is not a native certified display under countable certificate systems, feeding the non-nativity argument rather than the T0–T8 forcing chain directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.