Faithful
plain-language theorem explainer
Faithfulness means a certificate map is injective: distinct data get distinct certificates. It is the minimal soundness condition for a genuine witness, and the vacuous layer is defined by dropping exactly this. Downstream cardinality arguments cite it to show that countable certificate systems cannot cover uncountable displays such as ℝ. The body is a one-line abbreviation of function injectivity.
Claim. An assignment $\mathrm{assign}: D \to \mathrm{Cert}$ is faithful when it is injective: if $\mathrm{assign}(d_1)=\mathrm{assign}(d_2)$ then $d_1=d_2$. Equivalently, distinct certified data receive distinct certificates.
background
In the Primitive Recognition Calculus, a certificate system is a type $\mathrm{Cert}$ together with an assignment from display (or witness) data $D$ into $\mathrm{Cert}$. The intended reading is that a certificate should determine what it certifies. Faithfulness is exactly that soundness demand: the assignment must be injective.
The surrounding module develops the cardinality form of non-nativity for the real line. Countable certificate systems are the natural comparison class once distinction has forced arithmetic (countable) structure. Injectivity then becomes a cardinality weapon: an injective map into a countable type forces the domain to be countable.
Upstream, related "faithful" language appears for log-characters on primes (independence of prime weights), but here the term is purely the set-theoretic injectivity predicate on certificate assignments.
proof idea
One-line definitional wrapper: the proposition is definitionally Function.Injective assign. No tactics or lemmas are involved; downstream theorems unpack the definition and apply standard cardinality facts about injective maps into countable types.
why it matters
This predicate is the hinge for the real-line non-nativity chain. It feeds faithful_cover_into_countable_imp_countable (injective cover into countable Cert forces Countable W), no_faithful_cover_of_uncountable, and real_not_faithfully_certifiable. Those are restated as real_not_forced_from_distinction: distinction forces countable arithmetic (LogicNat), never $\mathbb{R}$.
It also marks the honest refinement boundary: countable_witness_has_faithful_cover and the iff with countability show that when witnesses are countable (algebraic cycles, rational Hodge classes), cardinality gives no obstruction and a finer geometric residual is required. In Recognition terms, this separates what the forcing chain can native-certify from continuum displays that remain non-native under countable certificates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.