values_countable
plain-language theorem explainer
Any countable registry of certified analytic protocol ingredients generates only countably many real display values. Analysts working the Primitive Recognition Calculus cite this to rule out continuum smuggling through analytic expressions. The proof is a one-line application of range-countability to the evaluation map from finite expression trees.
Claim. For every registry $R$ of certified analytic protocol ingredients (countably many constant protocols and countably many unary protocol transformers), the set of real values obtained by evaluating finite expression trees over $R$ is a countable subset of $\mathbb{R}$.
background
In the Primitive Recognition Calculus, analytic content is carried by Delta-real protocols rather than by arbitrary reals. A Registry packages a countable family of constant protocols and a countable family of unary protocol transformers; binary additive structure is taken from the already-certified Delta-real layer.
Finite expressions over a registry are trees built from rational leaves, addition, negation, registered constants, and registered unary transformers. Evaluation of an expression yields a protocol; the display map then extracts a real. The set of registry values is defined as the range of that display map.
The local goal is to keep every certified analytic construction inside a countable, protocol-witnessed carrier, so that continuum-sized sets cannot enter as "analytic content" by stealth.
proof idea
One-line term proof. The set of values is defined as the range of the evaluation-and-display map from expressions to reals. Mathlib's Set.countable_range then yields countability of that range, because the domain of finite expression trees over a countable label set is countable (implicit in the range lemma application).
why it matters
This is the countability half of transcendental protocol closure: any countably indexed registry generates only countably many reals, each witnessed by a Delta-real protocol. Downstream, transcendental_protocol_closure packages this fact with protocol witnesses and the rational/additive laws. The same pattern lifts to rich registries with binary transformers (rich_transformer_closure, certified_transformer_headline), where the analogous countability lemma is reused.
In the Recognition framework this blocks continuum smuggling: analytic constructions stay on a countable protocol carrier. That discipline supports the forcing-chain style of argument (unique J-cost, phi fixed point, discrete octave structure) by keeping the analytic layer discrete and certifiable rather than continuum-parametrized.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.