countable_setOf_lists_mem
plain-language theorem explainer
Any countable ground set yields only countably many finite lists with entries in that set. Generative-stage and native-cost arguments in the Primitive Recognition Calculus cite this to keep each finitary stage countable. The proof injects the constrained lists into ordinary lists over the countable subtype and inherits countability.
Claim. If $s \subseteq \alpha$ is a countable set, then the set of all finite lists $\ell$ with values in $\alpha$ such that every entry of $\ell$ lies in $s$ is countable.
background
This lemma sits in the Primitive Recognition Calculus native-cost uniqueness module, which develops finitary generative stages and the discrete $\delta$-act cost ladder used to pin calibration invariants.
Countability here is Mathlib's Set.Countable: a set admits an injection into the naturals (equivalently, its subtype is a countable type). Lists are ordinary finite sequences; the constrained collection is ${\ell : \mathrm{List},\alpha \mid \forall y\in\ell,, y\in s}$.
The immediate consumer is the stage-countability theorem for a finitary generative system: starting from a countable seed and a countable rule set, each inductive stage remains countable. That stage fact feeds later uniqueness and ladder arguments for native cost.
proof idea
Pass from set-countability of $s$ to type-countability of the subtype. Rewrite the goal as countability of the corresponding subtype of lists via Set.countable_coe_iff.
Build the map sending a constrained list $L$ to the list of subtype elements obtained by attaching membership proofs (List.attach then mapping into $s$). A short simp identity shows that mapping those subtype values back recovers $L$.
Injectivity follows: equal images, after applying List.map Subtype.val and the recovery identity, give equal underlying lists, hence equal subtypes. An injective image of a countable type (lists over countable $s$) is countable, so the constrained set is countable.
why it matters
In the Recognition framework this is bookkeeping infrastructure, not a physics axiom: it licenses inductive countability of generative stages (genStage_countable, tagged thm:countgen). Without it, finitary closure under countable rule sets could escape to uncountable carrier sets and break discrete enumeration of cost stages.
That stage-countability supports the native-cost uniqueness development, including the $\delta$-act ladder limit that recovers the calibration invariant $c^2$ (costLambda_successor_increment_tendsto). The ladder statement is the discrete Move-1 claim that act-cost increments see $c^2$ and nothing more.
Relative to the forcing chain, this is pre-physics set theory under PRC cost uniqueness; it does not itself force $J$, $\varphi$, the eight-tick octave, or $D=3$, but keeps the generative scaffolding countable so those uniqueness arguments stay on discrete stages.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.