conservative_iff_no_artifact
plain-language theorem explainer
Conservativity of a completion for a display predicate is equivalent to the absence of uncertified display artifacts. Anyone working the primitive recognition calculus or citing the completion-conservativity headline will use this biconditional. The proof is a short classical unfolding: certificate-covered is definitionally the negation of an artifact.
Claim. Fix a completion $C$ from native data $N$ to display data $D$ with certificate type $\mathrm{Cert}$, and a display predicate $P:D\to\mathrm{Prop}$. Then $C$ is conservative for $P$ (every $d$ with $P(d)$ carries some certificate) if and only if there is no artifact for $P$ (no $d$ with $P(d)$ and no certificate).
background
The module sets up a completion interface: a map from native data $N$ to display data $D$, together with a certification relation from certificates $\mathrm{Cert}$ to display points. The point is to track which display claims are backed by finite/native certificates rather than free-floating display structure.
A display predicate $P$ is certificate-covered when every display datum satisfying $P$ admits some certificate under $C$. Conservativity for $P$ is defined to be exactly that covering property. An artifact for $P$ is the dual witness: some display $d$ with $P(d)$ but no certificate at all.
This sits in the foundation layer of Recognition Science, where display-level structure must not invent content beyond what native recognition data can certify. The equivalence below is the bookkeeping lemma that makes "conservative" and "no artifact" interchangeable.
proof idea
Term-mode proof by unfolding the three definitions (conservativity, certificate-covered, artifact) and splitting the biconditional.
Forward: from certificate-covered, any putative artifact $\langle d, P(d), \text{no cert}\rangle$ is immediate contradiction, since covering supplies a certificate for that $d$.
Backward: assume no artifact; for arbitrary $d$ with $P(d)$, argue by contradiction that a certificate must exist, else $\langle d, P(d), \text{no cert}\rangle$ would be an artifact. Pure classical quantifier logic; no external lemmas.
why it matters
This is the local equivalence that the module's headline packages. Downstream, completion_conservativity_headline states that a completion is conservative exactly when it has no uncertified display artifacts, and that the identity completion is conservative for every predicate; the first conjunct is literally this theorem quantified over $P$.
In the Recognition framework the point is methodological: display completions (identity, product, and later certificate-preserving constructions) must not smuggle non-native content. Equating conservativity with artifact-freeness gives a clean audit criterion before those constructions are stacked. It does not itself force $\varphi$, the eight-tick octave, or $D=3$; it is infrastructure for the primitive recognition calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.