ProductPredicate
plain-language theorem explainer
On a product of display types, the product predicate holds exactly when each component predicate holds on its factor. Anyone proving that certificate-preserving completions stay conservative under products cites this. The body is the pointwise conjunction of the two component predicates.
Claim. Given predicates $P_1:D_1\to\mathrm{Prop}$ and $P_2:D_2\to\mathrm{Prop}$, the product predicate on $D_1\times D_2$ is the map $(d_1,d_2)\mapsto P_1(d_1)\land P_2(d_2)$.
background
In the Primitive Recognition Calculus, a completion pairs a native object with a display type and a certificate type, and a predicate on the display is conservative when every display point satisfying the predicate is covered by some certificate. Multi-field or multi-sector displays are modeled as products of display types, so one needs a canonical way to lift component predicates to the product.
The surrounding module studies when completions remain conservative under standard constructions (identity, products). Upstream, display maps send $F_{RS}[i]$ amplitudes to finite Hilbert vectors, and bridge composition chains native-to-display maps that commute with the observable protocol. The product predicate is the pure logical ingredient those product theorems apply to the display side.
proof idea
Pure definition: the predicate on a pair is the conjunction of the first predicate on the first projection and the second predicate on the second projection. No lemmas or tactics.
why it matters
This is the display-side glue for product conservativity. The theorem product_conservative states that if each component completion is conservative for its predicate, then the product completion is conservative for the product predicate; the headline theorem packages the same fact as stability of certificate-preserving completion under products, so multi-field display objects can be certified componentwise. Without a named product predicate, those statements would have to inline the conjunction everywhere. In the Recognition foundation layer this keeps multi-sector Hilbert displays inside the same certificate discipline used for single-field displays, rather than inventing a separate product certificate calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.