value_mem
plain-language theorem explainer
Every Delta-real protocol's designated real value sits inside every approximating interval: the lower endpoint at precision n is at most the value, and the value is at most the upper endpoint. Anyone proving uniqueness or observational faithfulness of protocols cites this sandwich. The proof is a one-line pairing of the lower-bound and upper-bound lemmas already on the structure.
Claim. Let $x$ be a Delta-real protocol (a nested family of rational intervals of width at most $1/(n+1)$). Write $\ell_n$ and $h_n$ for the real lower and upper endpoints of the $n$th interval, and let $v = \sup_n \ell_n$ be the value of $x$. Then for every $n \in \mathbb{N}$, $\ell_n \le v \le h_n$.
background
A Protocol (Delta-real) is a nested sequence of rational intervals whose widths shrink at least as fast as $1/(n+1)$. The intended real is the unique point common to every interval. Lower and upper endpoints are cast to $\mathbb{R}$ as lo and hi; the value is defined as the supremum of the lower endpoints.
The module builds a constructive real layer for the primitive recognition calculus: quantities are carried as certified nested approximations rather than bare floats. Nestedness and the width bound force the intervals to shrink to a single real.
Upstream, lo_le_value already records that each lower endpoint is $\le$ the supremum. The matching upper bound value_le_hi is the other half of the sandwich used here.
proof idea
Term-mode constructor: the conjunction is assembled as the pair of the two directed inequalities already proved on Protocol. The left conjunct is lo_le_value (each lower endpoint is $\le$ the supremum). The right conjunct is value_le_hi (the value never exceeds any upper endpoint). No further arithmetic is required.
why it matters
This is the basic membership fact that makes the value the unique real in the nested family. Downstream, value_unique uses it as the comparison half of a squeeze: any real that also lies in every interval must equal the value, via a $1/(n+1)$ bound on the absolute difference. The faithfulness theorem obsEq_iff_value likewise obtains the same bound when comparing two protocols, so observational equality collapses exactly to equality of values.
In the Recognition foundation this sits under the certified analytic layer that feeds later forcing and measurement constructions: protocols are the carrier type for quantities that must be compared without floating-point ambiguity. It does not itself invoke J-cost, phi, or the T0–T8 chain; it is infrastructure those layers rely on when they need a unique real from nested rational data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.