ofRat
plain-language theorem explainer
Embeds each rational as a constant Delta-real protocol whose every approximation interval is the singleton [q,q]. Anyone building the rational spine inside the completion, or evaluating certified-analytic expressions, cites this embedding. The construction is immediate: nestedness and the width bound hold because the width is identically zero.
Claim. For every rational $q \in \mathbb{Q}$, there is a Delta-real protocol whose approximation at every precision $n$ is the degenerate closed interval $[q,q]$. Nestedness holds by reflexivity of $\le$ on the endpoints, and the interval width is $0 \le 1/(n+1)$.
background
A Delta-real protocol is a nested family of closed rational intervals whose width at precision $n$ is at most $1/(n+1)$. The intended quantity is the unique real common to all intervals. A closed rational interval is a pair $(\mathrm{lo},\mathrm{hi})$ of rationals with $\mathrm{lo}\le\mathrm{hi}$; its width is $\mathrm{hi}-\mathrm{lo}$.
This module builds the real line from such protocols rather than from classical Cauchy sequences or Dedekind cuts. The constant protocol at a rational is the base embedding of $\mathbb{Q}$ into that presentation: every stage is the same singleton interval.
Upstream, reflexivity of rational order supplies the endpoint inequalities needed for both the interval constructor and the nestedness certificates.
proof idea
Define the approximation map to ignore the precision index and return the degenerate interval $\langle q,q,\mathrm{le_refl},q\rangle$. Nestedness is the pair of reflexive inequalities on the fixed endpoints. The width bound unfolds width to $q-q$, simplifies by $\mathrm{sub_self}$ to $0$, and finishes by positivity against $1/(n+1)$.
why it matters
This is the rational spine of the Delta-real presentation. Downstream, $\mathrm{value}$ of the constant protocol recovers $q$ as a classical real, and observational equality of two constant protocols is exactly equality of the underlying rationals; both feed the Phase 1 headline that the classical real line is the forgetful value of a protocol (surjectivity of value, faithfulness of observational equality, and native ring operations).
Certified-analytic expression evaluators send the rational constructor to this embedding, so every finite expression tree bottoms out here. The same embedding appears in the null-distance quotient carrier and in the continuum forcing argument that recognition laws on the completion force the canonical cost $J(x)=(x+1/x)/2-1$ (T5 J-uniqueness on $R_\delta$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.