canonical
plain-language theorem explainer
Canonical dyadic Protocol for a classical real r: at precision n the interval is the unique length-2^{-n} dyadic cell containing r. Anyone embedding ℝ into Delta-reals or building cost data on nested rational intervals cites this. Nestedness is discharged by the floor-doubling lemma; the width bound is the elementary comparison 2^{-n} ≤ 1/(n+1).
Claim. For every real $r$ there is a Delta-real protocol whose $n$-th rational interval is $\bigl[\lfloor r\cdot 2^n\rfloor/2^n,\,(\lfloor r\cdot 2^n\rfloor+1)/2^n\bigr]$. Consecutive intervals are nested, and the width at stage $n$ is at most $1/(n+1)$.
background
A Protocol (Delta-real) is a nested family of rational intervals approx : ℕ → RatInterval whose width at precision $n$ is bounded by $1/(n+1)$. The intended real is the unique point common to every interval. Lower and upper endpoints are exposed as real-valued maps lo and hi.
The local module builds reals from such controlled nested intervals rather than from Cauchy sequences or Dedekind cuts. The key arithmetic fact used here is floor_double: $\lfloor r\cdot 2^{n+1}\rfloor$ lies in ${2\lfloor r\cdot 2^n\rfloor,, 2\lfloor r\cdot 2^n\rfloor+1}$. That dichotomy is exactly what forces consecutive dyadic cells to nest.
The construction is noncomputable only because it reads the classical floor of a real; once the floors are given, all interval arithmetic is rational.
proof idea
Three structure fields are filled.
approx n is the closed dyadic cell with endpoints $\lfloor r\cdot 2^n\rfloor/2^n$ and $(\lfloor r\cdot 2^n\rfloor+1)/2^n$. The endpoint inequality is immediate: the difference equals $1/2^n>0$.
nested applies floor_double r n. After clearing positive powers of two, the lower-endpoint inequality is $2\lfloor r\cdot 2^n\rfloor \le \lfloor r\cdot 2^{n+1}\rfloor$, and the upper-endpoint inequality is $\lfloor r\cdot 2^{n+1}\rfloor+1 \le 2(\lfloor r\cdot 2^n\rfloor+1)$; both are the cast forms of the doubling bound, finished by nlinarith.
width_bound rewrites the width as exactly $1/2^n$, then proves $n+1\le 2^n$ by a short induction on $n$, and compares reciprocals.
why it matters
This is the standard bridge from classical $\mathbb{R}$ into the Protocol type that the primitive recognition calculus uses as its real line. Downstream cost-algebra packaging (canonicalCostAlgebra, canonicalRecognitionCostSystem, CostAlgebraData, and the uniqueness/nonnegativity lemmas around them) sits on the same foundation layer: once reals are available as nested rational protocols, the carrier $\mathbb{R}_+$ for the cost $J$ and the Recognition Composition Law can be assembled without a second real-number stack.
In the forcing chain the object is infrastructural rather than a T5–T8 landmark: it supplies the analytic substrate on which J-uniqueness, the $\varphi$-fixed point, and the eight-tick octave are later stated. It closes no open sorry; it is the concrete witness that every classical real yields a well-formed Delta-real.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.