generated
plain-language theorem explainer
The generated collection is the finitary inductive closure of a seed set under a family of finite-arity rules: the union of all finite generative stages. Anyone proving countability, native-cost uniqueness, or character-generated gauge orbits cites this set as the ambient universe of reachable objects. The body is a one-line indexed union over the stage hierarchy.
Claim. Fix a type $\alpha$, a seed $S_0 \subseteq \alpha$, and a set $R$ of finite-arity maps $\mathrm{List}\,\alpha \to \alpha$. The generated collection is $\bigcup_{k \in \mathbb{N}} G_k$, where $G_0 = S_0$ and each $G_{k+1}$ adjoins every value $\rho(\ell)$ for $\rho \in R$ and finite lists $\ell$ with entries already in $G_k$.
background
In the Primitive Recognition Calculus native-cost uniqueness development, one builds objects by applying a fixed set of finite-arity rules to a seed. The stage hierarchy genStage encodes that process: stage $0$ is the seed $S_0$; stage $k+1$ is the previous stage union every rule image on lists drawn from that stage.
The generated collection packages the entire hierarchy as a single set: everything reachable in finitely many applications. No infinitary or limit-stage construction appears; reachability is strictly finitary.
This is pure set-theoretic scaffolding for later uniqueness and countability arguments about native costs and ratio characters. It does not itself encode the J-cost, the Recognition Composition Law, or any physical constant.
proof idea
Definition only: the body is the indexed union $\bigcup_k$ of the stage map. No tactics, no lemmas, no proof obligations beyond the type of genStage.
why it matters
This set is the ambient universe for finitary generation arguments across the monolith. Downstream uses include gauge-orbit classification (odd-power generated native costs versus the zero-exponent sign cost), cost comparisons from minimality, cosmic scale-affine witnesses, and algebraic weight lemmas that need a generated carrier.
In the Recognition framework it supports the uniqueness side of native cost structure that feeds T5-style J-uniqueness arguments and character-to-cost matching, without itself stating those theorems. The open corrected classification that every anchor-free structural inhabitant is either the sign cost or an odd-power generated cost relies on this generated universe as the place those families live.
With roughly forty use sites, it is infrastructure rather than a landmark theorem: parent results quote it whenever they quantify over objects reached by finite rule application.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.