$L(n) \ge m_1 m_2$ when $\mathbb{Z}_{m_1} \times \mathbb{Z}_{m_2} \setminus \{0\}$ is covered by $n - 1$ sets sumfree in the group

This is Corollary 4 of the note: a lower bound for $L(n)$ from a finite abelian group.

Let $n \ge 3$ and $m_1, m_2 \ge 1$ be natural numbers, and let $G = \mathbb{Z}_{m_1} \times \mathbb{Z}_{m_2}$. Suppose that $C_1, \dots, C_{n-1} \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

where $L(n)$ is the least positive integer $L$ such that every sequence $A$ of positive integers with $|A| = L$ and average $\mu(A) \le n$ satisfies $\operatorname{sdeg}(\hat A) \ge n$ (Definition 5.1 of Eliahou and Revuelta).

With $n = 5$, $m_1 = m_2 = 7$ and the four sets $D_0, \dots, D_3$ of the Values bundle, it gives $L(5) \ge 49$. For comparison, the lower bound of Proposition 5.3 of the paper at $n = 5$ is $S(4) + 1 = 45$, where $S(4) = 44$ is the Schur number.

Formalization Note The note assumes that $C_1, \dots, C_{n-1}$ partition $G \setminus \{0\}$; the Lean statement only asks that they cover the nonzero elements, a weaker hypothesis. The conditions $m_1, m_2 \ge 1$, which the note takes from Lemma 3, are explicit hypotheses. $L(n)$ is erL n of the Basic bundle.