completion_conservativity_headline
plain-language theorem explainer
A completion from native data to display data is conservative for a display predicate exactly when that predicate has no uncertified artifacts; the identity completion is conservative for every native predicate. Certificate architects assembling display layers cite this as the headline conservativity package. The proof is a one-line pairing of the local iff lemma with the identity-conservativity fact.
Claim. For any completion $C$ from native type $N$ to display type $D$ with certificate type $\mathrm{Cert}$, and every display predicate $P:D\to\mathrm{Prop}$, $C$ is conservative for $P$ if and only if there is no uncertified display artifact for $P$. Moreover, the identity completion on $N$ is conservative for every predicate on $N$.
background
In the primitive recognition calculus, a completion is an interface that maps native data $N$ into display data $D$ and supplies a certificate type $\mathrm{Cert}$ together with a relation "certifies" between certificates and display points. Display predicates are meant to be witnessed by finite or native certificates rather than free-floating display values.
Conservativity for a predicate means every display point satisfying the predicate carries some certificate (certificate-covered). An artifact is the dual failure mode: a display point that satisfies the predicate yet admits no certificate. The identity completion is the trivial completion that treats native data as already displayed, so every native predicate is automatically certificate-covered.
This module packages those notions so later strong-closure certificates can assert that display layers introduce no non-native content.
proof idea
Term-mode pair constructor. The first conjunct is discharged by applying the local lemma that conservativity is equivalent to absence of artifacts, specialized to the given completion $C$ and quantified over display predicates. The second conjunct is the already-proved fact that the identity completion is conservative for every native predicate. No further rewriting or case analysis is required.
why it matters
This is the headline conservativity statement for completion interfaces in the primitive recognition calculus. Downstream, the strong-closure certificate in Delta-native strong closure assembles a closed theorem surface of display-real, generable-carrier, certified-analytic, and transformer entries; that certificate relies on knowing that completions do not smuggle uncertified display content and that the identity layer is always safe.
In the broader Recognition framework this sits in Foundation: it polices the native-to-display boundary so later forcing-chain and mass-ladder constructions can treat display objects as certificate-backed rather than free. It does not itself force dimension, $\varphi$, or the eight-tick octave; it only guarantees that whatever display layer is chosen stays conservative.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.