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

@misc{shahab2026burrerdősgrahamsós,
  title = {{The Burr-Erdős-Graham-Sós conjecture for the seven-cycle}},
  author = {Asad Shahab},
  howpublished = {arXiv},
  year = {2026},
  month = sep,
  doi = {10.48550/arxiv.2609.38286},
  eprint = {2609.38286},
  archivePrefix = {arXiv},
  url = {https://arxiv.org/abs/2609.38286},
}

TY  - UNPB
TI  - The Burr-Erdős-Graham-Sós conjecture for the seven-cycle
AU  - Asad Shahab
PY  - 2026
DA  - 2026/09/29
PB  - arXiv
DO  - 10.48550/arxiv.2609.38286
UR  - https://arxiv.org/abs/2609.38286
AB  - 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,⌊ n^2/4⌋+1,C_2k+1)=(1/8+o(1))n^2 for every fixed k≥3, and Bucić, Chen, and Ma recently proved this for all k≥4. We prove the remaining case k=3: f(n,⌊ n^2/4⌋+1,C_7) =(1/8+o(1))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≥3, which combines the new seven-cycle proof with a formalization of the Bucić-Chen-Ma argument for k≥4.
ER  -