deltaForced_prod
plain-language theorem explainer
The Cartesian product of two δ-forced types is again δ-forced: each factor carries an injection into ℕ, and so does the pair type. Anyone assembling product state spaces or joint certificates under the physical-reality demarcation would cite this. The proof reduces both hypotheses to countability, then invokes the equivalence δ-forced ↔ countable and Mathlib’s product instance.
Claim. If $X$ and $Y$ are $\delta$-forced (each admits an injection into $\mathbb{N}$), then the Cartesian product $X \times Y$ is $\delta$-forced.
background
In this module a type is δ-forced when it carries an explicit countable certificate: a nonempty type of injections $X \hookrightarrow \mathbb{N}$. That is the formal content of “finitely generated, hence enumerable, from the act of distinction.” By thesis, physically real coincides with δ-forced; the mathematical work sits entirely on the injection certificate.
Upstream, every δ-forced type is countable by projecting the certificate (choice-free). The converse equivalence δ-forced ↔ countable holds as well: the reverse direction extracts an injection into ℕ from countability and uses choice. The continuum is the standard non-example, since a certificate would force $\mathbb{R}$ countable.
The local setting is the primitive recognition calculus: which collections can arise as forced, enumerable distinctions. Closure under pairing is the product case of that calculus.
proof idea
From each hypothesis obtain countability via the choice-free projection lemma (certificate implies countable). Mathlib then supplies Countable (X × Y) by typeclass inference. Apply the reverse direction of the equivalence δ-forced ↔ countable to reinstall a product certificate. The whole argument is three lines: two haves and one exact ... mpr inferInstance.
why it matters
δ-forced is the formal stand-in for “physically real” in the recognition calculus: only collections with an explicit ℕ-certificate count. Closure under Cartesian product means joint configurations of two forced collections remain forced, so product state spaces and paired observables stay inside the demarcation line.
No downstream consumers are wired yet in the graph; the lemma sits with the sibling closures for ℕ, ℤ, and related countable constructions. It does not itself touch the forcing chain T5–T8 (J-uniqueness, φ, eight-tick, D = 3), but it underwrites the enumerability side of the foundation on which those later steps rest: if the factors are enumerable from distinction, so is the pair.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.