value
plain-language theorem explainer
A Delta-real protocol denotes a unique real given by the supremum of its lower endpoints. Anyone citing constructive reals, certified analytic evaluation, or cost/action functionals built on nested rational intervals uses this extraction. The definition is a one-line iSup of the lower-endpoint sequence.
Claim. Given a protocol $x$ (a nested family of rational intervals with width at most $1/(n+1)$ at stage $n$), the real it denotes is $\sup_n \underline{x}_n$, where $\underline{x}_n$ is the lower endpoint of the $n$-th interval (equivalently, the unique real lying in every interval of the family).
background
In this module a Delta-real is packaged as a Protocol: a sequence of rational intervals that is nested and whose width at precision $n$ is bounded by $1/(n+1)$. The intended mathematical object is the unique real common to all those intervals.
The lower-endpoint map sends each stage $n$ to the real embedding of the rational lower bound of the $n$-th interval. Because the intervals nest and shrink, the sequence of lower endpoints is monotone and bounded above, so its supremum exists in $\mathbb{R}$ and coincides with the intersection point of the family.
Related evaluation maps in the certified-analytic layer extract a real the same way: evaluate an expression to a protocol, then take this value. A separate measurement-protocol structure in RS-native measurement is unrelated naming; here the object is purely the constructive real.
proof idea
Pure definition, not a proved theorem. The body is the single term $\sup_n x.\mathrm{lo},n$ (Lean iSup over the lower-endpoint sequence). No lemmas are applied; noncomputability is inherited from real supremum.
why it matters
This is the bridge from nested rational certificates to ordinary reals used throughout the monolith. Downstream, defect-distance non-negativity and shifted $H$-value algebra in CostAlgebra read costs as reals via this extraction; path-space coercions and geodesic-minimization-via-convexity in the action layer compare action functionals on admissible paths whose values are reals; mass-to-light derivations in astrophysics likewise treat $J$-bits and derived ratios as reals obtained this way.
In the Recognition foundation it is the standard readout for any quantity built by certified analytic protocols or transformers: once a protocol is assembled, value is how the framework names the unique real in every interval. It does not itself force $\phi$, the eight-tick octave, or $D=3$, but every numeric claim that sits on Delta-reals passes through it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.