functionCompletion
plain-language theorem explainer
Pointwise function-space completion lifts a native-to-display completion along an index type, so multi-component objects (finite vectors, finite fields) inherit certificates coordinatewise. Anyone certifying I-indexed displays cites this construction before proving conservativity lift. The definition fills the completion structure by applying the base display at each index and requiring certification at every coordinate.
Claim. Given a completion interface from native data $N$ to display data $D$ with certificates $C$, and an index type $I$, there is an induced completion from $I\to N$ to $I\to D$ with certificates $I\to C$: display sends $n$ to $i\mapsto$ (base display of $n(i)$), and a pair $(c,d)$ is certified exactly when every coordinate $i$ is certified by the base interface.
background
The module develops completion conservativity for the primitive recognition calculus. A completion interface packages a display map from native data $N$ to display data $D$ together with a certification relation from certificates to display values. A display predicate is certificate-covered when every satisfying display carries a finite or native certificate; conservativity means the completion preserves that covering (equivalently, produces no uncertified artifacts).
Function-space completion is the finite-vector / finite-field pattern named in the doc-comment: once a single-component completion is fixed, objects indexed by $I$ are completed coordinatewise through the same interface. Sibling constructions include the identity completion and the product completion, which handle the trivial and paired cases respectively.
Upstream dimension constants ($D=3$ from T8) appear among graph edges but are not parameters here; the index type remains free.
proof idea
Definitional construction, not a proved theorem. The display field is the pointwise application of the base display map. The certification field is universal quantification of the base certification predicate over the index type. No lemmas are applied; both structure fields are filled by lambda terms.
why it matters
Direct input to the pointwise conservativity lift: if the base completion is conservative for a predicate $P$, the function-space completion is conservative for the pointwise ("all coordinates") predicate. That fact is restated as the function-space completion headline: certificate-preserving completion is stable under pointwise finite or function displays, so finite vectors and finite fields can be certified coordinatewise.
Also consumed when assembling the Delta-native strong closure certificate, whose fields point at closed theorem heads on the recognition calculus surface. In the broader framework this keeps multi-component displays (amplitudes, fields, rung data) inside the same certificate discipline as the scalar case, without new ad hoc certificate logic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.