product_conservative
plain-language theorem explainer
Conservative completions compose under products: if each factor's display predicate is certificate-covered, the product predicate is covered by paired certificates. Anyone certifying multi-field display objects componentwise cites this lemma. The proof unpacks the product hypothesis and re-pairs the two component certificates.
Claim. Let $C_1$ and $C_2$ be completions (native-to-display maps with certificate relations). If $C_1$ is conservative for a display predicate $P_1$ and $C_2$ is conservative for $P_2$, then the product completion is conservative for the product predicate $d\mapsto P_1(d_1)\land P_2(d_2)$: every product display satisfying both component predicates carries a paired certificate.
background
A completion is an interface from native data $N$ to display data $D$ together with a certificate type $\mathrm{Cert}$ and a relation $\mathrm{certifies}:\mathrm{Cert}\to D\to\mathrm{Prop}$. Conservativity for a predicate $P:D\to\mathrm{Prop}$ means $P$ is certificate-covered: every display datum satisfying $P$ admits some certificate. Equivalently, there are no uncertified display artifacts for $P$.
The product completion pairs two such interfaces componentwise on native, display, and certificate types. The product predicate is the pointwise conjunction $P_1(d_1)\land P_2(d_2)$ on $D_1\times D_2$. This module records that certificate-preserving completion is stable under that product construction.
The local setting is foundational bookkeeping for the primitive recognition calculus: display-level claims must descend to finite native certificates, so multi-field objects can be certified field by field without introducing non-native artifacts.
proof idea
Term-style unpacking of the product. Introduce a product display $d$ and the hypothesis that the product predicate holds, which splits as $P_1(d_1)$ and $P_2(d_2)$. Apply conservativity of $C_1$ at $d_1$ to obtain a certificate $c_1$, and conservativity of $C_2$ at $d_2$ to obtain $c_2$. Reassemble $(c_1,c_2)$ as a certificate for the product completion, using the component certification witnesses. No external lemmas beyond the definitions of product completion, product predicate, and conservativity.
why it matters
Feeds the in-module headline product_completion_headline, which packages the same stability statement as the public claim that certificate-preserving completion is stable under products, so multi-field display objects can be certified componentwise. Together with the identity-completion conservativity fact and the artifact characterization (conservative iff no uncertified display artifact), it closes the basic algebra of the completion interface.
In the Recognition foundation this is plumbing rather than a forcing-chain step: it ensures that when native recognition data are displayed as products (paired fields, multi-register readouts), conservativity does not leak. It does not itself force $\varphi$, the eight-tick octave, or $D=3$; it keeps display-level product structure honest relative to native certificates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.