generated_volume_zero
plain-language theorem explainer
Any set of reals generated from a countable seed by countably many finite-arity rules has Lebesgue measure zero. Measure theorists and RS foundation readers cite it as the measure form of non-forcing: finitary generative reach occupies none of the line. The proof is a one-line application of countable-nullness to the already-proved countability of the generated set.
Claim. If $S_0 \subseteq \mathbb{R}$ is countable and $R$ is a countable set of finite-arity real operations, then the set of all reals reachable from $S_0$ by finitely many applications of rules from $R$ has Lebesgue measure zero: $\lambda(\mathrm{Gen}(S_0,R)) = 0$.
background
In the Primitive Recognition Calculus native-cost uniqueness module, a finitary generative system on a type $\alpha$ consists of a seed set $S_0$ and a set $R$ of rules, each a map $\mathrm{List},\alpha \to \alpha$. The generated collection is the ascending union over stages: everything obtained from the seed by finitely many rule applications.
The upstream theorem thm:countgen states that if both the seed and the rule set are countable, then the generated collection is countable. That argument is completeness-free: countable unions, countable products of countable sets, and images suffice. On $\mathbb{R}$, Lebesgue volume is an atomless measure, so every countable set is null.
The local claim is the measure-theoretic form of non-forcing: finitary generative reach on the line occupies none of the continuum in the Lebesgue sense.
proof idea
One-line term proof. Apply Set.Countable.measure_zero to the already-established countability of the generated set (generated_countable hS0 hR) and to Lebesgue volume. No separate measure-theoretic work is done here; nullness is inherited from countability plus atomlessness of volume.
why it matters
This is cor:measure in the four non-forcing arguments of native-cost uniqueness: the reachable reals form a null set, so almost every real lies outside any finitary generative system. The immediate parent is generated_ae_unreachable, which rewrites the volume-zero statement into the almost-everywhere form ("a real drawn at random is unreachable"), called the sharpest size statement among those four arguments.
In the Recognition framework this blocks any attempt to force a native cost, or a continuum-many family of costs, by closing a countable seed under countable finitary rules. Continuum structure and the forced J-cost (T5 uniqueness via the Recognition Composition Law) must therefore enter by analytic or functional-equation means, not by generative enumeration. It also feeds the broader uniqueness narrative that later identifies the discrete $\delta$-act ladder with the calibration invariant $c^2$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.