finite_certificate_transfer
plain-language theorem explainer
For a conservative completion from native data to continuum display data, every legitimate continuum witness and every continuum obstruction carries a finite certificate. Anyone citing the quantized-proof method or Delta-native strong closure needs this hinge. The proof is a one-line pairing of the two one-sided transfer lemmas (witness side and obstruction side).
Claim. Let $C$ be a completion from native data $N$ to display data $D$ with certificate type $\mathrm{Cert}$. If predicates $P$ and $O$ on $D$ are both conservative for $C$, then $\forall d\in D$, $P(d)$ implies some certificate certifies $d$, and $\forall d\in D$, $O(d)$ implies some certificate certifies $d$.
background
The module sits in the Primitive Recognition Calculus layer: continuum display statements are only admissible when they reduce to finite native certificates. A completion $C$ packages a display map from native data $N$ into continuum data $D$ together with a certification relation $\mathrm{certifies}:\mathrm{Cert}\to D\to\mathrm{Prop}$.
Conservativity of a display predicate $Q$ for $C$ means continuum truth of $Q$ is controlled by the certificate interface (no continuum-only residue). The sibling one-sided lemmas already record that, under conservativity, witnesses of a legitimate predicate transfer to certificates, and that obstructions likewise descend.
Upstream, Completion is exactly that native-to-display interface with certificates for display predicates. The present theorem is the two-sided headline that packages both directions for the quantized-proof audit.
proof idea
Term-mode pairing, not a tactic script. The goal is a conjunction. The left conjunct is exactly the conclusion of conservative_completion_transfers applied to $C$, $P$, and the conservativity hypothesis on $P$. The right conjunct is exactly the conclusion of obstruction_descends applied to $C$, the obstruction predicate, and its conservativity hypothesis. The proof is the pair constructor assembling those two applications; no further rewriting or case analysis.
why it matters
Doc-comment names this the formal hinge behind the quantized-proof method: continuum legitimacy and continuum pathology both collapse to finite certificates once the completion is conservative. Downstream, problemAudit_finiteReduction is a direct application, feeding a problem audit's legitimate and pathology predicates through this theorem to obtain HasFiniteReduction. The same transfer surface is assembled into strongClosureCertificate on the Delta-native strong-closure side.
In the broader Recognition stack this is bookkeeping for finite reduction of continuum claims, not a forcing-chain step (T5–T8). It underwrites the claim that continuum display layers cannot smuggle uncertified content past a conservative completion, which is the honesty condition the module's next section strengthens to sound-and-faithful covers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.