value
plain-language theorem explainer
Extracts the real number denoted by a finite expression built from a rich certified-analytic registry. Any development that needs a concrete ℝ from nested protocol transformers (cost algebra, action functionals, mass-to-light) cites this projection. The body is a one-line unwrap: evaluate the expression to a protocol, then take that protocol's real value.
Claim. Given a rich registry $R$ (countable constants plus unary and binary protocol transformers) and a finite expression $e$ over $R$, $\mathrm{value}(R,e)$ is the real number denoted by the protocol obtained by evaluating $e$ in $R$.
background
In the certified analytic layer, a protocol is a nested real interval whose lower endpoints determine a unique real: the supremum of those lowers (equivalently, the unique point in every interval). The simpler registry/expression pair already exposes evaluation-then-display as a real. This module lifts that pattern to a richer registry.
A rich registry supplies three countable families: constant protocols, unary transformers of protocols, and binary transformers. Finite expressions over it are built from rationals, named constants, negation, addition, subtraction, and applications of those unary/binary transformers. Evaluation walks the expression tree and returns a protocol; the real value is then the protocol's denoted real.
Local setting: Primitive Recognition Calculus needs a closed, countable language of certified reals so that cost functionals, defect distances, and derived astrophysical ratios can be stated as concrete ℝ expressions without leaving the formal development.
proof idea
One-line definitional wrapper. Compose the rich-expression evaluator with the protocol-to-real projection: evaluate $e$ under $R$ to a protocol, then take that protocol's value (supremum of lower endpoints). No separate lemmas are invoked in the body; the work lives in eval and in the upstream protocol value.
why it matters
This is the standard bridge from rich certified expressions to ordinary reals. Downstream it feeds cost algebra (nonnegativity of defect distance, shifted $H$-value arithmetic), path-space coercions and geodesic minimality via convexity of the action, and astrophysical mass-to-light derivations that need explicit real constants such as bit costs on the $\varphi$-ladder.
In the Recognition framework it sits under the foundation layer that makes the J-cost and related functionals computable as reals inside Lean, so later forcing-chain and composition-law arguments can quote concrete numeric values rather than abstract protocols. It is infrastructure, not a forcing step itself, but without it the forty-plus use sites cannot discharge their real-valued claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.