product_completion_headline
plain-language theorem explainer
Certificate-preserving completion is stable under products: if each component completion is conservative for its display predicate, the product completion is conservative for the paired predicate. Multi-field display objects can therefore be certified componentwise. Anyone assembling multi-coordinate native-to-display maps cites this headline. The proof is a one-line application of the product conservativity lemma.
Claim. Let $C_1$ and $C_2$ be completion interfaces (maps from native data to display data equipped 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 of $C_1$ and $C_2$ is conservative for the product predicate $(d_1,d_2)\mapsto P_1(d_1)\wedge P_2(d_2)$.
background
A completion interface packages a display map from native data $N$ to display data $D$ together with a certificate relation on $D$. Conservativity for a display predicate $P$ means $P$ is certificate-covered: every display datum satisfying $P$ carries a finite native certificate. Equivalently, there is no non-native artifact (a display point in $P$ with no certificate).
The product completion pairs two such interfaces: native and display spaces become cartesian products, and a paired certificate certifies a paired display point exactly when each component certificate certifies its component. The product predicate is the pointwise conjunction of the two component predicates.
This module develops conservativity as the formal guarantee that display-level claims remain grounded in native certificates, so multi-field displays do not invent structure absent from the components.
proof idea
One-line term wrapper. It applies the already-proved product conservativity theorem to the two completions and the two predicates, discharging the headline statement directly. No extra case analysis or rewriting is required; the algebraic content lives in that upstream lemma (component certificates pair, and certificate-coveredness lifts across the product).
why it matters
In the primitive recognition calculus, physical displays are often multi-field (paired amplitudes, joint coordinates, product carriers). This headline states that certificate-preserving completion is stable under those products, so multi-field objects can be certified componentwise rather than by a bespoke joint argument.
Downstream it is consumed by the strong closure certificate in the Delta-native strong-closure module, which assembles a closed theorem surface from real-display, generable-carrier, analytic-protocol, and transformer entries. Product stability lets that certificate treat paired display structure without introducing non-native artifacts.
Within the broader foundation layer this is bookkeeping for native-to-display fidelity, not a forcing-chain step (T5–T8). It keeps multi-coordinate displays honest relative to the certificate interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.