bddAbove_lo
plain-language theorem explainer
The set of lower endpoints of a Delta-real protocol is bounded above in ℝ. Anyone defining the denoted real as the supremum of those endpoints needs this bound. The proof exhibits the upper endpoint at precision zero as a uniform majorant and invokes the cross comparison of lower and upper endpoints.
Claim. Let $x$ be a Delta-real protocol (a nested family of rational intervals with width at most $1/(n+1)$ at stage $n$). Write $x_{\mathrm{lo}}(n)$ for the lower endpoint of the stage-$n$ interval, viewed as a real. Then the set $\{x_{\mathrm{lo}}(n):n\in\mathbb{N}\}$ is bounded above in $\mathbb{R}$.
background
A Protocol (Delta-real) is a nested sequence 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. The maps lo and hi send each stage to the corresponding endpoint cast to $\mathbb{R}$.
Nestedness and the per-stage bound $x_{\mathrm{lo}}(n)\le x_{\mathrm{hi}}(n)$ together imply a stronger cross inequality: any lower endpoint lies below any upper endpoint, regardless of stage. That fact is recorded as lo_le_hi_cross.
The real value of a protocol is defined as the supremum of the lower-endpoint sequence. Existence of that supremum in $\mathbb{R}$ requires the range to be bounded above; the present lemma supplies exactly that hypothesis.
proof idea
Exhibit an explicit upper bound: the upper endpoint at stage $0$. For an arbitrary element of the range, unpack it as $x_{\mathrm{lo}}(n)$ for some $n$, then apply the cross comparison $x_{\mathrm{lo}}(n)\le x_{\mathrm{hi}}(0)$. The resulting witness package is exactly the definition of BddAbove on a set.
why it matters
This is the boundedness half of the construction of the real denoted by a protocol. Immediately downstream, lo_le_value applies the conditional-supremum lemma le_ciSup with this bound to conclude that every lower endpoint sits below the value $x.{\mathrm{value}}:=\sup_n x_{\mathrm{lo}}(n)$.
In the Primitive Recognition Calculus, Delta-reals are the certified analytic carriers for quantities built from the recognition cost and its fixed-point data. Without a proved upper bound on the lower envelope, the supremum definition of value would be stuck at a noncomputable existence claim. The lemma therefore closes a small but load-bearing gap between the nested-interval structure and the real-valued evaluation map used by certified analytic protocols and transformers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.