identity_conservative
plain-language theorem explainer
The identity completion is conservative for every predicate on the native type: any display datum that satisfies the predicate is certified by itself. Foundation work on certificate-preserving completions cites this as the trivial base case. The argument is immediate: exhibit the datum as its own certificate under equality certification.
Claim. For any type $N$ and any predicate $P : N \to \mathrm{Prop}$, the identity completion on $N$ (display map $\mathrm{id}$, certification relation $c = d$) is conservative for $P$: every $d$ with $P(d)$ carries a certificate.
background
In the primitive recognition calculus, a completion packages a display map from native data into a display type together with a certification relation between certificates and display data. Conservativity for a predicate $P$ means $P$ is certificate-covered: every display datum satisfying $P$ admits some certificate under that relation. Equivalently, there are no uncertified artifacts for $P$.
The identity completion is the base interface: native type, display type, and certificate type all coincide with $N$; display is the identity; certification is equality. Its doc-comment states that it is conservative whenever the predicate itself supplies a certificate, and that this is the base case for certificate-preserving completions.
The local module develops conservativity as the absence of non-native artifacts and records headline equivalences linking conservativity, artifact-freeness, and product stability of completions.
proof idea
Unfold conservativity to certificate coverage. Given a display datum $d$ with $P(d)$, take the certificate to be $d$ itself. Under the identity completion, certification is equality, so reflexivity closes the witness. No external lemmas are required beyond the definitions of the identity completion and of conservativity as certificate coverage.
why it matters
This is the base case that the completion-conservativity headline packages: a completion is conservative exactly when it has no uncertified display artifacts, and the identity completion is conservative for every predicate. The headline theorem quotes this result as its second conjunct.
It also discharges both legs of the identity certificate audit in the hard-problem audit layer: legitimate and pathology predicates on a finite certificate type are each conservative under the identity completion. That audit is the trivial reference point against which nontrivial certificate-preserving completions are compared.
Within Recognition Science foundation work, the result anchors the claim that native recognition data need no extra display layer to stay certificate-covered, before product and other structured completions are shown to preserve the same property.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.