$49 \le L(5) \le 65$ for the number $L(n)$ of Eliahou and Revuelta

This theorem bounds $L(5)$ from both sides.

Let $L(n)$ be the least positive integer $L$ such that every sequence $A$ of positive integers with $|A| = L$ and average $\mu(A) \le n$ has block sums $\hat A$ of Schur degree $\operatorname{sdeg}(\hat A) \ge n$ (Definition 5.1 of Eliahou and Revuelta). Then

The statement has two parts:

1. the lower bound $49 \le L(5)$;
2. the upper bound $L(5) \le 65$.

At $n = 5$, Proposition 5.3 of the paper gives $L(5) \ge S(4) + 1 = 45$, where $S(4) = 44$ is the Schur number, and Conjecture 5.6 states $L(5) = 45$. The lower bound $49$ shows that Conjecture 5.6 does not hold at $n = 5$.

Formalization Note The note gives the upper bound $L(5) \le R_4(3) - 1 \le 61$ from the known bound $R_4(3) \le 62$. The Lean statement has the weaker bound $65$, from the pigeonhole bound $\rho(4) = 66$ of the Ramsey bundle, because the bound $R_4(3) \le 62$ is not formalized here. $L(5)$ is erL 5 of the Basic bundle.