Goodman-type lower bounds for odd cycles I: The dense regime
Seonghyuk Im, Taeyoung Kim, Hongseok Yang
math.CO
Oct 13, 2026 · v1
TL;DR
The odd-cycle Goodman-type lower bound and strengthened commonality inequality are formalised in Lean 4, with the formalisation produced largely by Claude models.
Abstract
Goodman proved a lower bound on triangle counts which, in graphon language, states that every graphon of edge density $p$ has triangle density at least $2p^2-p$. Bennett, Dudek, Lidický, and Pikhurko established the corresponding bound for $C_5$, determining its minimum density at every Turán density $p=1-1/k$ with an integer $k\ge3$. We extend this bound to every odd cycle in the dense regime: for every odd integer $m\ge3$ and every graphon $W$ with edge density $p\ge2/3$, $t(C_m, W) \ge p^m-p(1-p)^{m-1}.$ For $2/3\le p<1$, equality holds precisely for balanced complete $k$-partite graphons with an integer $k\ge3$, up to graphon equivalence, and we establish qualitative stability at these densities. In the same density range, we also strengthen Kim and Lee's density-sensitive commonality inequality for odd cycles by adding the nonnegative term $t(P_{m-1},1-W)-(1-p)^{m-1}$ to the lower bound, where $P_{m-1}$ is the path with $m-1$ edges. To prove the main results, we develop a spectral excursion expansion and use Dirichlet averaging to reduce the resulting polynomial inequalities in arbitrarily many spectral variables to a one-variable problem. We prove the one-variable inequality through a uniform inequality comparing odd and even moments of shifted Gamma random variables. We also formalise the odd-cycle lower-bound theorem in Lean 4.
Problem
Goodman's bound gives the minimum triangle density at edge density p. The question is whether the analogous bound t(C_m,W) ≥ p^m − p(1−p)^{m−1} holds for every odd cycle C_m and every graphon of edge density p.
Approach
The authors reduce to step graphons and finite matrices. They develop a spectral excursion expansion that writes the inequality gap as polynomial integrals against a nonnegative spectral measure. Dirichlet averaging reduces these multivariable polynomials to a one-variable diagonal case, which is proved via an inequality comparing odd and even moments of shifted Gamma random variables. The main theorems were formalised in Lean 4 by Claude models with minimal author input, and the authors checked that the definitions and statements match the paper.
Results
The bound holds for every odd m ≥ 3 when p ≥ 2/3, with equality exactly for balanced complete k-partite graphons, together with qualitative stability. Kim and Lee's commonality inequality is strengthened by a path-density term. Theorems 1.1, 1.2 and 7.2 are formalised in Lean 4; the stability corollary is not.
