values_countable
plain-language theorem explainer
For any rich certified-analytic registry, the set of real display values obtained by evaluating finite expressions is countable. Analysts cite this to show that adding unary and binary protocol transformers still cannot smuggle a continuum of constants. The proof is a one-line wrapper: the value map has countable domain, so its range is countable.
Claim. Let $R$ be a rich registry (countably many constant protocols, unary protocol transformers, and binary protocol transformers). The set of real numbers obtained by evaluating finite expressions over $R$ is a countable subset of $\mathbb{R}$.
background
In the certified analytic layer, a registry packages countably many protocols and transformers; expressions are finite trees over those labels. Evaluation yields a Delta-real protocol, and value displays that protocol as a real. The set of all such displays is the range of the evaluation map.
A RichRegistry extends the plain registry by also indexing unary and binary protocol transformers. Finite expressions over it (RichExpr) still form a countable inductive type: natural-number labels plus finitely many constructors. The companion plain-registry fact already records that "registry values are countable because expressions are finite trees over countable labels. This is the countability fact that blocks continuum smuggling."
The local module lifts that discipline to the richer signature so that transformer closure theorems can quote a single countability lemma.
proof idea
One-line wrapper. By definition the value set is the range of the evaluation map from rich expressions to reals. Mathlib's Set.countable_range then yields countability of that range, using that the domain of finite rich expressions is countable. Identical shape to the plain-registry values_countable.
why it matters
This is the countability half of rich certified-analytic closure. It is consumed by rich_transformer_closure (countable values plus protocol witnesses and rational/additive laws) and by the headline theorem certified_transformer_headline, which states that "adding binary transformers and finite compositions of unary transformers does not re-import the continuum: generated values remain countable and protocol-witnessed."
It also parallels the plain-registry lemma feeding transcendental_protocol_closure, whose slogan is that "the continuum is not the carrier of analytic content; a certified countable protocol registry is." In the Recognition foundation this keeps analytic constants inside a countable, protocol-witnessed carrier rather than an uncountable real line of free parameters, consistent with the forcing chain's demand that physical content be finitely generated from discrete recognition data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.