generated_ae_unreachable
plain-language theorem explainer
Lebesgue-almost every real lies outside the set generated from any countable seed set by any countable family of real-valued list operations. Anyone arguing that finitary generative closure cannot force a unique continuous cost cites this null-set bound. The proof is a one-line rewrite of almost-everywhere into measure-zero, then applies the companion volume-zero lemma.
Claim. Let $S_0\subseteq\mathbb{R}$ be countable and let $R$ be a countable set of maps $\mathrm{List}\,\mathbb{R}\to\mathbb{R}$. Then for Lebesgue-almost every $x\in\mathbb{R}$, $x$ does not lie in the set generated from $S_0$ by iterated application of the operations in $R$.
background
In the Primitive Recognition Calculus cost-uniqueness development, one family of arguments shows that no finitary generative process on the reals can pin down a continuous cost by pure closure. A generative system here is a countable seed $S_0\subseteq\mathbb{R}$ together with a countable repertoire $R$ of operations $\mathrm{List},\mathbb{R}\to\mathbb{R}$; the generated set is the smallest set containing $S_0$ and closed under those operations.
The module's non-forcing cluster treats four size notions for that generated set. The present statement is the measure-theoretic one: under Lebesgue measure on $\mathbb{R}$, the generated set is null, so a randomly drawn real is almost surely unreachable. The companion fact is that the generated set has Lebesgue measure zero whenever both the seed and the operation family are countable.
Locally this sits beside the monotone d'Alembert forcing for the native recognition cost $J(x)=(x+x^{-1})/2-1$ (equivalently $H=J+1$ satisfying the standard d'Alembert equation). The generative null-set bound is independent of that forcing; it only limits what pure generation can achieve.
proof idea
One-line wrapper. Rewrite the almost-everywhere claim via MeasureTheory.ae_iff (a property holds a.e. iff the set of failures has measure zero). The failure set is exactly the generated set, so the goal becomes measure-zero of that set. Discharge by simpa from the companion lemma generated_volume_zero at the same countable hypotheses on the seed and the operation family.
why it matters
Among the four non-forcing size arguments in native cost uniqueness, this is the sharpest: not merely countable or meager, but Lebesgue-null, so the complement is conull. It blocks any claim that a continuous cost on $\mathbb{R}_{>0}$ is forced by closing a countable seed under a countable operation list alone.
Downstream it feeds costLambda_successor_increment_tendsto, which shows that the discrete $\delta$-act ladder recovers exactly the calibration invariant $c^2$ for every member of the forced scale family (n^2\cdot\mathrm{costLambda}\,c((n+1)/n)\to c^2/2). That parent theorem needs the generative side-channel ruled out so the ladder reading is not contaminated by unreachable reals manufactured outside the forced family.
In the broader Recognition chain this protects the T5 J-uniqueness story: the cost is forced by the composition law and monotonicity (log-coordinate transform is $\cosh$), not by generative enumeration of values. No scaffolding remains; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.