width_real_bound
plain-language theorem explainer
For any Delta-real protocol, the real gap between upper and lower endpoints at precision n is at most 1/(n+1). Anyone proving uniqueness or observational faithfulness of the protocol value cites this bound. The proof is a short cast from the rational width axiom through the real embeddings of the endpoints.
Claim. Let $x$ be a Delta-real protocol (a nested family of closed rational intervals with rational width at most $1/(n+1)$ at each precision $n$). Then for every $n\in\mathbb{N}$, writing $\mathrm{lo}_n(x)$ and $\mathrm{hi}_n(x)$ for the real embeddings of the lower and upper endpoints of the $n$th interval, one has $\mathrm{hi}_n(x)-\mathrm{lo}_n(x)\le 1/(n+1)$.
background
A Delta-real protocol packages a sequence of closed rational intervals that nest and shrink: at precision $n$ the rational width is at most $1/(n+1)$. The intended real is the unique point common to every interval. The module works with rational intervals first, then embeds endpoints into $\mathbb{R}$ via the maps $\mathrm{lo}$ and $\mathrm{hi}$.
The rational width of an interval $I$ is simply $I.hi-I.lo$. The protocol structure already records the rational bound width_bound. This lemma is the real-number counterpart of that axiom: once endpoints are cast to $\mathbb{R}$, the same numerical ceiling still holds.
Local setting is the primitive recognition calculus for constructing reals from nested rational data, before uniqueness and observational equality are proved.
proof idea
Start from the protocol axiom that the rational width of approx n is $\le 1/(n+1)$. Unfold rational width and the real endpoint maps. Show that the real difference of the cast endpoints equals the cast of the rational difference (push_cast and ring). Transfer the rational inequality by exact_mod_cast, then finish by casting $1/(n+1)$ from $\mathbb{Q}$ to $\mathbb{R}$. No nesting or monotonicity facts are used; only the width axiom and casting.
why it matters
Uniqueness of the protocol value and the faithfulness of observational equality both need a uniform real diameter bound that vanishes as $n\to\infty$. Downstream, value_unique squeezes any real lying in every interval against the constructed value by bounding $|y-x.value|$ by $1/(n+1)$; obsEq_iff_value likewise bounds $|x.value-y.value|$ by twice that quantity. Without the real lift of the rational width axiom those squeeze arguments cannot start.
In the Recognition foundation this is bookkeeping for the constructive real layer that sits under later forcing and cost calculus, not itself a T0–T8 step. It closes the gap between the rational protocol data and the real arithmetic used by uniqueness and observational equality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.