The property defining $L(4)$ fails at every length $1 \le L \le 15$

This theorem is the lower half of $L(4) = 16$.

For a natural number $L$, let $P_4(L)$ be the property of Definition 5.1 of Eliahou and Revuelta at $n = 4$: every sequence $A$ of positive integers with $|A| = L$ and average $\mu(A) \le 4$ has $\operatorname{sdeg}(\hat A) \ge 4$. Here $\hat A$ is the set of sums of the nonempty runs of consecutive entries of $A$, and $\operatorname{sdeg}(X)$ is the least $n \ge 1$ such that $X$ is covered by $n$ sumfree sets ($\infty$ if there is none). Then

That is, for each such $L$ there is a sequence $A$ of $L$ positive integers with $\mu(A) \le 4$ and $\operatorname{sdeg}(\hat A) \le 3$.

Since $L(4)$ is the least positive $L$ such that $P_4(L)$ holds, this gives $L(4) \ge 16$. The case $L = 14$ answers, in the negative, the question that Eliahou and Revuelta ask after Conjecture 5.6: whether every sequence of positive integers of length $14$ and average at most $4$ has $\operatorname{sdeg}(\hat A) \ge 4$.

Formalization Note $P_4(L)$ is ERProperty 4 L of the Basic bundle: the average is computed in $\mathbb{Q}$, and the Schur degree in the extended naturals, where $\operatorname{sdeg}(\hat A) \le 3$ is the negation of $\operatorname{sdeg}(\hat A) \ge 4$.