Lift lemma: a sumfree $q$-cover of $\mathbb{Z}_{m_1} \times \mathbb{Z}_{m_2} \setminus \{0\}$ gives a positive sequence of length $m_1 m_2 - 1$ with $\operatorname{sdeg}(\hat A) \le q$

This is Lemma 3 of the note: a lift from the finite abelian group $\mathbb{Z}_{m_1} \times \mathbb{Z}_{m_2}$ to sequences of positive integers.

Let $m_1, m_2, q \ge 1$ be natural numbers, let $G = \mathbb{Z}_{m_1} \times \mathbb{Z}_{m_2}$, and let $M \ge 3m_1 - 2$. 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$. Let $A = (a_1, a_2, \dots)$ 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\}$. Let $\hat A$ be the set of block sums of $A$, and $\operatorname{sdeg}$ the Schur degree. Then

and in full the statement has four parts:

1. $A$ has length $|A| = m_1 m_2 - 1$;
2. every entry of $A$ is positive;
3. $\operatorname{sdeg}(\hat A) \le q$;
4. for every $L$ with $0 \le L \le m_1 m_2 - 1$, the first $L$ entries of $A$ have sum $a_1 + \dots + a_L = (L \bmod m_1) + M \lfloor L/m_1 \rfloor$.

The lemma turns a cover of $G \setminus \{0\}$ by sets sumfree in $G$ into a sequence for the property of Definition 5.1 of Eliahou and Revuelta: with $M = 3m_1 - 2$, part 4 bounds the average of every nonempty prefix of $A$ by $3$, and part 3 bounds the Schur degree of its block sums. These are the facts behind the lower bound $L(n) \ge m_1 m_2$ (Corollary 4 of the note).

Formalization Note The Lean statement differs from the note in three places. (1) The note assumes that the $C_i$ partition $G \setminus \{0\}$; here they only need to cover the nonzero elements, a weaker hypothesis. (2) The note bounds the prefix sums by $L \cdot \max(1, M/m_1)$ for $1 \le L \le m_1 m_2 - 1$; part 4 gives their exact value, which implies that bound, and it includes $L = 0$. (3) Part 2 is implicit in the note, where $A$ is the jump sequence of a set. The hypothesis $q \ge 1$ is also in the note: for $q = 0$ the statement fails at $m_1 = m_2 = 1$, where $A$ is empty, $\hat A = \emptyset$ and $\operatorname{sdeg}(\emptyset) = 1$.