A cover of $\mathbb{Z}_{m_1} \times \mathbb{Z}_{m_2} \setminus \{0\}$ by $q$ sets sumfree in the group lifts to a cover of $\hat A$ by $q$ sumfree sets

This lemma transfers a cover of a finite abelian group by sumfree sets to a cover of a block-sum set of integers. It is the cover part of Lemma 3 of the note.

Let $m_1, m_2 \ge 1$ and $q$ be natural numbers, let $G = \mathbb{Z}_{m_1} \times \mathbb{Z}_{m_2}$, and let $M \ge 3m_1 - 2$. Let $A$ be the lifted sequence of the Lift bundle, that is, the sequence of successive jumps of the grid $X = \{u + Mj : 0 \le u \le m_1 - 1,\ 0 \le j \le m_2 - 1\}$, and let $\hat A$ be its set of block sums. Suppose that $C_1, \dots, C_q \subseteq G$ are sumfree in $G$ ($x + y \notin C_i$ for all $x, y \in C_i$, including $x = y$) and that every nonzero element of $G$ lies in at least one $C_i$. Then $\hat A$ is covered by $q$ sumfree sets of natural numbers:

This is the step from the group to the integers. It gives the Schur-degree bound $\operatorname{sdeg}(\hat A) \le q$ of the lift lemma, and it is used in the lower bound $L(n) \ge m_1 m_2$.

Formalization Note The note assumes that $C_1, \dots, C_q$ partition $G \setminus \{0\}$; the Lean statement only asks that they cover the nonzero elements, which is a weaker hypothesis (a set that is sumfree in $G$ cannot contain $0$). The case $q = 0$ is allowed.