The largest index of a representation of $n/2^n$ is even

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). Theorem. If $t\ge2$ and $\frac{n}{2^n}=\sum_{k=1}^t\frac{a_k}{2^{a_k}}$ with distinct positive $a_k$, then $\max_k a_k$ is even.

In the carry formulation, the top column has coefficient $c_N=N$ and incoming carry $0$, so $N=2r_N$. (It is the case $a_t-a_{t-1}\ge1$ of the Tengely–Ulas–Zygadło divisibility $2^{a_t-a_{t-1}}\mid a_t$.)

Formalization Note. $\max$ is Finset.univ.sup a.