conservative_completion_transfers
plain-language theorem explainer
If a completion from native data to continuum display data is conservative for a display predicate P, every continuum witness of P carries a finite certificate. Anyone citing the finite-certificate transfer headline needs this half of the conjunction. The proof is a one-line unfolding of the conservativity hypothesis.
Claim. Let $C$ be a completion from native data $N$ to display data $D$ with certificate type $\mathrm{Cert}$. If $C$ is conservative for a display predicate $P:D\to\mathrm{Prop}$, then for every $d\in D$ with $P(d)$ there exists a certificate $c\in\mathrm{Cert}$ such that $C$ certifies $c$ for $d$.
background
In the primitive recognition calculus, continuum statements are not taken as primitive. A completion $C$ packages a display map from native data $N$ into continuum display data $D$, together with a certification relation $\mathrm{certifies}:\mathrm{Cert}\to D\to\mathrm{Prop}$. Certificates are the finite/native witnesses that justify continuum claims.
Conservativity for a predicate $P$ means $P$ is certificate-covered: every display datum satisfying $P$ already carries some certificate under $C$. Equivalently, there are no non-native artifacts for $P$ (display points that satisfy $P$ yet have no certificate). The module sits in the Foundation layer that separates native recognition structure from continuum packaging.
This lemma simply reifies that definition as an explicit universal quantifier over display witnesses, ready for conjunction with the dual obstruction transfer.
proof idea
One-line term proof: the goal is definitionally identical to $\mathrm{ConservativeFor},C,P$, which is an alias of certificate-coveredness. The hypothesis $hC$ is therefore the goal, and the proof is just $hC$. No lemmas are applied.
why it matters
This is the positive half of the finite-certificate transfer headline. Downstream, finite_certificate_transfer packages it with the dual obstruction descent:
For a conservative completion, valid continuum witnesses and valid continuum obstructions both descend to finite certificates. This is the formal hinge behind the quantized-proof method.
In Recognition Science, continuum claims (mass ladders, gap statements, dimensional forcing) must ultimately rest on finite native certificates rather than free continuum existence. Conservativity is the interface condition that makes that descent legitimate. The result does not itself force $D=3$ or the eight-tick octave; it supplies the transfer rule those later certificates rely on when continuum packaging is used.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.