Kraft's inequality, sufficiency direction, for positive codeword lengths

Let $\alpha$ be a finite nonempty code alphabet with $D=|\alpha|$ letters, let $\iota$ be a finite set of source symbols, and let $\ell:\iota\to\mathbb N$ prescribe a positive codeword length $\ell_i\ge 1$ for each symbol. If the lengths satisfy Kraft's inequality

then there is an injective assignment of codewords $c:\iota\to\alpha^{*}$ with $|c(i)|=\ell_i$ for every $i$ whose set of codewords $\{c(i)\}$ is uniquely decodable, in the sense that distinct finite sequences of codewords have distinct concatenations.

This is the sufficiency direction of Kraft's theorem (Kraft 1949; Cover and Thomas, Elements of Information Theory, Theorem 5.2.1): a prefix code with the prescribed lengths exists, and prefix codes are uniquely decodable. The necessity direction, for uniquely decodable codes, is the Kraft–McMillan inequality available in Mathlib as InformationTheory.kraft_mcmillan_inequality. The positivity hypothesis $\ell_i\ge1$ is essential: a codeword of length $0$ is the empty word, which no uniquely decodable code can contain, and without the hypothesis the statement is false already for a one-symbol source with $\ell\equiv0$ (this is why the earlier platform statement SourceCoding.kraft_inequality_sufficiency was disproved). No lower bound on $D$ is assumed: for $D=1$ the Kraft bound forces at most one symbol, and a single nonempty codeword is uniquely decodable.