Labeled open on erdosproblems.com (last edited 1 April 2026), whose commentary credits Bucić, Chen and Ma [BCM26] with the affirmative answer for every $k\ge4$ and records nothing for $k=3$. The frontmatter standing is derived from the claim pages. Two accepted full claims settle the problem on formalized evidence. Each is a Lean proof of the full statement for every $k\ge3$ that this corpus built and audited. No outside review of either proof is known. One is Asad Shahab's claim, filed on erdosproblems.com first (erdosproblems.com's proof claim 358, before the project's 367, both on 27 September 2026). It is a seven-cycle proof with a Lean development for every $k\ge3$. That development was built here at its pinned commit and audited clause by clause against the Statement (see the Formalization paragraph) (claim page (Shahab, 2026)). The other is the project's claim L17, a kernel-checked Lean proof of the full statement for every $k\ge3$, public on GitHub from 24 September 2026, before Shahab's (see "Outside claims and priority"). Its statement was audited by the project's fidelity review and grade of 2026-10-02 (see the Formalization paragraph) (claim page (Plasma AI, 2026)). Its tier-2 standing is the project's own verification, not community acceptance. Bucić, Chen and Ma's theorem is an accepted partial claim covering $k\ge4$ on formalized evidence, namely the $k\ge4$ branches of both developments (claim page (Bucić, Chen and Ma, 2026)). The erdosproblems.com commentary credits the theorem, but on a problem Bloom's catalog labeled OPEN that credit is not acceptance. Bucić, Chen and Ma's Theorem 1.2 (arXiv:2603.18952v1, 19 March 2026, a preprint with no journal record found on 2026-09-18) gives $\chi_S(n,e,C_{2k+1})=e/2+(n/2)\sqrt{e-n^2/4}+o(n^2)$ over the whole range $\lfloor n^2/4\rfloor+1\le e\le\binom n2$. At $e=\lfloor n^2/4\rfloor+1$ this is $n^2/8+o(n^2)$. The case $k=3$ ($C_7$) is outside that theorem. For it, the 1989 paper gives only the lower bound $\chi_S(n,\lfloor n^2/4\rfloor+1,C_7)\ge cn^2$ and the two-clique coloring that its authors say would make $c=1/8$ best possible. No refereed source found determines the $C_7$ constant. Shahab's preprint arXiv:2609.38286 (29 September 2026), unrefereed and not read here, states it (see "Outside claims and priority").