Upper bound $L(k+1) \le \rho(k) - 1$ (ER Proposition 5.3 with the pigeonhole bound)

This is the upper bound of Proposition 5.3 of Eliahou and Revuelta, with the pigeonhole bound $\rho$ in place of the Ramsey numbers.

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 of Schur degree $\operatorname{sdeg}(\hat A) \ge n$. Let $\rho(0) = 2$ and $\rho(k+1) = (k+1)(\rho(k) - 1) + 2$. Then for every $k \in \mathbb{N}$,

The values $\rho(1) - 1, \dots, \rho(4) - 1 = 2, 5, 16, 65$ give $L(2) \le 2$, $L(3) \le 5$, $L(4) \le 16$ and $L(5) \le 65$. The first two agree with the values $L(2) = 2$ and $L(3) = 5$ of the paper, and the last is the upper half of the bounds $49 \le L(5) \le 65$ of the mission.

Formalization Note The paper states $L(n) \le R_{n-1}(3) - 1$ for $n \ge 2$; the Lean statement has $n = k + 1$ for every $k \ge 0$, and $\rho(k) \ge R_k(3)$ in place of $R_k(3)$. At $k = 4$ it gives $65$, while the known bound $R_4(3) \le 62$ with Proposition 5.3 gives $L(5) \le 61$. The subtraction is ordinary subtraction because $\rho(k) \ge 2$.