ArtifactFor
plain-language theorem explainer
A completion admits a non-native artifact for a display predicate P when some display datum satisfies P yet carries no certificate. Anyone proving conservativity of a completion cites this as the negation of certificate coverage. The body is a one-line existential definition over display data and the certifies relation.
Claim. Given a completion $C$ from native data to display data with certificates, and a display predicate $P$, $C$ has an artifact for $P$ when there exists a display datum $d$ such that $P(d)$ holds and no certificate $c$ satisfies $\mathrm{certifies}_C(c,d)$.
background
The module studies when a completion from native recognition data $N$ to display data $D$ is conservative: every display predicate that holds is backed by a finite native certificate. A completion interface supplies a display map $N\to D$ and a relation $\mathrm{certifies}:\mathrm{Cert}\to D\to\mathrm{Prop}$.
Certificate coverage means every display datum satisfying $P$ has some certificate. The complementary notion is a non-native artifact: a witness in $D$ that meets $P$ with no certificate at all. Conservativity is then exactly the absence of such artifacts.
Upstream dimension constants $D=3$ (T8/T9) and CKM-style certificate structures appear only as type-parameter names in the dependency graph; the definition itself is purely logical and does not use their numeric content.
proof idea
Pure definitional expansion: unfold to an existential over display data $d$ with $P,d$ and the negated existence of a certificate under $C.\mathrm{certifies}$. No lemmas or tactics; the Prop is the statement.
why it matters
This is the negative half of the conservativity dictionary. The sibling theorem $\mathrm{ConservativeFor},C,P\leftrightarrow\neg\mathrm{ArtifactFor},C,P$ is proved by unfolding both sides, and the module headline packages that equivalence with the fact that the identity completion is conservative for every predicate.
In the Recognition framework the point is methodological: display-layer constructions (products, bridges, derived observables) must not invent uncertified structure. Naming artifacts makes "no new physics from completion" a checkable Prop rather than a slogan. It does not itself force $D=3$, $\phi$, or the eight-tick octave; those enter only when concrete completions are instantiated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.