hi_anti
plain-language theorem explainer
Upper endpoints of a Delta-real form a nonincreasing sequence of reals. Anyone proving cross-precision comparisons or building interval arithmetic on nested rational approximations cites this. The argument is a short term proof: Mathlib's successor criterion for antitone maps on ℕ, fed by the nested-subset field of the protocol.
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 $h_n$ for the upper endpoint of the interval at precision $n$, viewed as a real. Then $n \mapsto h_n$ is antitone: $m \le n$ implies $h_n \le h_m$.
background
A Delta-real (Protocol) is a constructive stand-in for a real number: a sequence of rational intervals approx n, nested so that the interval at precision $n+1$ sits inside the interval at precision $n$, with width bounded by $1/(n+1)$. The intended real is the unique point common to every interval.
The upper-endpoint projection hi sends each precision $n$ to the right endpoint of approx n, cast to $\mathbb{R}$. Nesting of intervals immediately forces those right endpoints to move left (or stay put) as precision increases; that is the content of this lemma. The matching lower-endpoint map is monotone, proved as a sibling.
The local module builds the elementary calculus of these protocols (order, width, and later arithmetic) before they are used as recognition-native reals.
proof idea
Apply Mathlib's antitone_nat_of_succ_le: it is enough to check the successor step $h_{n+1} \le h_n$. The protocol field nested n supplies a subset relation between the rational intervals at $n+1$ and $n$; the second component of that subset is the inequality of upper endpoints. Unfold hi and discharge the cast from $\mathbb{Q}$ to $\mathbb{R}$ with exact_mod_cast.
why it matters
This is one of the two monotonicity legs that make nested rational intervals usable as reals. Downstream, lo_le_hi_cross chains lower monotonicity, the same-precision bound lo_le_hi, and this antitone upper map to conclude that any lower endpoint sits below any upper endpoint, even at mismatched precisions. Protocol addition also relies on the endpoint projections behaving under refinement when it samples operands at doubled precision to keep the width bound.
In the Recognition foundation this sits under Primitive Recognition Calculus: Delta-reals are the constructive carriers on which later forcing and measurement layers read off limits. It is pure order infrastructure, not a physics claim, but without it the comparison and arithmetic lemmas that feed measurement do not close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.