function_conservative
plain-language theorem explainer
Certificate-covered display predicates remain certificate-covered after lifting the completion to function spaces: if every coordinate of a display function satisfies P and carries a certificate, the whole function is certified by a coordinatewise certificate family. Anyone proving finite-vector or finite-field displays in the primitive recognition calculus cites this. The proof is a short choice argument that packages pointwise certificates.
Claim. Let $C$ be a completion from native data $N$ to display data $D$ with certificates $Cert$, and let $P:D\to\mathrm{Prop}$. If $C$ is conservative for $P$ (every display satisfying $P$ carries a certificate), then the function-space completion of $C$ is conservative for the pointwise predicate $\mathrm{All}(P)$ on $I\to D$: whenever $d:I\to D$ satisfies $P(d(i))$ for all $i$, there is a certificate family witnessing that fact.
background
In the primitive recognition calculus, a completion is an interface that maps native data $N$ to display data $D$ and supplies certificates $Cert$ for display predicates. Conservativity for a predicate $P$ means $P$ is certificate-covered: every display datum satisfying $P$ comes with a finite/native certificate, so no non-native artifact can satisfy $P$.
The pointwise lift $\mathrm{All}(P)$ on functions $I\to D$ holds exactly when every coordinate satisfies $P$. The function-space completion extends $C$ so that displays and certificates act coordinatewise on such functions. This module studies when conservativity is stable under identity, product, and function constructions, ensuring that completing native structure cannot invent new certified displays.
Upstream, spatial dimension $D=3$ is forced in the forcing chain (T8/T9), but this lemma is purely about the certificate interface and does not depend on that value.
proof idea
Assume the base completion is conservative for $P$, and take a function display $d:I\to D$ that satisfies $\mathrm{All}(P)$, i.e. $P(d(i))$ for every index $i$. Apply conservativity at each coordinate to obtain a certificate $c(i)$ for $d(i)$. Package the family $c$ as a single certificate for the function display under the function-space completion. The argument is a direct intro/choose/exact packaging with no further lemmas.
why it matters
This is the function-space half of completion conservativity: certificate-preserving completion stays conservative under pointwise finite/function displays. The immediate parent is function_completion_headline, which restates the implication as the module headline that finite vectors and finite fields can be certified coordinatewise.
In Recognition Science foundation work, native structure is completed to richer displays only if no new certified content appears. Stability under function displays lets multi-component objects (coordinate tuples, finite fields of values) inherit certificates from their parts, which is required before linking displays to the eight-tick octave and $D=3$ geometry without smuggling artifacts. Together with the product and identity conservativity siblings, it closes the basic algebraic closure properties of the completion interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.