lo_le_value
plain-language theorem explainer
Every lower endpoint of a Delta-real protocol sits at or below the real it denotes (the supremum of those endpoints). Interval-arithmetic and constructive-real developments cite this when placing the value inside each approximating interval. The proof is a one-line wrapper of the standard supremum inequality, using the already-proved upper bound on the range of lower endpoints.
Claim. Let $x$ be a nested family of rational intervals with width at most $1/(n+1)$ at stage $n$. Write $\ell_n(x)$ for the lower endpoint of the $n$th interval (as a real) and $v(x)=\sup_k\ell_k(x)$. Then for every $n\in\mathbb{N}$, $\ell_n(x)\le v(x)$.
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 module exposes the lower and upper endpoints as real sequences $\ell_n$ and $h_n$, together with elementary comparison facts such as $\ell_n\le h_m$ across indices.
The denoted value is defined as $v(x)=\sup_n\ell_n(x)$. Boundedness of the range of $\ell$ is already recorded: the zeroth upper endpoint is an upper bound, via the cross-index comparison $\ell_n\le h_0$. That fact is exactly what licenses the supremum construction in classical real analysis.
proof idea
One-line wrapper. Apply the Mathlib lemma that any point of a nonempty set bounded above is at most the supremum of that set, instantiating the set as the range of $\ell$ and the bounded-above witness as the theorem that the range of lower endpoints is bounded above. The natural-number index $n$ selects the corresponding element of the range.
why it matters
This is the left half of the sandwich that puts the denoted value inside every approximating interval. Downstream, membership of the value in each interval is the conjunction of this inequality with the dual upper bound; that membership is the uniqueness engine for addition and negation of protocols (value of sum equals sum of values; value of negation equals negation of value). In the Recognition foundation layer, Delta-reals supply the certified real carrier on which later analytic protocols and transformers evaluate expressions, so the inequality is infrastructure rather than a physics claim. It does not itself invoke the forcing chain, RCL, or $\varphi$-ladder landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.