lo_mono
plain-language theorem explainer
The lower-endpoint sequence of a Delta-real protocol is monotone nondecreasing in the precision index. Anyone comparing nested rational interval approximations in the primitive recognition calculus cites this. The argument reduces monotonicity on naturals to the successive nesting axiom, then coerces the rational lower-bound inequality to reals.
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 $\underline{x}_n$ for the lower endpoint of the $n$th interval, viewed as a real. Then $n \mapsto \underline{x}_n$ is monotone: $m \le n$ implies $\underline{x}_m \le \underline{x}_n$.
background
A Delta-real protocol is a nested family of rational intervals approx : ℕ → RatInterval such that each finer interval is a subset of the coarser one, and the width at precision $n$ is at most $1/(n+1)$. The intended quantity is the unique real lying in every interval.
The lower-endpoint map sends $n$ to the rational lower bound of approx n, coerced to $\mathbb{R}$. Interval subset means the finer lower bound is at least the coarser lower bound, so the sequence of lower endpoints can only rise (or stay) as precision increases.
This lives in the Primitive Recognition Calculus foundation layer: constructive reals built from controlled rational intervals, before measurement extraction. The sibling upper-endpoint map is antitone; together they pin the nested family.
proof idea
One short tactic proof. Apply the standard lemma that a sequence on $\mathbb{N}$ is monotone iff consecutive terms are ordered. For each $n$, the nesting field of the protocol supplies that the interval at $n+1$ is a subset of the interval at $n$; the first component of that subset relation is the inequality on rational lower endpoints. Unfold the lower-endpoint coercion and cast the rational comparison to reals.
why it matters
Feeds the cross-level comparison that any lower endpoint sits below any upper endpoint (used to keep nested intervals coherent), and appears in the construction of protocol addition, which reads both operands at a finer precision so the summed width bound still holds.
Without monotone lower endpoints, one cannot compare approximations at mismatched precisions or close arithmetic on Delta-reals. The result is pure scaffolding for constructive reals inside the Recognition foundation; it does not itself invoke the forcing chain (T5 J-cost, T6 $\varphi$, T7 eight-tick, T8 $D=3$), but those later layers need a clean real carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.