deltaForced_sum
plain-language theorem explainer
If two types each carry a countable certificate (injection into the naturals), their disjoint union does too. Anyone working the primitive recognition calculus cites this to close δ-forced under binary choice of branches. The proof extracts countability from each hypothesis, then returns via the equivalence of δ-forced with countability, using the standard instance that sums of countable types are countable.
Claim. If $X$ and $Y$ are $\delta$-forced (each admits an injection into $\mathbb{N}$), then the disjoint union $X \oplus Y$ is $\delta$-forced.
background
In the primitive recognition calculus, a type is $\delta$-forced when it carries an explicit countable certificate: a nonempty type of injections $X \hookrightarrow \mathbb{N}$. That is the formal content of being finitely generated, hence enumerable, from the act of distinction. By the module's ontological reading, physically real is identified with $\delta$-forced; the mathematics lives entirely in the injection certificate.
Upstream, countable_of_deltaForced gives the choice-free direction: a $\delta$-forced type is countable. The converse equivalence deltaForced_iff_countable recovers a certificate from countability (using choice). The ambient Forced notion from maximal forcing is the broader claim-level language (a claim holds in every admissible realization); here the local predicate is the type-level $\delta$-forced certificate.
The sum type $X \oplus Y$ is the mathematical stand-in for a binary branch: an inhabitant is either a left $X$ or a right $Y$. Closing $\delta$-forced under that constructor says choosing between two forced branches remains forced.
proof idea
Term-mode proof in three beats. From hX : DeltaForced X apply countable_of_deltaForced to obtain Countable X; likewise for Y. Then apply the reverse direction of deltaForced_iff_countable at $X \oplus Y$, discharging the countability goal by inferInstance (Mathlib's instance that the sum of two countable types is countable). No custom encoding of the sum into $\mathbb{N}$ is written by hand.
why it matters
This is a closure lemma for the $\delta$-forced class under disjoint union. The doc-comment states the intended reading: choosing between two forced branches is forced. Together with the sibling facts that $\mathbb{N}$ and $\mathbb{Z}$ are $\delta$-forced (and the equivalence with countability), it keeps finite branching inside the physically-real demarcation line of the module.
No downstream consumers are wired yet (used_by is empty), so the lemma presently stockpiles structural hygiene for later forcing or recognition constructions that need binary case splits on certificates. It does not itself touch the T0–T8 forcing chain, the Recognition Composition Law, or the $\varphi$-ladder; it sits one layer below, at the type-theoretic substrate those later steps assume when they treat discrete alternatives as enumerable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.