value_unique
plain-language theorem explainer
Any real that sits in every nested interval of a Delta-real protocol equals that protocol's value (the sup of lower endpoints). Analysts building certified arithmetic on protocols cite this squeeze uniqueness. The proof bounds |y − value| by the width 1/(n+1) at each precision, then invokes the tiny-implies-zero lemma.
Claim. Let $x$ be a Delta-real protocol (nested rational intervals of width at most $1/(n+1)$). If $y \in \mathbb{R}$ satisfies $x.lo(n) \le y \le x.hi(n)$ for every $n \in \mathbb{N}$, then $y$ equals the real value of $x$ (equivalently $\sup_n x.lo(n)$).
background
A Protocol (Delta-real) is a nested family of rational intervals approx : ℕ → RatInterval with width bound width(approx n) ≤ 1/(n+1). The intended quantity is the unique real common to all intervals. The lower and upper endpoint maps lo and hi cast those rationals to reals; nestedness and the width bound force the intervals to shrink onto a single point.
The real value of a protocol is defined as value x := ⨆ n, x.lo n, equivalently the unique real in every interval. Upstream, value_mem places that value inside each interval, and width_real_bound converts the rational width control into a real inequality. The squeeze lemma tiny_le_zero states that a nonnegative real bounded by 1/(n+1) for all n must be zero; that is the only analytic ingredient beyond interval arithmetic.
proof idea
Fix a protocol x and a real y lying in every interval. For each n, combine hy n with x.value_mem n and x.width_real_bound n: both y and x.value sit in an interval of real width at most 1/(n+1), so |y − x.value| ≤ 1/(n+1). The resulting uniform bound, together with nonnegativity of the absolute value, feeds tiny_le_zero, which forces |y − x.value| = 0. Absolute-value vanishing then yields y = x.value by a short linarith cleanup.
why it matters
Uniqueness of the real denoted by a protocol is the hinge for all certified arithmetic on Delta-reals. Downstream, value_add, value_neg, and value_canonical each prove their identities by exhibiting a candidate real inside every interval of the constructed protocol and invoking this theorem (typically via symm; apply value_unique). Without the squeeze, addition and negation of protocols would not be known to realize ordinary real arithmetic, and the canonical embedding of an arbitrary real would not recover that real. In the Primitive Recognition Calculus layer this closes the gap between interval protocols and ordinary reals, so later analytic transformers and registries can treat value as a well-defined evaluation map.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.