after a skipped m >= 2, another skip within (m, 2m]

$\displaystyle m \ge 2 \ \wedge\ r_m < \frac{1}{2^m-1} \ \Longrightarrow\ \exists n,\ m < n \le 2m \ \wedge\ r_n < \frac{1}{2^n-1}$

Here r is the greedy remainder of 1/2: r_0 = 1/2, r_(m+1) = r_m - 1/(2^m-1) if that term fits under r_m, else r_m. In words: the set A the walk chooses never contains the whole block m+1, ..., 2m right after an element m >= 2 it skipped. A purely combinatorial statement about runs of A. It is stronger than the parent (it also excludes 2^-m < r_m <= 2^-m + 4^-m/3 at a skipped m), and holds numerically to depth 5000 (longest run of consecutive chosen elements 13; the lead reports 20 at depth 10^6, against the m needed at step m).

$\displaystyle \exists\, r:\mathbb{N}\to\mathbb{R},\ \exists\, m:\mathbb{N}:\quad r_0=\tfrac12\ \wedge\ \forall m:\ r_{m+1}=\begin{cases} r_m-\dfrac{1}{2^m-1} & \text{if } \dfrac{1}{2^m-1}\le r_m,\\[4pt] r_m & \text{otherwise}\end{cases}\ \wedge\ 2\le m\ \wedge\ r_m<\frac{1}{2^m-1}$

The witness is the greedy remainder of $\tfrac12$ itself, defined by recursion on $m$ (Nat.rec): $r_0 = \tfrac12$ and the step rule as written, so both equations hold by definition (rfl). Lean convention: at $m = 0$ the term is $\frac{1}{2^0-1} = \frac10 = 0$, so step $0$ is taken and subtracts nothing; $r_1 = \tfrac12$. The skipped step exhibited is $m = 4$: the proof unfolds the four steps $r_1 = r_2 = \tfrac12$, $r_3 = \tfrac16$, $r_4 = \tfrac1{42}$ (steps $2$ and $3$ taken) and checks $\tfrac1{42} < \frac{1}{2^4-1} = \tfrac1{15}$ (norm_num).