generated_countable
plain-language theorem explainer
A finitary generative system with countable seed and countably many finite-arity rules has countable reach. Anyone arguing that distinction or native cost generation forces the continuum cites this barrier. The proof unfolds the generated set as a countable union of stages and applies the stagewise countability lemma. Completeness of the reals is never used.
Claim. Let $S_0 \subseteq \alpha$ be countable and let $R$ be a countable family of maps $\mathrm{List}\,\alpha \to \alpha$. Then the set of all elements obtained from $S_0$ by applying rules from $R$ through finitely many stages is countable.
background
In the Primitive Recognition Calculus, a generative system is specified by a seed set $S_0$ and a family $R$ of finite-arity rules (maps from lists into the ambient type). The $k$-th stage collects everything obtained by applying rules to lists drawn from earlier stages; the generated collection is the union over all finite stages.
The upstream stage lemma already shows each individual stage is countable when the seed and the rule set are: base stage is the seed; the successor stage is a countable union of images of countable list-sets under countable rule sets. The present result only lifts that stagewise fact to the full union.
The local setting is completeness-free native cost uniqueness: costs and distinctions are read as finitary generative acts. Doc-comment: "Completeness-free; the only inputs are countable unions, countable products of countable sets, and images."
proof idea
One-line wrapper after unfolding the definition. The generated collection is $\bigcup_k$ of the stages. Apply the standard countable-union lemma for sets to the family of stages, supplying the upstream result that every stage is countable under the same seed and rule hypotheses. All inductive work (base equals seed; successor closes under countable images of list-sets) lives in that stage lemma; nothing further is proved here.
why it matters
This is paper thm:countgen: finitary generation cannot manufacture an uncountable reach. It is the direct engine for three siblings in the same module. The contrapositive states that uncountable reach forces an uncountable seed or uncountably many rules ("the escape is circular": continuum reach smuggles in an infinitary act). The real-line corollary says no such system equals all of $\mathbb{R}$. The measure corollary says the reachable set has Lebesgue volume zero.
In the Recognition framework this blocks any claim that distinction, read as a finitary generative process, forces the continuum or a positive-measure set of reals. Native cost uniqueness in the module can therefore pin costs on discrete ladders without assuming continuum generation. It sits upstream of the completeness-free half of the cost-character story, separate from the forcing chain T5–T8 but aligned with the same finitary discipline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.