function_completion_headline
plain-language theorem explainer
Certificate-preserving completion is stable under pointwise function displays: if a completion is conservative for a display predicate, the induced function-space completion is conservative for the pointwise lift of that predicate. Anyone certifying finite vectors or finite fields coordinatewise would cite this. The proof is a one-line application of the underlying function-conservativity lemma.
Claim. If a completion $C$ from native data to display data is conservative for a predicate $P$ on displays, then the induced function-space completion (completing each coordinate through $C$) is conservative for the pointwise predicate $\forall i,\, P(d_i)$ on functions into the display type.
background
In the Primitive Recognition Calculus, a completion is an interface mapping native data $N$ to display data $D$, together with certificates for display predicates. Conservativity means the predicate is certificate-covered: every display datum satisfying it carries a finite/native certificate, so there are no non-native artifacts.
Function-space completion builds a new interface on $I\to N$ and $I\to D$ by applying the base completion coordinatewise; certificates are themselves maps $I\to\mathrm{Cert}$. The pointwise predicate requires $P$ at every index. This is the finite-vector / finite-field display pattern: structured displays are certified without inventing new certificate machinery beyond the base interface.
proof idea
One-line term proof that applies the already-proved function-conservativity lemma for the same completion and predicate. That lemma shows that if each coordinate predicate is certificate-covered, the whole function display has a coordinatewise certificate, which is exactly conservativity of the function completion against the pointwise predicate.
why it matters
This is a headline conservativity result in the completion module, parallel to the identity and product headlines. It is consumed by the strong closure certificate in Delta-native strong closure, which assembles the closed Delta-native theorem surface (real forgetful display, generable carriers, certified analytic protocols and transformers). Coordinatewise certification of finite displays keeps the native-to-display bridge free of artifacts, so the display layer of the Recognition forcing chain stays conservative when finite vectors or fields appear.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.