hi
plain-language theorem explainer
Extracts the upper endpoint of the nth nested rational interval of a Delta-real and coerces it to a real. Anyone working with the constructive real layer of the primitive recognition calculus cites this accessor. The body is a one-line field projection plus cast.
Claim. For a Delta-real $x$ (a nested family of rational intervals with width at most $1/(n+1)$ at stage $n$) and any $n \in \mathbb{N}$, the value $\mathrm{hi}(x,n)$ is the upper endpoint of the stage-$n$ interval, viewed as an element of $\mathbb{R}$.
background
A Delta-real (structure Protocol in this module) is a nested family 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 in the family. Each stage is a RatInterval with rational lower and upper endpoints and a nonnegative width.
This module builds the real-analytic interface around that constructive presentation: lower and upper endpoint sequences, monotonicity, and cross inequalities that pin the intersection to a single real. The companion accessor for lower endpoints is defined in the same namespace.
The name Protocol here is the Delta-real structure, not the measurement-protocol structure from RS-native measurement (which records how an observable is extracted from a state or trace).
proof idea
Pure definition: project the stage-$n$ rational interval of $x$, take its upper endpoint field, and coerce that rational to a real. No lemmas or tactics.
why it matters
Supplies the upper-bound sequence used throughout the Delta-real calculus: nestedness, width control, and the squeeze that identifies the unique real. Sibling facts such as endpoint ordering and monotonicity of the upper sequence are stated in terms of this accessor.
In the Recognition foundation stack this is scaffolding for constructive reals inside the primitive recognition calculus, not a forcing-chain step (T0–T8) or a physical constant identity. No downstream theorems currently depend on it in the graph, so its role is local infrastructure for later uniqueness and limit arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.