PROVED (LEAN). Theorem 1(i) of Erdős, Sárközy and Sós (1989) gives, for every $k\ge2$ and every $k$-partition, $|C^2_M|>M/2-3M^{1-2^{-k-1}}$ for $M>M_0(k)$, where $C^2_M$ counts the even integers up to $M$ that are sums of two distinct integers of one class; so at least $cM$ integers up to $M$ are monochromatic sums for any fixed $c<\tfrac12$ once $M$ is large in terms of $k$, which is the statement with the absolute constant $c$. The source is a chapter of a Springer conference volume. The site's suffix (LEAN) is a catalog label whose scope is qualified under Existing formalization below, and no local kernel credit is claimed. The claim page Erdős, Sárközy and Sós 1989 (accepted on the site's crediting of the paper; the Lean 4 formalization of the result is a link on it, neither built nor checked here) records the result, its postings and its acceptance evidence, and the frontmatter standing derives from it.