countable_of_deltaForced
plain-language theorem explainer
Any δ-forced type is countable: the certificate is an injection into ℕ, so the type injects into a countable set. Physicists and set-theorists working the Primitive Recognition Calculus cite this to pass from ontological “forced by distinction” to ordinary countability. The proof unpacks the nonempty embedding and applies the standard injective-into-ℕ countability lemma; it is choice-free.
Claim. If a type $X$ is $\delta$-forced (i.e., there exists an injection $X \hookrightarrow \mathbb{N}$), then $X$ is countable. The argument uses only the certificate embedding and does not invoke the axiom of choice.
background
In the Primitive Recognition Calculus, a type is called $\delta$-forced when it carries an explicit countable certificate: a nonempty injection into $\mathbb{N}$. The module glosses this as the formal content of being “finitely generated, hence enumerable, from the act of distinction.” The companion notion PhysicallyReal is identified with $\delta$-forced by thesis; the mathematical content lives entirely in the injection certificate.
Countability here is Mathlib’s Countable: existence of an injection into $\mathbb{N}$ (or an equivalent enumeration). The forward direction from certificate to countability needs no choice; the converse, developed later in the same module, extracts a certificate from countability and does use choice.
Local setting is the Foundation layer that demarcates which types can appear as physically real collections under Recognition Science. Upstream scaffolding includes the cost-projector and gap-derivation constants, but this lemma itself is pure type theory.
proof idea
One-step unpacking. From h : DeltaForced X, which is Nonempty (X ↪ ℕ), obtain a concrete embedding e : X ↪ ℕ. Then e.injective.countable (Mathlib: an injective map into a countable type yields countability of the domain) finishes the proof. No induction, no classical choice, no further Recognition lemmas.
why it matters
This is the bridge from the ontological certificate to ordinary set-theoretic countability. Downstream it is the forward half of deltaForced_iff_countable ($\delta$-forced $\leftrightarrow$ countable), and it is the workhorse that closes the product, subtype, and sum closure theorems: each reduces $\delta$-forcedness of a compound type to countability of the factors via this lemma, then re-enters through the iff. It also powers not_deltaForced_real: a $\delta$-forced certificate on $\mathbb{R}$ would force Countable ℝ, contradicting $\mathfrak{c} > \aleph_0$.
In the Recognition framework the lemma enforces the demarcation line: only enumerable collections (those generable by successive distinction) can be physically real. Continuum-sized state spaces are thereby excluded as primitive carriers. It does not itself touch the forcing chain T0–T8 or the J-cost uniqueness, but it underwrites the later claim that physical spectra live on countable $\varphi$-ladders rather than on continuum parameter spaces.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.