genStage_countable
plain-language theorem explainer
Each finite stage of a finitary generative system is countable whenever the seed set and the rule set are countable. Anyone proving that the full generated collection is countable cites this stagewise fact first. The argument is induction on the stage index, closing under countable unions and images of countable list-sets.
Claim. Let $S_0\subseteq\alpha$ be a countable seed and let $R$ be a countable family of finite-arity rules $\mathrm{List}\,\alpha\to\alpha$. Write $G_0=S_0$ and $G_{k+1}=G_k\cup\{\rho(\ell):\rho\in R,\;\ell\text{ has all entries in }G_k\}$. Then $G_k$ is countable for every $k\in\mathbb{N}$.
background
In this module a finitary generative system is a seed set $S_0$ together with a set $R$ of rules, each a map from finite lists in $\alpha$ to an element of $\alpha$. Stage $0$ is the seed; stage $k+1$ adjoins every value obtained by applying a rule to a finite tuple already reached at stage $k$. The generated collection is the countable union of all stages.
The local goal is a completeness-free countability calculus: only countable unions, countable products of countable sets, and images are used. An upstream lemma records that the set of all lists whose entries lie in a fixed countable set is itself countable; that fact supplies the list-space input at each successor stage.
proof idea
Fix the seed and rule countability hypotheses and induct on the stage index $k$. The base case is immediate: stage $0$ is the seed.
At a successor, the stage is the previous stage union the set of all rule applications to lists from the previous stage. The inductive hypothesis makes the previous stage countable. The list-set lemma then makes the set of admissible lists countable. Rewrite the adjoined set as a big union, over rules in $R$, of images of that list-set under each rule; countability of $R$ and preservation of countability under images and countable unions finish the step.
why it matters
This is the stagewise half of thm:countgen. The immediate parent is the theorem that the full generated collection is countable, obtained by taking the countable union over stages of the present result. That parent is the completeness-free countability engine used in the native-cost uniqueness development: once seeds and finitary rules are countable, everything they generate remains countable, so continuum-sized pathologies cannot appear from finitary generation alone.
In the broader Recognition foundation this supports the claim that escaping countability requires a genuinely infinitary input, keeping the primitive recognition calculus on a countable, rule-generated substrate rather than an uncountable continuum of ad hoc costs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.