ConservativeFor
plain-language theorem explainer
Conservativity of a completion for a predicate means every display datum satisfying that predicate carries a native certificate. It is the named interface used throughout the completion-conservativity layer: identity, product, and function completions all state their guarantees in this language. The definition is a one-line alias of certificate coverage.
Claim. Given a completion $C$ from native data $N$ to display data $D$ with certificate type $\mathrm{Cert}$, and a predicate $P$ on $D$, $C$ is conservative for $P$ when every $d \in D$ with $P(d)$ admits some certificate $c$ such that $C$ certifies $c$ at $d$.
background
In the primitive recognition calculus, a completion is an interface that maps native data $N$ into display data $D$ and supplies a relation $\mathrm{certifies} : \mathrm{Cert} \to D \to \mathrm{Prop}$. Display objects are the Hilbert-style or multi-field presentations used downstream; certificates are the finite native witnesses that those presentations are not free-floating artifacts.
Certificate coverage says: whenever a display datum satisfies a chosen predicate $P$, some certificate exists for it. Conservativity is that same property under a shorter name, so later theorems can speak of "conservative completions" without repeating the quantifiers.
The surrounding module develops identity, product, and function-space completions and proves they preserve this property. Spatial dimension $D=3$ and related gap constants appear only as ambient RS parameters elsewhere in the import graph; they are not parameters of this definition.
proof idea
Definitional abbreviation only: the body is exactly certificate coverage of $P$ under $C$. No tactics, no lemmas. Unfolding later theorems (for example the equivalence with absence of artifacts) expands this alias and works with the $\forall d,, P(d)\to \exists c,, C.\mathrm{certifies}, c, d$ form.
why it matters
This is the central predicate of the completion-conservativity layer. The headline theorem states that a completion is conservative for every predicate if and only if it has no uncertified display artifacts, and that the identity completion is always conservative. Product and function-space headlines lift conservativity componentwise and pointwise, so multi-field and finite-vector displays stay certificate-preserving.
Downstream, strong-closure certificates in the delta-native layer consume the same notion. In Recognition Science terms, the point is methodological: display completions (Hilbert amplitudes, products of fields) must not invent physics that the native ledger cannot certify. Conservativity is the formal non-invention condition those constructions must meet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.