value_ofRat

A Delta-real protocol is a nested family of rational intervals whose width at precision $n$ is at most $1/(n+1)$. The intended quantity is the unique real common to every interval. The real value of a protocol is defined as the supremum of its lower endpoints (cast to $\mathbb{R}$).

The constant rational embedding builds, for each $q\in\mathbb{Q}$, the protocol whose every approximation is the degenerate interval $[q,q]$. Nesting and the width bound are immediate: width is zero. Lower endpoints are therefore constantly $q$ as reals.

This sits in the Primitive Recognition Calculus layer that reconstructs classical reals as the forgetful display of certified nested rational protocols, before native arithmetic and observational equality are developed.

Unfold the three definitions in play: value (supremum of lower endpoints), lower-endpoint cast, and the constant rational protocol. After unfolding, every lower endpoint is the cast of $q$, so the supremum collapses to $q$ by a single simp. No external lemmas beyond definitional reduction are required.

This is the rational-embedding clause of the Phase 1 headline display_real_forgetful: classical $\mathbb{R}$ is the forgetful value of Delta-real protocols, and $\mathbb{Q}$ sits inside via the constant protocols with exact value recovery. Downstream, both certified-analytic stacks (CertifiedAnalyticProtocols.value_rat and CertifiedAnalyticTransformers.value_rat) reduce rational-literal evaluation to this identity. It also feeds ofRat_obsEq_iff, which proves the embedding is faithful: two constant rational protocols are observationally equal iff the rationals agree, by rewriting observational equality as equality of values and applying this theorem twice. In the Recognition foundation, that faithfulness is the bridge from constructive interval presentations back to ordinary real equality on the rational subfield.