productCompletion
plain-language theorem explainer
Given two completion interfaces (native data to display data with certificates), their product is again a completion: display acts componentwise and a paired certificate certifies a paired display exactly when each factor certifies its component. Anyone assembling multi-field or multi-sector display objects cites this constructor. The body is a pure structure instance, pairing the two maps and conjoining the two certification predicates.
Claim. If $C_1$ is a completion from native type $N_1$ to display type $D_1$ with certificates $Cert_1$, and $C_2$ likewise from $N_2$ to $D_2$ with $Cert_2$, then there is a product completion from $N_1\times N_2$ to $D_1\times D_2$ with certificates $Cert_1\times Cert_2$, whose display map is $(n_1,n_2)\mapsto (C_1.\mathrm{display}(n_1), C_2.\mathrm{display}(n_2))$ and whose certification relation holds on a pair of certificates and a pair of displays precisely when each component certifies its own display.
background
In the Primitive Recognition Calculus, a completion interface packages the passage from native (finite, ledger-level) data $N$ to display data $D$, together with a certificate type $Cert$ and a relation $\mathrm{certifies}: Cert\to D\to\mathrm{Prop}$. The point is to keep display-level predicates accountable to native certificates rather than smuggling in continuum artifacts.
Conservativity for a completion $C$ and a display predicate $P$ means every display point satisfying $P$ carries a certificate under $C$. The product construction is the natural way to form multi-component displays (paired fields, joint sectors) while retaining that accountability.
The surrounding module develops identity and product completions and proves that conservativity is stable under both. Upstream, the same interface is used when Hilbert-display maps send $F_{RS}$ amplitudes to finite Hilbert vectors, so product completions sit between native recognition data and multi-factor display objects.
proof idea
Definitional structure instance, not a tactic proof. The product completion fills the two fields of Completion by pairing: display on a pair of natives is the pair of component displays; a pair of certificates certifies a pair of displays if and only if the first certificate certifies the first display and the second certifies the second. No lemmas are invoked; the instance is the pairing of the two given completions.
why it matters
This constructor is the algebraic backbone for multi-field certificate-preserving completion. Downstream, product_conservative shows that if each factor is conservative for its display predicate, the product completion is conservative for the product predicate; product_completion_headline packages that stability as the module headline ("multi-field display objects can be certified componentwise").
In the broader Delta-native strong-closure surface, product completions feed certificate assembly for joint carriers and multi-protocol displays (StrongClosureCertificate / strongClosureCertificate), so paired native data can be certified without inventing new continuum structure. Within the Recognition foundation this keeps the forcing-chain display layer (T-bridge and primitive distinction) closed under products: joint observables remain certificate-covered rather than introducing artifacts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.