identityCompletion
plain-language theorem explainer
The identity completion treats native data as its own display and takes equality as the certificate relation. It is the trivial base case of a certificate-preserving completion: every true display fact is certified by the datum itself. Downstream conservativity and audit lemmas cite it as the zero-artifact reference completion.
Claim. For any type $N$, the identity completion is the completion interface with native, display, and certificate types all equal to $N$, display map the identity $N\to N$, and certificate relation $\mathrm{certifies}(c,d)\iff c=d$.
background
In the primitive recognition calculus, a completion is an interface from native data $N$ to display data $D$ together with a certificate type $\mathrm{Cert}$ and a relation $\mathrm{certifies}:\mathrm{Cert}\to D\to\mathrm{Prop}$. The point is to separate what is shown on the display from what can be finitely certified from native structure.
A display predicate is certificate-covered when every satisfying display datum carries such a certificate. Conservativity means the completion introduces no uncertified display artifacts: anything true on the display is already witnessed natively. The identity completion is the degenerate case in which native, display, and certificate types coincide, so the display map is the identity and certificates are just equality of data.
This sits in the CompletionConservativity module, which develops the base and product cases before the headline that a completion is conservative exactly when it has no artifacts.
proof idea
Definitional construction, not a proof. The structure fields are filled directly: display is the identity function on $N$, and certifies is propositional equality of certificate and display datum. No lemmas are applied; the body is a pure structure instance.
why it matters
This is the base case for certificate-preserving completions. The theorem identity_conservative shows that for every predicate $P$ on $N$, the identity completion is conservative for $P$: any display witness is its own certificate via reflexivity. That fact is packaged into the completion-conservativity headline, which states that conservativity is equivalent to absence of artifacts and that the identity completion is always conservative.
Hard-problem certificate audits reuse it as the default completion in an identity audit over a finite certificate type, with both legitimate and pathology predicates discharged by the same conservativity lemma. In the Recognition foundation stack this anchors the claim that completing native recognition data to a display cannot invent uncertified content when the completion is trivial (and, later, when it is a product of conservative pieces).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.