deltaForced_iff_countable
plain-language theorem explainer
δ-forced is equivalent to countable: a type admits an injection into ℕ if and only if it is countable. Foundation work on the physical-reality demarcation cites this bridge. Forward direction is the choice-free certificate lemma; reverse pulls an injective map from Mathlib countability and packages it as a δ-forced witness.
Claim. For any type $X$, $X$ is $\delta$-forced (i.e., there exists an injection $X \hookrightarrow \mathbb{N}$) if and only if $X$ is countable. The forward implication is choice-free; the reverse extracts an injective certificate from countability and may use choice.
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}$. The doc-comment frames this as the formal content of being "finitely generated, hence enumerable, from the act of distinction." Ontologically, physically real is identified with $\delta$-forced; the mathematics sits entirely in the injection certificate.
Mathlib countability is the standard notion (existence of an injection into $\mathbb{N}$, up to the usual choice packaging). The sibling lemma countable_of_deltaForced already shows every $\delta$-forced type is countable, choice-free, by unpacking the certificate and applying injectivity. This theorem closes the biconditional so that type-formers with known countability instances can be re-certified as $\delta$-forced.
proof idea
Term-mode constructor on the iff. Left-to-right is exactly countable_of_deltaForced. Right-to-left: from Countable X, obtain an injective $f : X \to \mathbb{N}$ via exists_injective_nat', then package $\langle f, hf \rangle$ as a nonempty embedding witness for DeltaForced X.
why it matters
This is the workhorse bridge used by the closure lemmas for products, subtypes, and sums: deltaForced_prod, deltaForced_subtype, and deltaForced_sum each reduce to Mathlib countability instances and re-enter via the reverse direction of this iff. Without it, every type-former would need a hand-built pairing or coding injection.
In the Recognition framework the $\delta$-forced line is the proposed demarcation of physical reality (enumerable from distinction). Equivalence with countability pins that line to a standard set-theoretic notion, so continuum-sized objects (e.g. $\mathbb{R}$) are excluded once and for all, while finite and countable constructions stay inside. It supports the foundation layer beneath the forcing chain rather than a numbered T-step itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.