Restart reduction: Erdős 261 for $n$ is greedy termination or a restart at a branch state

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). Let $g_j$ be the greedy carry from $(n,n)$: $g_0=n$, $g_{j+1}=2g_j-(n+j+1)$ if $2g_j\ge n+j+1$ and $g_{j+1}=2g_j$ otherwise. Theorem. For $n\ge2$, $n$ has a representation iff

So the only freedom beyond the greedy algorithm is a restart at branch states $(N,N/2+1)$: one may skip $N+1$, take $N+2$, and continue with the instance $N+2$. Problem 261 is therefore equivalent to a termination statement for the greedy carry map $R\mapsto 2R\bmod(N+1)$ with restarts.

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 theorem is a repackaging of that result for finite representations of $n/2^n$: after a deviation the remainder is exactly $(N+2)/2^{N+2}$, i.e. the instance $N+2$. The Lean formalization is new; the reduction is not.