value_surjective
plain-language theorem explainer
Every classical real number arises as the value of some Delta-real protocol: nested rational intervals of width at most 1/(n+1). Analysts and RS foundation work cite this to recover ℝ as a forgetful display rather than a primitive completed object. The proof is a one-line term: send each real to its canonical constant-interval protocol and apply the evaluation lemma for that construction.
Claim. The evaluation map from Delta-real protocols to $\mathbb{R}$ is surjective: for every $r \in \mathbb{R}$ there exists a nested family of rational intervals of width $\le 1/(n+1)$ whose unique common real is $r$.
background
A Delta-real protocol is a nested sequence of rational intervals whose widths shrink at least as fast as $1/(n+1)$. The intended quantity is the unique real lying in every interval; value extracts that real (via the nested-interval theorem on $\mathbb{R}$).
This module develops the Phase-1 claim that classical $\mathbb{R}$ is not a primitive completed object inside Recognition Science, but the forgetful display of such refinement protocols. Rational constants embed as constant-interval protocols, and protocol arithmetic is defined by native interval rules whose values are ring operations.
Upstream, a canonical protocol is available for each real (constant intervals around a rational approximation tight enough for the width bound), together with the companion fact that evaluating that canonical protocol recovers the original real. Certified analytic protocols supply the ambient value interface used here.
proof idea
Term-mode existence proof. For arbitrary $r:\mathbb{R}$, inhabit the surjectivity witness by the pair consisting of the canonical protocol at $r$ and the lemma that the value of that canonical protocol equals $r$. No further case analysis or completeness argument is replayed at this site; both ingredients are already established for the canonical construction.
why it matters
This is clause (1) of the Phase-1 headline display_real_forgetful: classical $\mathbb{R}$ is recovered as the forgetful value of Delta-real protocols, so analysis never needs more than rational data to any requested precision. Downstream, has_protocol_display uses it to render every finite-description F_RS carrier evaluation into the $\mathbb{R}^\delta$ interface. The Phase-2 guard display_exceeds_generation also depends on it: the value map hits the full continuum while the generable ontology stays countable, blocking uncountable smuggling through the analysis display. In the broader RS foundation this keeps completed reals as presentation, not ontology, consistent with building physics from discrete recognition structure rather than assuming $\mathbb{R}$ as primitive.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.