value_canonical
plain-language theorem explainer
The canonical dyadic nested-interval protocol of any real r evaluates back to r. Anyone identifying classical reals with forgetful displays of certified dyadic protocols cites this identity. The argument is uniqueness of the nested-interval limit, plus the standard floor sandwich that places r inside every dyadic bracket.
Claim. For every real $r$, if $P_r$ is the canonical dyadic protocol whose $n$th interval is $[\lfloor r\cdot 2^n\rfloor/2^n,(\lfloor r\cdot 2^n\rfloor+1)/2^n]$, then the real value extracted from $P_r$ equals $r$.
background
In DeltaReal, a Protocol is a nested family of rational intervals (dyadic brackets) with monotone lower and antitone upper endpoints. The maps lo and hi cast those endpoints to $\mathbb{R}$. The extracted value of a protocol is the unique real lying in every interval (when the nested-interval limit exists and is unique).
The local definition canonical r builds, at each precision $n$, the standard half-open dyadic cell containing $r$: $[\lfloor r\cdot 2^n\rfloor/2^n,(\lfloor r\cdot 2^n\rfloor+1)/2^n]$. Width is exactly $2^{-n}$, so the mesh goes to zero.
This sits in the Primitive Recognition Calculus layer that treats classical $\mathbb{R}$ as a forgetful display of a richer certified object $\mathbb{R}_\delta$. Upstream uniqueness of protocol values is the hinge: once $r$ is shown to inhabit every canonical bracket, it must equal value.
proof idea
Symmetrize the goal and apply the uniqueness lemma for protocol values: it suffices to show $r$ lies in every interval of canonical r.
Fix $n$. Positivity gives $2^n>0$. The floor inequalities $\lfloor r\cdot 2^n\rfloor\le r\cdot 2^n<\lfloor r\cdot 2^n\rfloor+1$ rearrange, after dividing by $2^n$, into lo n ≤ r and r ≤ hi n. Unfold canonical and the endpoint projections, push casts, and finish each side by linarith.
No analytic estimates beyond floor arithmetic are used.
why it matters
Immediate parent is value_surjective: every real is the value of some protocol, witnessed by ⟨canonical r, value_canonical r⟩. That surjectivity is the first half of the Phase 1 headline in this module: classical $\mathbb{R}$ is the forgetful value of the certified dyadic object $\mathbb{R}_\delta$.
In the Recognition foundation stack this closes the display map from nested dyadic certificates back onto ordinary reals, so later forcing and calibration results can quote classical real identities without leaving the protocol layer. It does not itself force $\varphi$, the eight-tick octave, or $D=3$; those live upstream in the Unified Forcing Chain. It is pure reconstruction infrastructure for the real line as a display.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.