Kraft's inequality (sufficiency)

The statement introduces a finite type $\alpha$ (with a Fintype instance and a proof that $\alpha$ is nonempty) and a second finite type $\iota$ (with its own Fintype instance), together with a function $\ell : \iota \to \mathbb{N}$ assigning a natural number to each element of $\iota$. It takes as hypothesis hK the assertion that

where $|\alpha|$ is the (finite) cardinality of $\alpha$ and the sum ranges over all $i$ in the finite index type $\iota$, with the summand for each $i$ computed as a real number. (If $\iota$ is empty, this sum is the empty sum, equal to $0$, and the hypothesis $0 \le 1$ holds automatically/vacuously regardless of $\ell$.)

Given this hypothesis, the theorem's conclusion asserts the existence of a function $c : \iota \to \mathrm{List}\,\alpha$ (assigning to each $i \in \iota$ a finite list, i.e. a "word," of elements of $\alpha$) satisfying, jointly, the following three properties:

1. Injectivity: $c$ is injective as a function, i.e. for all $i, j \in \iota$, if $c(i) = c(j)$ (as lists) then $i = j$; equivalently, distinct elements of $\iota$ are mapped to distinct lists.
2. Length matching: for every $i \in \iota$, the length of the list $c(i)$ equals $\ell(i)$ exactly — i.e. $(c\,i).\mathrm{length} = \ell(i)$ for all $i$, with no slack or inequality, an exact equality for every single index.
3. Unique decodability of the range: writing $S := \mathrm{range}(c) = \{c(i) : i \in \iota\} \subseteq \mathrm{List}\,\alpha$ for the image (as a set) of $c$, the property $\mathrm{UniquelyDecodable}(S)$ holds, which unfolds exactly as follows: for all finite lists of words $L_1, L_2 : \mathrm{List}(\mathrm{List}\,\alpha)$ such that every word $w$ occurring in $L_1$ belongs to $S$ and every word $w$ occurring in $L_2$ belongs to $S$, if the concatenation ("flatten") of $L_1$ equals the concatenation of $L_2$ (as lists of elements of $\alpha$, obtained by flattening each list of lists into one list), then $L_1 = L_2$ as lists (i.e. as sequences — same length, same words in the same order, not merely as sets or multisets). This is a universally quantified statement over all pairs of finite sequences of words drawn from $S$ (repetitions of words from $S$ within $L_1$ or $L_2$ are allowed, and $L_1, L_2$ may have any length, including zero), asserting that the map "concatenate the sequence of words" is injective when restricted to sequences whose words all lie in $S$.

The existential quantifier over $c$ has the widest scope: a single function $c$ is claimed to exist that simultaneously satisfies all three properties (injectivity, exact length-matching for every $i$, and unique decodability of its range), and this is asserted for every choice of $\alpha$, $\iota$, $\ell$, and every proof of $hK$ satisfying the stated hypothesis — i.e. $hK$ is a hypothesis of the theorem, universally bound (implicitly, via the theorem's signature) before the existential claim about $c$.

Nothing in the conclusion states or implies that the set $S = \mathrm{range}(c)$ has the "prefix" property (that no codeword is a prefix of another) or any other structural property of the codewords (such as being a prefix code, suffix code, or satisfying any combinatorial condition on how the words relate to one another as strings) beyond exactly these three stated properties: injectivity of $c$, exact matching of lengths to $\ell$, and unique decodability of the range as defined above. In particular, unique decodability here is stated purely in terms of the flatten/concatenation-injectivity condition on sequences of words drawn from $S$, not in terms of any prefix-free or other syntactic condition on the words themselves.