lo
plain-language theorem explainer
Extracts the lower endpoint of a Delta-real's rational interval at precision n, coerced to a real. Anyone working with nested-interval reals, protocol arithmetic, or the value map (sup of lowers) cites this. The body is a one-line cast of the rational lower bound.
Claim. For a Delta-real protocol $x$ (a nested family of rational intervals with width at most $1/(n+1)$) and precision $n\in\mathbb{N}$, $\mathrm{lo}(x,n)$ is the lower endpoint of $x$'s $n$th approximating interval, viewed as a real number.
background
A Protocol (Delta-real) is a nested sequence of rational intervals approx : ℕ → RatInterval with width(approx n) ≤ 1/(n+1). Nestedness means each finer interval sits inside the previous one. The intended real is the unique point common to every interval.
RatInterval carries rational endpoints lo ≤ hi. This definition lifts those rational lowers into ℝ so they can enter real analysis (boundedness, suprema, comparison with uppers).
The module builds a constructive continuum bridge: reals as controlled nested rational intervals rather than Cauchy sequences or Dedekind cuts, matching the Recognition calculus need for explicit precision bounds.
proof idea
Pure definition: coerce (x.approx n).lo : ℚ to ℝ. No proof obligations. Sibling hi does the same for upper endpoints. Downstream lemmas such as lo_le_hi recover the interval inequality after the cast via exact_mod_cast.
why it matters
This is the primitive lower-bound accessor for the entire Delta-real API. It feeds lo_le_hi, lo_mono, lo_le_hi_cross, bddAbove_lo (the range of lowers is bounded above by any upper), and the value map as supremum of lowers. Protocol addition reads both operands' lo at doubled precision so combined width stays controlled. Canonical dyadic protocols and cosmology band checks (e.g. Hubble tension empirical-central-in-band) sit on the same endpoint infrastructure. In the foundation layer it supplies the concrete lower sequence that makes the nested-interval real usable in later forcing and measurement arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.