SoundFaithfulCover
plain-language theorem explainer
A sound, faithful certificate cover is the three-part interface on a completion: every witness of a display predicate gets a certificate, certificates land only on genuine witnesses, and each certificate pins at most one datum. Downstream continuum and countability obstructions cite this packing. Pure structure definition; no proof obligations.
Claim. Fix a completion $C$ from native data $N$ to display data $D$ with certificate type $\mathrm{Cert}$, and a display predicate $P$ on $D$. A sound, faithful cover of $P$ by $C$ is the conjunction of three properties: (completeness) every $d$ with $P(d)$ admits some certificate $c$ such that $c$ certifies $d$; (soundness) if $c$ certifies $d$ then $P(d)$; (faithfulness) if the same $c$ certifies both $d_1$ and $d_2$ then $d_1=d_2$.
background
The ambient module develops finite-certificate transfer for the primitive recognition calculus: how much of a completed (display) continuum can be recovered from finite native certificates without smuggling continuum structure into the certificate layer.
A completion (from CompletionConservativity) is an interface $C$ with a display map $N\to D$ and a relation $\mathrm{certifies}:\mathrm{Cert}\to D\to\mathrm{Prop}$. Display predicates $P:D\to\mathrm{Prop}$ are the statements one might hope to certify. The weak layer of the calculus drops faithfulness and thereby becomes vacuous: one can certify everything by a single dummy certificate. The third field here restores the missing constraint.
The companion remark in-module records the vacuity-defeating fact: a completion that certifies every display point cannot be faithful once $D$ has two distinct points. So the three-field package is genuinely constrained, not a free lunch.
proof idea
No proof. This is a Prop-valued structure whose fields are exactly the three universal statements (completeness, soundness, faithfulness). Inhabitants are assembled by supplying those three proofs; consumers project the fields or pass the whole cover into the injection and countability lemmas below.
why it matters
This is the honest hinge the weak certificate layer could not state. It feeds four immediate results in the same module: the cover injects the witness set into $\mathrm{Cert}$; with countable certificates the witness set is countable; therefore no such cover exists for any predicate with uncountably many witnesses; and as a named instance, no countable certificate system soundly and faithfully covers the real line (the always-true predicate on $\mathbb{R}$).
In Recognition Science terms this is foundation-level hygiene for the primitive recognition calculus: finite distinction data cannot soundly and faithfully certify a continuum. That blocks a common cheat path when lifting native discrete structure (eight-tick octave, $D=3$ spatial forcing, $\varphi$-ladder) into completed display objects. It does not itself force physics constants; it polices what completions are allowed to claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.