floor_double
plain-language theorem explainer
For any real r and natural n, the dyadic floor at scale n+1 equals either twice the floor at scale n, or one more than that. Anyone proving nested dyadic approximations of reals cites this dichotomy. The proof doubles the standard floor sandwich inequalities, rewrites the power, and closes with Int.le_floor / Int.floor_lt plus nlinarith and omega.
Claim. For every real $r$ and every natural number $n$, $$2\lfloor r\cdot 2^n\rfloor \le \lfloor r\cdot 2^{n+1}\rfloor \le 2\lfloor r\cdot 2^n\rfloor + 1.$$ Equivalently, $\lfloor r\cdot 2^{n+1}\rfloor \in \{2\lfloor r\cdot 2^n\rfloor,\, 2\lfloor r\cdot 2^n\rfloor+1\}$.
background
The module builds reals as limits of nested dyadic rational intervals. A Protocol is a precision-indexed family of rational intervals with controlled width and nesting; the canonical protocol of a real $r$ at precision $n$ returns the unit dyadic cell
$$\bigl[\lfloor r\cdot 2^n\rfloor/2^n,;(\lfloor r\cdot 2^n\rfloor+1)/2^n\bigr].$$
The integer floor satisfies $\lfloor x\rfloor\le x<\lfloor x\rfloor+1$. Scaling the argument from $2^n$ to $2^{n+1}$ multiplies by two, so the new floor can only be $2\lfloor r\cdot 2^n\rfloor$ or one more. That two-point dichotomy is exactly the arithmetic reason consecutive dyadic cells nest (lower endpoint nondecreasing, upper endpoint nonincreasing).
Sibling material in the same file defines RatInterval, width, subset/overlap relations, and the Protocol structure with its lo/hi monotonicity lemmas.
proof idea
Record the two floor axioms at scale $n$:
$\lfloor r\cdot 2^n\rfloor\le r\cdot 2^n<\lfloor r\cdot 2^n\rfloor+1$.
Rewrite $r\cdot 2^{n+1}=(r\cdot 2^n)\cdot 2$ by pow_succ and ring.
Lower bound: apply Int.le_floor, push casts, rewrite the power identity, and finish by nlinarith on the doubled lower inequality.
Upper bound: first prove the strict inequality $\lfloor r\cdot 2^{n+1}\rfloor<2\lfloor r\cdot 2^n\rfloor+2$ via Int.floor_lt and nlinarith on the doubled strict upper inequality; then omega tightens it to the claimed non-strict bound $\le 2\lfloor r\cdot 2^n\rfloor+1$.
why it matters
This is the arithmetic engine behind the canonical dyadic protocol of a real. The protocol constructor packages the unit dyadic cell at each precision; without the doubling dichotomy one cannot prove those cells nest, which is required for the Protocol interface (monotonic lo/hi).
In the Recognition foundation, continuum quantities are recovered from completed traces of distinction acts. The dyadic protocol is the concrete approximation scheme that turns an arbitrary real into a recognition protocol with shrinking rational intervals. The lemma itself is classical real arithmetic, independent of $\varphi$, $J$-cost, or the forcing chain, yet it sits at the base of every later comparison between continuum observables and discrete recognition ticks.
Downstream it is consumed directly by the canonical protocol definition in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.