lo_le_hi
plain-language theorem explainer
For any Delta-real protocol and precision n, the real lower endpoint of the n-th approximating interval is at most the real upper endpoint. Cited by anyone building nested-interval reals, cross-precision comparisons, or certification intervals that require lo ≤ hi as a field. One-line wrapper: cast the rational interval's built-in order to ℝ.
Claim. For every Delta-real protocol $x$ and every $n \in \mathbb{N}$, if $\ell_n$ and $u_n$ are the lower and upper endpoints of the $n$-th rational approximating interval (coerced to $\mathbb{R}$), then $\ell_n \le u_n$.
background
A Protocol (Delta-real) is a nested family of rational intervals with width at most $1/(n+1)$ at precision $n$. The intended quantity is the unique real lying in every interval. Nestedness says each finer interval is a subset of the previous one; the width bound forces diameters to zero.
The endpoint maps send a protocol and a precision to the lower (resp. upper) rational endpoint of that interval, viewed as a real. The underlying rational interval type already carries an order witness that its lower bound is $\le$ its upper bound (difference nonnegative in the signed-orbit order). This theorem is the real-valued shadow of that fact at fixed precision.
proof idea
One-line wrapper. Pull the order fact from the rational interval at precision $n$ via its built-in $\mathrm{le}$ field, unfold the real endpoint definitions, and finish by modular cast from $\mathbb{Q}$ to $\mathbb{R}$. No arithmetic or nestedness is used.
why it matters
Supplies the fixed-precision order step used by the cross-precision theorem: any lower endpoint is below any upper endpoint (chain lower-mono, this fact at $\max(a,b)$, upper-anti). That cross comparison is the glue that makes nested rational intervals a coherent real.
Downstream, Recognition certification packages closed intervals and zero-width certificates whose structure fields demand $\mathrm{lo}\le\mathrm{hi}$; residue certificates in the RS bridge do the same for rational endpoint pairs. Without the real lift, Delta-reals cannot feed those certificate constructors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.