Centred-interval Schur bound: if $R_k(3) \le r$, then $[1, 2(k+1)\lfloor (r-1)/2 \rfloor + 2]$ has no cover by $k+1$ sumfree sets

This is the centred-interval bound: a bound on the Schur number with $k + 1$ colours from a bound on the triangle Ramsey number with $k$ colours.

Let $k, r \in \mathbb{N}$ and suppose that $\mathrm{TR}(k, r)$ holds (Lean TriangleRamsey k r): every colouring with at most $k$ colours of the pairs $x < y$ of a finite set of at least $r$ naturals has a monochromatic triangle. For $k \ge 1$ this is the inequality $R_k(3) \le r$. A set $S \subseteq \mathbb{N}$ is sumfree if $x + y \notin S$ for all $x, y \in S$, the case $x = y$ included. Put $s = \lfloor (r - 1)/2 \rfloor$. Then the interval $[1, 2((k+1)s + 1)]$ is not covered by $k + 1$ sumfree sets:

For the Schur number $S(k+1)$, the largest $N$ such that $[1, N]$ is partitioned into $k + 1$ sumfree sets, this gives: if $R_k(3) \le r$, then

For example, $R_2(3) = 6$ gives $S(3) \le 13$, which is the true value, and $R_5(3) \le 302$ gives $S(6) \le 1801$. The bound improves on $S(k+1) \le R_{k+1}(3) - 2$ combined with the recursive Ramsey bound only for even $r$. In the mission it fixes the frontier: with $r = 2t + 2$ and $m = (k+1)t$, it excludes $[1, 2m + 2]$, so $[1, 2m + 1]$ is the largest interval that this bound does not exclude for $k + 1$ colours. The other theorems describe a Schur colouring of that interval.

Formalization Note. The cover CoveredBySumFree X (k + 1) asks for $k + 1$ sumfree subsets of $\mathbb{N}$, indexed by Fin (k + 1), whose union contains $X$; they need not be disjoint and need not lie in $X$. A partition into sumfree sets is a special case, so the bound on $S(k+1)$ follows. In TriangleRamsey k r the colours are natural numbers from any Finset of at most $k$ elements, and the pair colouring is a function $\mathbb{N} \to \mathbb{N} \to \mathbb{N}$ that is constrained only on the pairs $x < y$ of the vertex set; for $k \ge 1$ the statement is $R_k(3) \le r$. In $(r - 1)/2$ the subtraction is truncated and the division rounds down; for $r \le 1$ the hypothesis is false, so the truncation never matters. The case $k = 0$ is included: $\mathrm{TR}(0, r)$ holds for $r \ge 2$, and the conclusion says that $[1, 2s + 2]$ is not one sumfree set, which holds since $1 + 1 = 2$.