A counterexample to Erdős 261 propagates along all restarts of its greedy orbit

Write $\operatorname{Rep}$ for a representation $\frac{n}{2^n}=\sum_k \frac{a_k}{2^{a_k}}$ by pairwise distinct positive integers $a_k$ (Erdős Problem 261). With $g_j$ the greedy carry from $(n,n)$, Theorem. If $n\ge2$ has no representation, then $g_j\ne0$ for all $j$, and for every $j$ with $n+j$ even and $2g_j=n+j+2$, the integer $n+j+2$ also has no representation.

This is the contrapositive form of the restart reduction: a minimal counterexample would force an infinite, never-terminating greedy orbit all of whose restart instances are counterexamples too.

Attribution. The mathematical content is due to Borwein and Loring (1990, Algorithm 3 and Proposition 4): the greedy *-binary algorithm may deviate ("cheat") only at states $a_n\in\{n,n+1\}$, and every finite representation of a dyadic rational arises from such a run. In the variables here $a_{N+1}=2g$, and the state $a=N+1$ only leads to infinite tails, so the branch states are exactly $2g_j=N+2$. This corollary of the restart reduction is likewise a repackaging of that result; only the Lean formalization is new.