values
plain-language theorem explainer
For any countable registry of certified analytic protocols, this is the set of all real numbers obtained by evaluating finite expression trees over that registry. Anyone citing certified-real closure, continuum-smuggling blocks, or registry-generated constants uses it. The body is a one-line range definition of the evaluation map.
Claim. Given a registry $R$ of certified analytic protocol ingredients, $\mathrm{values}(R) := \{ v \in \mathbb{R} : v = \mathrm{value}_R(e)\ \text{for some finite expression}\ e\}$ is the image of the evaluation map from finite expression trees over $R$ into $\mathbb{R}$.
background
A registry packages a countable family of constant protocols and unary protocol transformers. Finite expressions over a registry are trees built from those ingredients; evaluation returns a protocol (a nested real interval sequence from DeltaReal), never an uncountable graph of reals.
The real denoted by a protocol is the supremum of its lower endpoints (equivalently the unique real in every nested interval). The sibling value composes evaluation with that display map: value R e = (eval R e).value.
This module sits in the Primitive Recognition Calculus layer: analytic constants and transforms must be generated from countable certified ingredients so that continuum-sized choice cannot enter the forcing chain or the cost algebra by stealth.
proof idea
Definitional one-liner: values R is exactly Set.range (value R), the image of the expression-to-real map. No tactics, no lemmas applied beyond the prior definition of value.
why it matters
This set is the ambient carrier for every real that a certified analytic registry is allowed to name. Downstream, CostAlgebra uses registry-generated values when relating the cost functional $H$ to the d'Alembert equation (the multiplicative form whose continuous solutions are cosh, tying back to T5 J-uniqueness and the Recognition Composition Law). Astrophysics and chemistry modules (nucleosynthesis M/L tiers, stellar assembly $\varphi$-powers, HCP packing ratios, electron affinities) pull concrete constants through the same image.
The sibling countability fact (values_countable) is the operational payoff: because expressions are finite trees over countable labels, the value set is countable, which is the explicit block against continuum smuggling into the foundation. Without a named image set, that countability statement and the forty-plus use sites would have nowhere to land.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.