genStage
plain-language theorem explainer
Recursive stages of a finitary generative system: start from a seed set S0 and, at each successor stage, close under a countable family of finite-arity rules. Anyone proving countability of generated objects or building the native-cost uniqueness ladder cites this. The body is a plain recursive definition on ℕ, not a theorem.
Claim. Fix a type $\alpha$, a seed set $S_0 \subseteq \alpha$, and a set $R$ of rules, each a map $\mathrm{List}\,\alpha \to \alpha$. Define stages $G_k$ by $G_0 = S_0$ and $G_{k+1} = G_k \cup \{ \rho(\ell) \mid \rho \in R,\; \ell \in \mathrm{List}\,\alpha,\; \mathrm{range}(\ell) \subseteq G_k \}$.
background
In the Primitive Recognition Calculus native-cost uniqueness module, one must show that certain cost-related constructions remain countable when generated from countable data by finitary operations. A finitary generative system consists of a seed set $S_0$ and a rule set $R$, where each rule is a finite-arity operation packaged as a function on lists.
Stage $0$ is just the seed. Each later stage adjoins every value obtained by applying some rule in $R$ to a finite list whose entries already lie in the previous stage. The generated collection (the union over all stages) is defined immediately from this recursion and is the object whose countability is needed downstream.
The surrounding development ties this combinatorics to the $\delta$-act cost ladder and the forced scale family for the native cost, where countability of generated stages underpins measure and uniqueness arguments.
proof idea
Pure recursive definition on $\mathbb{N}$. Base case returns the seed $S_0$. Successor case takes the previous stage and unions it with the set of all rule applications $\rho(\ell)$ where $\rho \in R$ and every entry of the list $\ell$ already belongs to the previous stage. No lemmas are invoked; the equation is the definition.
why it matters
This is the stagewise engine behind the generated collection $\bigcup_k G_k$, which is the ambient set for countability results such as thm:countgen (each stage of a finitary generative system is countable). Downstream, genStage_countable inducts on this recursion, and the generated union feeds the native-cost uniqueness story, including the $\delta$-act ladder result that the discrete cost determines the calibration invariant $c^2$ and nothing more.
In Recognition Science terms, finitary generation is the combinatorial skeleton that keeps the native cost and character-trace constructions inside a countable, effectively presentable universe before analytic uniqueness (J-cost / RCL scale family) is applied. Without staged generation, the countability half of the uniqueness pipeline has no inductive handle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.