Solution (source code)

= Solution

The disjoint sets $E_k$ contain at most one applicable summand at each $x$. Thus $F_n$ stabilizes to $F=2^k$ when $x\in E_k$ and to $0$ when $f(x)=0$ or $\infty$. By definition $F\le f\le2F$ (with the extended-value interpretation).