I shared the link to this thread with several colleagues, some of whom answered the call and helped me get to the bottom of it. I am especially grateful to Pierre-Yves Bienvenu and Sophie Frisch for taking the time to examine Kneser's paper and Halberstam and Roth's book, and to Melvyn Nathanson for providing some behind-the-scenes information.
$\bullet$ Kneser's paper.
As it turns out, Kneser's theorem (on the structure of sets of non-negative integers with positive lower asymptotic density) can be found at the bottom of p. 463 (of the 1953 paper by Kneser cited in the OP). Below is the English translation by ChatGPT (I'm reproducing the original text as faithfully as I can, except for changing 'natural number' to 'positive integer'):
Density theorem for asymptotic density: Let $\mathfrak{A}_0, \mathfrak{A}_1, \ldots, \mathfrak{A}_n$ be $n+1$ sets of rational integers with the sum $\mathfrak{A} = \sum_{v=0}^n \mathfrak{A}_v$. Then, either $$\delta(\mathfrak{A}) \geq \delta(\mathfrak{A}_0, \mathfrak{A}_1, \ldots, \mathfrak{A}_n),$$ or there exists a positive integer $g$ with the two properties $$\mathfrak{A}^{(g)} \sim \mathfrak{A}$$ and $$\delta(\mathfrak{A}^{(g)}) \geq \delta(\mathfrak{A}_0^{(g)}, \mathfrak{A}_1^{(g)}, \ldots, \mathfrak{A}_n^{(g)}) - \frac{n}{g}.$$
All the necessary notations are explained in the first few lines of Sect. 1 (again on p. 463). In particular, let $X$ be a subset of $\mathbb Z$. Given $g \in \mathbb N^+$, we take $ X^{(g)} := X + \{gx: x \in \mathbb Z\}$; and $X \sim Y$, for some $Y \subseteq \mathbb Z$, means that $X$ and $Y$ are equal from a certain point on. In addition, $$ \delta(X) := \liminf_{k \to \infty} \frac{\bigl|X \cap [\![1, k]\!] \bigr|}{k} $$ is the lower asymptotic density of $X$, whose definition disregards the non-positive elements of $X$ (if there are any) and is then extended to any finite tuple $(X_0, X_1, \ldots, X_n)$ of subsets of $\mathbb Z$ by $$ \delta(X_0, X_1, \ldots, X_n) := \liminf_{k \to \infty} \frac{1}{k} \sum_{v=0}^n \bigl|X_v \cap [\![1, k]\!]\bigr|. $$ The result in the OP is now the special case of the above theorem in which $n = 1$ and $\mathfrak A_0 = \mathfrak A_1$.
$\bullet$ Halberstam and Roth's book.
Please allow me to begin with a complaint. On p. xv of the front matter, the authors write:
We are aware of the drawbacks of elaborate notations and have tried, in various ways, to limit the burden placed on the reader [...]. Nevertheless, throughout the book, we introduce quite a number of notations, many of which are already in common use [...].
For sure, their strategy for limiting "the burden placed on the reader" has not worked with me.
Kneser's theorem is Theorem I.17' on p. 57, which reads as follows (I will reproduce the notations as faithfully as I can, except for writing '$\mathscr V$' and '$V$' instead of the corresponding underlined versions of these same symbols used in the book):
If the system $\mathfrak A$ satisfies $\underline{\mathrm{d}} \mathscr C < \underline{\mathrm{d}} \mathscr{V}$, there exists a natural number $g$ such that $\mathscr C \sim \mathscr C^{(g)}$.
We gather from the first lines of Sect. I.7 (on p. 51) that "the system $\mathfrak A$" in this formulation is a $(k+1)$-tuple $(\mathscr A_0, \mathscr A_1, \ldots, \mathscr A_k)$ of strictly increasing sequences of integers, where a sequence of integers is, as usual, a function from $\mathbb N^+$ (the positive integers) to $\mathbb Z$ (the integers). So, each sequence $\mathscr A_i$ can be equivalently regarded as an infinite subset of $\mathbb Z$ that is bounded from below.
NOTE. Halberstam and Roth denote the integers by $\mathscr Z$, the non-negative integers by $\mathscr Z_0$, and the positive integers (referred to in the book as natural numbers) by $\mathscr Z_1$; this is all explained in the first paragraph of Sect. I.1 (on p. 1).
As for the '$\mathscr C$' and '$\mathscr V$' in the statement of the theorem, these are shorthand notations for $$ \mathscr C(\mathfrak A) := \mathscr A_0 + \mathscr A_1 + \cdots + \mathscr A_k \qquad\text{and}\qquad \mathscr V(\mathfrak A) := \bigvee_{v=0}^k \mathscr A_k, $$ as we can conclude from reading p. 52 (see, in particular, Eqs. (I.7.2) and (I.7.4)).
What is $\bigvee_{v=0}^k \mathscr A_k$? In the words of the authors themselves (see the paragraph following Eq. (I.7.2)), the answer is
[...] the aggregate of the elements of $\mathscr A_0, \mathscr A_1, \ldots, \mathscr A_k$, each element being counted according to its multiplicity; except that $0$, if it occurs at all, is to be counted only once.
It only remains to understand the meaning of $\underline{\mathrm{d}} \mathscr C$ and $\underline{\mathrm{d}} \mathscr{V}$, as the notations $\mathscr C^{(g)}$ and $\mathscr C \sim \mathscr C^{(g)}$ have the same meaning as the analogous ones in the previous block on Kneser's paper (see Definitions I.9 on p. 53 and I.11 on p. 56).
Unsurprisingly, $\underline{\mathrm{d}} \mathscr C$ is just the lower asymptotic density of $\mathscr C$, which (according to the definition on p. xvii of the front matter) is given by $$ \liminf_{n \to \infty} \frac{\bigl|\mathscr C \cap [\![1, n]\!]\bigr|}{n}. $$ As for $\underline{\mathrm{d}} \mathscr{V}$, the paragraph preceding Eq. (I.7.3) on p. 52 reads,
[...] by analogy with the definition of $\underline{\mathrm{d}}\mathscr A$, we write $$\underline{\mathrm{d}} \mathscr{V} = \liminf_{n \to \infty} \frac{1}{n} V(\mathfrak A; n),$$
where, as explained in the paragraph following Eq. (I.7.2),
[...] we denote by $$V(n) = V(\mathfrak A; n)$$ the counting number of the positive part of $\mathscr V(\mathfrak A)$.
In other words, $\underline{\mathrm{d}} \mathscr{V}$ is nothing else than the limit in Eq. (I.7.1) on p. 52, as explicitly noted in the comments preceding Eq. (I.7.3). Namely, $$ \underline{\mathrm{d}} \mathscr{V} = \liminf_{n \to \infty} \frac{1}{n} \sum_{v=0}^k \bigl|\mathscr A_v \cap [\![1,n]\!]\bigr|. $$
Therefore, the result in the OP is the special case of Halberstam and Roth's Theorem I.17' in which $n = 1$ and $\mathscr A_0 = \mathscr A_1$. By the way, Theorem I.17' is proved on p. 70.
$\bullet$ Nathanson's account of Kneser's theorem.
I've learned from Melvyn Nathanson that a modern account of Kneser's theorem and its proof is included in a long-awaited forthcoming volume of his series on additive number theory (I'm sharing this information with Nathanson's permission). Among other things, he mentioned that
[...] The chapter with the proof of Kneser's theorem was actually written 30 years ago, and I lectured on it in a graduate course I gave at Tel Aviv University in 2001.
