uncountable_generated_needs_infinitary
plain-language theorem explainer
If a finitary generative system reaches an uncountable set, then either its seed or its rule family is already uncountable. Anyone arguing that distinction, read as finite-stage generation, cannot force the continuum without smuggling completeness would cite this. The proof is a one-step contrapositive of the countable-generation theorem.
Claim. Let $S_0 \subseteq \alpha$ be a seed and $R$ a family of finite-arity rules (maps $\mathrm{List}\,\alpha \to \alpha$). Write $G$ for the set of all elements reached from $S_0$ in finitely many applications of rules from $R$. If $G$ is uncountable, then either $S_0$ is uncountable or $R$ is uncountable.
background
The local setting is Primitive Recognition Calculus cost uniqueness: distinction is modeled as a finitary generative system, not as a completed continuum. A seed $S_0$ and a set $R$ of list-to-element rules produce stages by applying rules whose inputs already lie in the previous stage; the generated collection is the countable union of those stages.
Upstream, the companion result (thm:countgen) states that a countable seed closed under countably many finite-arity rules has countable reach. Its only inputs are countable unions, countable products of countable sets, and images; no completeness axiom is used. The present statement is exactly the logical contrapositive of that fact.
The paper's point is that any route from pure distinction to the continuum must therefore posit an uncountable seed or uncountably many simultaneous rules, i.e. an infinitary act already equivalent to completeness.
proof idea
Assume for contradiction that both the seed and the rule family are countable. The upstream countable-generation theorem then yields that the generated collection is countable, contradicting the hypothesis. The tactic block is: by_contra, push_neg, then apply generated_countable to the two countability hypotheses.
why it matters
This is the formal "escape is circular" lemma of the paper: the only way a generative reading of distinction reaches an uncountable set is by already assuming an infinitary input. Immediately downstream in the same module sits the real-line corollary that no countable seed under countably many finite-arity rules exhausts $\mathbb{R}$, so finitary distinction does not force the continuum.
In the broader Recognition Science forcing chain, continuum structure (and with it calibration invariants extracted from discrete act-cost ladders) cannot be smuggled in as a free generative consequence; it must be justified separately. The result is used in the native-cost uniqueness development that later identifies the $\delta$-act ladder coefficient with the calibration invariant $c^2$ (Move 1), keeping that extraction free of hidden completeness assumptions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.