values
plain-language theorem explainer
The image of the evaluation map for a rich certified-analytic registry: every real obtained by evaluating a finite expression built from constants and unary/binary protocol transformers. Downstream algebra and physics modules cite it whenever they need the ambient set of admissible real constants. The body is a one-line range definition.
Claim. For a rich registry $R$ (countable constants together with unary and binary protocol transformers), $\mathrm{values}(R)$ is the set of all real numbers obtained by evaluating finite expressions over $R$. Equivalently, $\mathrm{values}(R) = \{ \mathrm{value}_R(e) : e \text{ a finite rich expression} \} \subseteq \mathbb{R}$.
background
In the certified analytic layer, a protocol is a nested real interval sequence whose value is the supremum of its lower endpoints (equivalently the unique real in every interval). A plain registry packages countable constants and transformers; the rich registry adds both unary and binary protocol transformers, so expressions form a larger free algebra of finite trees.
Evaluation of a rich expression yields a protocol; projecting to its real value gives a map from expressions to $\mathbb{R}$. The ordinary-registry sibling already defines the same range construction: "The set of values generated by a registry." The present definition is the identical construction for the richer signature.
Countability of the expression trees (finite trees over countable labels) is the structural fact that later blocks continuum smuggling: only countably many reals can appear as certified values.
proof idea
One-line definitional wrapper: values R is declared as Set.range (value R), where value R sends each rich expression to the real denoted by its evaluated protocol. No lemmas are applied; the body is pure Set.range.
why it matters
This set is the ambient carrier of all reals the foundation is allowed to name via certified analytic protocols. Cost algebra uses it when building the shifted monoid and verifying that $H$ satisfies the multiplicative d'Alembert equation $H(xy)+H(x/y)=2H(x)H(y)$ (the continuous solution being $\cosh$), which sits next to the Recognition Composition Law and the T5 $J$-cost $J(x)=(x+x^{-1})/2-1$.
Astrophysics and chemistry modules pull concrete constants from the same pool: nucleosynthesis mass-to-light tiers on the $\varphi$-ladder, stellar $M/L$ as $\varphi$-powers, ideal HCP $c/a$ ratio bounds, packing efficiencies, and electron-affinity zeros. The definition therefore sits under both the algebraic forcing chain and the numerical extraction of RS-native constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.