The Burr-Erdős-Graham-Sós conjecture for the seven-cycle

For a graph $H$, let $f(n,e,H)$ be the least number of colors in an edge-coloring of some $n$-vertex graph with at least $e$ edges in which every copy of $H$ is rainbow. Burr, Erdős, Graham, and Sós conjectured that $f(n,\lfloor n^2\mathrm{/}4\rfloor +1,C_{2k+1})=(1\mathrm{/}8+o(1))n^2$ for every fixed $k\ge 3$, and Bucić, Chen, and Ma recently proved this for all $k\ge 4$. We prove the remaining case $k=3$: $$f(n,\lfloor n^2\mathrm{/}4\rfloor +1,C_7)=(\frac{1}{8}+o(1))n^2\mathrm{.}$$ The lower bound rests on a weighted palette inequality, which we prove with an exact rational certificate on five sampled vertices. Its main ingredients are a fractional matching of compatible triangular edges and private resources attached to nontriangular edges. A stable form of the inequality, combined with regularity, triangle removal, and a direct argument for graphs close to bipartite, transfers the bound to arbitrary edge-colorings. We also describe a Lean 4 formalization of the conjecture for every fixed $k\ge 3$, which combines the new seven-cycle proof with a formalization of the Bucić-Chen-Ma argument for $k\ge 4$.