The sequence $W$, three sumfree classes covering $\hat W$, and four sumfree sets covering $\mathbb{Z}_7 \times \mathbb{Z}_7 \setminus \{0\}$

This bundle records the explicit finite objects of the note from which the lower bounds $L(4) \ge 16$ and $L(5) \ge 49$ are obtained.

1. The sequence $W$ (Lean seqW) of length $15$ and sum $31$, displayed below (note, §2).
2. Three finite sets of positive integers (Lean classesW, indexed by $0, 1, 2$; note, Lemma 2): $C_0 = \{1, 3, 8, 12, 18, 22, 28\}$, $C_1 = \{2, 6, 7, 10, 11, 25, 26, 29, 30\}$ and $C_2 = \{9, 13, 16, 17, 19, 20, 21, 27, 31\}$.
3. Four subsets $D_0, D_1, D_2, D_3$ of $\mathbb{Z}_7 \times \mathbb{Z}_7$ (Lean partitionZ7Z7, indexed by $0, 1, 2, 3$; called $C_0, \dots, C_3$ in Theorem 5 of the note), each with $12$ elements, listed in the table.

The sequence $W$ and, by Lemma 1 of the note, its set of block sums are

where $[a, b] = \{a, a+1, \dots, b\}$; so $\hat W$ has $25$ elements. In the note, $C_0, C_1, C_2$ are sumfree and partition $\hat W$ (Lemma 2), so $\operatorname{sdeg}(\hat W) \le 3$; and $D_0, \dots, D_3$ are sumfree in $\mathbb{Z}_7 \times \mathbb{Z}_7$ and partition its $48$ nonzero elements (Theorem 5).

The sequence $W$ with the classes $C_0, C_1, C_2$ is the witness for $L(4) \ge 16$. The four sets $D_i$, through the lift of the Lift bundle, give $L(5) \ge 49$.

Formalization Note The classes are Lean Finsets indexed by Fin 3 and Fin 4. The bundle contains only the data. The facts that the mission uses (the sumfree property of $C_0, C_1, C_2$ and their cover of $\hat W$, the bound $4L$ on the sum of the first $L$ entries of $W$ for $L \le 15$, and the sumfree property of the $D_i$ in the group and their cover of the nonzero elements) are proved inside the proofs of the theorems that use them. The disjointness of the classes, which the note also states, is not needed there.