value
plain-language theorem explainer
Extracts the real number denoted by a finite expression over a countable registry of certified analytic protocols. Anyone working with countable generation of reals in the primitive recognition calculus cites this. The body is a one-line projection: evaluate the expression tree to a protocol, then take that protocol's real value.
Claim. Given a countable registry $R$ of certified analytic protocol ingredients and a finite expression tree $e$ over $R$, $\mathrm{value}(R,e)$ is the real number denoted by the protocol obtained by evaluating $e$ in $R$.
background
In the primitive recognition calculus, reals are not introduced as an uncountable completed continuum. A protocol is a nested-interval object; its real value is the supremum of the lower endpoints (equivalently, the unique real lying in every interval). That extraction is already defined on protocols in DeltaReal.
A registry packages a countable family of constant protocols and unary protocol transformers. Binary structure is limited to the native additive operations already certified on protocols. Finite expression trees over a registry (rationals, registered constants, negation, addition, subtraction, and registered unary transforms) are the native syntactic objects; evaluation returns a protocol, never an uncountable graph.
This definition is the composite that turns an expression into the real it denotes: evaluate first, then read off the protocol value. The image of this map is the set of registry-generated values, which is countable because the expression trees are countable.
proof idea
One-line definitional wrapper. Apply the expression evaluator for the given registry, then project with the protocol-to-real map (supremum of lower endpoints). No tactics, no lemmas beyond that composition.
why it matters
This is the bridge from countable certified syntax to ordinary real numbers used throughout the monolith. Downstream cost algebra cites it when proving non-negativity of defect distance and when packaging shifted $H$-values; path-space and action-convexity results use the same real readout when comparing action functionals along admissible paths; mass-to-light derivations pull concrete real constants through the same channel.
In Recognition Science terms it supports the discipline that continuum quantities must be generated, not smuggled: every real that enters cost identities, geodesic minimization, or astrophysical ratios is the value of some finite certified expression. That countability fact (registry values form a countable set) is what blocks continuum smuggling into uniqueness and forcing arguments built on the $J$-cost and related analytic protocols.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.