AI 中文总结
该论文证明了 Burr-Erdős-Graham-Sós 猜想在七圈情形（k=3）下成立，即 f(n,⌊n²/4⌋+1,C₇)=(1/8+o(1))n²，通过加权调色板不等式及精确有理证书给出下界，并结合正则性等方法证明上界，同时提供 Lean 4 形式化验证。
AI 中文摘要
对于图 $H$，设 $f(n,e,H)$ 为某个具有至少 $e$ 条边的 $n$ 顶点图进行边着色所需的最少颜色数，使得该图中每个 $H$ 的副本都是彩虹的。Burr、Erdős、Graham 和 Sós 猜想：对每个固定的 $k\ge3$，有 $f(n,\lfloor n^2/4\rfloor+1,C_{2k+1})=(1/8+o(1))n^2$。Bucić、Chen 和 Ma 最近对所有 $k\ge4$ 证明了该猜想。我们证明剩余情形 $k=3$：\\[ f\left(n,\left\lfloor n^2/4\right\rfloor+1,C_7\right) =\left(\frac18+o(1)\right)n^2. \\] 下界依赖于一个加权调色板不等式，我们通过五个采样顶点上的精确有理证书来证明该不等式。其主要成分是相容三角形边的分数匹配和附加于非三角形边的私有资源。该不等式的一个稳定形式，结合正则性、三角形移除以及对接近二部图的直接论证，将界转移到任意边着色上。我们还描述了针对每个固定 $k\ge3$ 的猜想的 Lean 4 形式化，该形式化将新的七圈证明与 Bucić-Chen-Ma 论证（针对 $k\ge4$）的形式化相结合。
英文摘要
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/4\rfloor+1,C_{2k+1})=(1/8+o(1))n^2$ for every fixed $k\ge3$, and Bucić, Chen, and Ma recently proved this for all $k\ge4$. We prove the remaining case $k=3$: \[ f\left(n,\left\lfloor n^2/4\right\rfloor+1,C_7\right) =\left(\frac18+o(1)\right)n^2. \] 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\ge3$, which combines the new seven-cycle proof with a formalization of the Bucić-Chen-Ma argument for $k\ge4$.
Comments20 pages. Lean 4 formalization and certificate verifier: https://github.com/Asad-Shahab/erdos-809-lean
