soundFaithfulCover_injects
plain-language theorem explainer
A sound, faithful certificate cover yields an injection from the witness subtype {d | P d} into the certificate type. Anyone proving countability or cardinality bounds on continuum-facing witness sets cites this. The argument picks a certificate for each witness by classical choice and recovers equality of witnesses from faithfulness of certification.
Claim. Let $C$ be a completion from native data to display data $D$ with certificates $\mathrm{Cert}$, and let $P : D \to \mathrm{Prop}$. If there is a sound, faithful cover of $P$ by $C$ (every $P$-witness has a certificate; certificates issue only to genuine witnesses; a certificate determines its datum), then there exists an injective map $\{d \mid P(d)\} \to \mathrm{Cert}$.
background
In the Primitive Recognition Calculus, a Completion packages a display map from native data $N$ to display data $D$ together with a certification relation $\mathrm{certifies} : \mathrm{Cert} \to D \to \mathrm{Prop}$. Display predicates on $D$ are the continuum-facing statements one hopes to reduce to finite or native certificates.
A SoundFaithfulCover for $P$ strengthens bare coverage in three ways: completeness (every witness carries some certificate), soundness (certificates only land on genuine witnesses), and faithfulness (one certificate cannot certify two distinct data). The module notes that faithfulness is the vacuity-defeating clause: a completion that certifies everything cannot be faithful once $D$ has two points.
This lemma sits in the Finite Certificate Transfer layer, which moves obstruction and legitimacy facts between native and display sides under conservative completion hypotheses.
proof idea
Classical choice supplies, for each witness $w : {d \mid P(d)}$, a certificate via the cover's completeness clause. The candidate injection sends $w$ to that chosen certificate.
For injectivity: if two witnesses map to the same certificate, the choose-spec facts say that certificate certifies both underlying data. Faithfulness of the cover forces the data equal, hence the subtypes equal by Subtype.ext. Soundness is not needed for the injection itself.
why it matters
This is the cardinality hinge under the honest (sound and faithful) cover. The immediate parent is soundFaithfulCover_countable_witnesses: once $\mathrm{Cert}$ is countable, the injection forces the witness set countable. That parent is labeled the "Honest hinge" in the module: continuum-sized witness sets cannot admit a sound, faithful cover by a countable certificate system.
In the Recognition framework this polices continuum claims that pretend to rest on finite certificates. Without faithfulness, "certify everything" collapses the weak layer; with it, uncountable witness sets are ruled out by the sibling non-existence theorem no_soundFaithfulCover_of_uncountable_witnesses. The result is pure set-theoretic transfer, not a forcing-chain step (T5–T8), but it underwrites which display predicates can honestly sit on the native ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.