no_faithful_cover_of_uncountable
plain-language theorem explainer
A countable certificate type cannot injectively label an uncountable display type: faithfulness would force the display to be countable. Anyone arguing that continuum objects cannot arise from finite-distinction witnesses cites this cardinality obstruction. The proof is a one-line contraposition of the faithful-cover-implies-countable lemma.
Claim. Let $D$ and $\mathrm{Cert}$ be types with $\mathrm{Cert}$ countable and $D$ uncountable. For any assignment $a : D \to \mathrm{Cert}$, the map $a$ is not injective (not faithful).
background
This module develops the cardinality form of real-line non-nativity in the Primitive Recognition Calculus: continuum objects cannot be produced by countable finite-distinction certificate systems. A certificate assignment $a : D \to \mathrm{Cert}$ is faithful when it is injective, so distinct certified data receive distinct certificates. That is the minimal soundness condition a genuine witness must satisfy; the vacuous layer drops exactly this condition.
The immediate upstream fact is that a faithful cover into a countable certificate system forces the covered type to be countable (via the cardinal comparison $\lvert D\rvert \le \lvert\mathrm{Cert}\rvert \le \aleph_0$). The present theorem is the contrapositive packaging of that implication for uncountable display types.
proof idea
Term-mode one-liner. Assume faithfulness of assign. Apply faithful_cover_into_countable_imp_countable to conclude that $D$ is countable, contradicting the hypothesis that $D$ is uncountable. No separate injectivity unfolding is needed: Faithful is definitionally injectivity, and the upstream lemma already consumes that hypothesis.
why it matters
This is the abstract cardinality weapon used by real_not_faithfully_certifiable, which specializes it to $\mathbb{R}$ and states the Non-Nativity of the Real Line in cardinality form: no countable finite-distinction certificate system faithfully covers the continuum. Downstream, that result underwrites the claim that $\mathbb{R}$ enters Recognition Science only through a completion interface, not from distinction alone.
In the broader foundation, the forcing chain already fixes discrete structure (eight-tick octave, $D=3$). The present lemma separates that discrete certificate layer from continuum surplus: any attempt to treat the real line as a native display of countable certificates fails injectivity. It does not itself force $D=3$ or the $J$-cost; it only blocks continuum nativity at the set-cardinality level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.