no_enumeration_seq
plain-language theorem explainer
There is no surjection from the naturals onto the space of binary sequences ℕ → Bool. Anyone arguing that a δ-enumerable (forced) carrier cannot cover the continuum cites this. The proof is the constructive diagonal argument: assume a listing, flip the diagonal bit, and derive a contradiction by evaluation at the putative index.
Claim. There does not exist a function $f : \mathbb{N} \to (\mathbb{N} \to \mathrm{Bool})$ that is surjective. Equivalently, the set of binary sequences cannot be enumerated by a sequence of sequences.
background
In the Primitive Recognition Calculus grow layer, a carrier is called δ-enumerable (forced) when it admits a countable listing that exhausts every element. The continuum candidate here is the function space of binary sequences $\mathbb{N} \to \mathrm{Bool}$, the constructive stand-in for $2^{\mathbb{N}}$.
Cantor's classical non-enumerability of the power set of $\mathbb{N}$ is restated without choice: no map from $\mathbb{N}$ can hit every binary sequence. The module isolates this fact as the choice-free core of the claim that the reals are not forced.
The only import is basic logic from Mathlib; no Recognition-specific cost functional or ladder structure is required at this step.
proof idea
Assume for contradiction a surjection $f : \mathbb{N} \to (\mathbb{N} \to \mathrm{Bool})$. Form the diagonal flip $d(k) := \neg f(k)(k)$. Surjectivity supplies some $n$ with $f(n) = d$. Evaluating both sides at $n$ yields $f(n)(n) = \neg f(n)(n)$, which simplifies to false. The argument is pure diagonalization; no classical choice or excluded-middle beyond Boolean negation is used.
why it matters
This lemma is the constructive heart of $\neg\mathrm{DeltaForced},\mathbb{R}$: a forced carrier cannot surject onto binary sequences, so the continuum is not forced by a δ-enumeration. In the Recognition Science foundation, forced structure is what the forcing chain (T0–T8) and the Recognition Composition Law may pin down; unforced continuum degrees of freedom stay outside that pin-down. The result therefore marks a hard boundary between what the framework can force (discrete octave structure, $D=3$, $\varphi$-ladder rungs) and what it cannot (a countable listing of all binary sequences). No downstream edges are recorded in this module, but the doc-comment positions it as the choice-free core of the non-forcing claim for $\mathbb{R}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.