lo_le_hi_cross
plain-language theorem explainer
Any lower endpoint of a Delta-real protocol sits weakly below any upper endpoint, even at mismatched precisions. Analysts building the real value as a supremum of lowers cite this to bound the range and place the value inside every interval. The proof chains monotonicity of lo, the same-index lo≤hi inequality, and antitonicity of hi through max(a,b), then closes by linear arithmetic.
Claim. Let $x$ be a Delta-real protocol (a nested family of rational intervals with width at most $1/(n+1)$ at precision $n$). Write $\mathrm{lo}_x(n)$ and $\mathrm{hi}_x(n)$ for the lower and upper endpoints of the $n$th interval, cast to $\mathbb{R}$. Then for all $a,b\in\mathbb{N}$, $\mathrm{lo}_x(a)\le\mathrm{hi}_x(b)$.
background
A Protocol (Delta-real) is a nested sequence of rational intervals approx n whose widths shrink at least as fast as $1/(n+1)$. Nestedness means each finer interval is a subset of the coarser one; the intended real is the unique point common to all intervals.
The maps lo and hi send precision $n$ to the lower and upper endpoints as reals. Same-index comparison lo_le_hi is immediate from the interval ordering. Nestedness upgrades to monotonicity of lowers (lo_mono) and antitonicity of uppers (hi_anti): refining never decreases the floor and never increases the ceiling.
This lemma removes the shared-index restriction, so any floor can be compared to any ceiling. That is the comparison needed before taking suprema of the lower sequence.
proof idea
Term-mode proof with three intermediate inequalities and linarith.
- By
lo_monoandle_max_left, $\mathrm{lo}(a)\le\mathrm{lo}(\max(a,b))$. - By
lo_le_hiat the common index $\max(a,b)$, $\mathrm{lo}(\max(a,b))\le\mathrm{hi}(\max(a,b))$. - By
hi_antiandle_max_right, $\mathrm{hi}(\max(a,b))\le\mathrm{hi}(b)$.
Transitivity of $\le$ (via linarith) yields $\mathrm{lo}(a)\le\mathrm{hi}(b)$.
why it matters
This is the cross-precision comparison that makes the Delta-real value well-defined as a real. Downstream, bddAbove_lo uses it with fixed upper endpoint hi 0 to show the range of lowers is bounded above, so the supremum value exists. Then value_le_hi applies it at every lower index against a fixed upper index to prove the value lies under every upper endpoint (and thus in every interval).
In the Recognition foundation stack this is pure analysis scaffolding for constructive reals used by the primitive recognition calculus: nested rational intervals with controlled width, not yet the J-cost or forcing chain. It closes the elementary order facts needed before naming the unique real carried by a protocol.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.