Solution (source code)

= Solution

The <codeword> lengths are <integers>. For necessity, take $L=\max_k l_k$ and view <codewords> as <nodes> of the <binary tree>. A <codeword> of length $l_k$ has $2^{L-l_k}$ descendant words at depth $L$. <Prefix code>[Prefix-freeness] makes these descendant <sets> disjoint, so
$$
\sum_k2^{L-l_k}\leq2^L,\qquad\text{hence}\quad\sum_k2^{-l_k}\leq1.
$$
For sufficiency, reorder the lengths nondecreasingly. Assign words successively. At depth $l_k$, words extending previously assigned <codewords> number
$$
\sum_{i<k}2^{l_k-l_i}.
$$
The asserted <inequality>, even after dropping the later nonnegative terms, gives
$$
\sum_{i<k}2^{l_k-l_i}+1\leq2^{l_k}.
$$
Thus at least one depth-$l_k$ word does not extend an earlier word. Choose it. Since lengths are nondecreasing, it cannot be a proper prefix of a shorter earlier word, and equal-length duplicates have been excluded. <Induction> constructs the required code. Therefore <Kraft inequality> is necessary and sufficient:
$$
\boxed{\text{a binary prefix code with these lengths exists}\iff\sum_k2^{-l_k}\leq1.}
$$