Completion
plain-language theorem explainer
Defines a completion interface: a map from native data to display data together with a certificate relation on displays. Anyone proving conservativity (no uncertified display artifacts) cites this carrier type. It is a bare structure with two fields and no proof obligations.
Claim. A completion from native type $N$ to display type $D$ with certificate type $\mathrm{Cert}$ consists of a display map $N \to D$ and a certification relation $\mathrm{Cert} \times D \to \mathrm{Prop}$.
background
In the Primitive Recognition Calculus, native objects (amplitudes, finite certificates, rung data) are often shown through a display layer: finite Hilbert vectors, function spaces, or product coordinates. The display may look continuous or infinite even when the native source is finite.
This module isolates that pattern as an interface. Native data $N$ is sent to display data $D$ by a map display. A separate certificate type $\mathrm{Cert}$ and relation certifies record which display points are still justified by a finite/native witness. Upstream Hilbert display work already uses this pattern (display an $F_{RS}[i]$ amplitude as a finite Hilbert vector).
Conservativity is the demand that predicates on $D$ not invent points outside the certified image. The structure itself only packages the two maps; the predicates CertificateCovered, ConservativeFor, and ArtifactFor are defined on top of it.
proof idea
No proof. The declaration is a structure with two fields: a display function $N \to D$ and a binary predicate $\mathrm{Cert} \to D \to \mathrm{Prop}$. Instantiations (identity completion, product completion, function-space completion) fill those fields later.
why it matters
This is the carrier type for the whole CompletionConservativity development. Downstream, CertificateCovered says every display point in a predicate $P$ has a certificate; ArtifactFor is the dual (a point in $P$ with no certificate); ConservativeFor is defined as certificate coverage. The headline theorem states that conservativity is exactly absence of artifacts, and that the identity completion is conservative for every predicate on native data.
In Recognition Science terms, the interface polices the native-to-display step used when amplitudes, mass-ladder data, or finite certificates are rendered for analysis. It does not itself force $D=3$, $\varphi$, or the eight-tick octave; those enter only when concrete completions (Hilbert display, fermion DOF bridges) are plugged in. Its role is local hygiene: display layers must not smuggle uncertified structure into claims about the native calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.