Bell–Chueluecha–Warnke bound $f(n,k) \le (Ck\log n)^n$

Proved

Erdos20.bell_chueluecha_warnke_bound

by Lucas · Sep 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricserdos-problemssunflower

Let $f(n,k)$ be the sunflower threshold. There is a constant $C \ge 4$ such that for all integers $n \ge 2$ and $k \ge 2$ ,

f(n,k) \le \bigl(C\, k \log n\bigr)^n.

This is Theorem 1 of Bell, Chueluecha and Warnke (2021), written there as $\mathrm{Sun}(p,k) \le (Cp\log k)^k$ with $p$ petals and set size $k$ ; it is the best known general upper bound.

Formalization Note $\log$ is the natural logarithm. Their $\mathrm{Sun}(p,k)$ is the least $s$ such that every family of at least $s$ distinct $k$ -element sets has a $p$ -sunflower, which is exactly $f(k,p)$ here, so no $+1$ appears.

Preamble

import Definitions.Def_Erdos20_defs
import Mathlib

Formal statement

namespace Erdos20
theorem bell_chueluecha_warnke_bound :
    ∃ C : ℝ, 4 ≤ C ∧ ∀ n k : ℕ, 2 ≤ n → 2 ≤ k →
      (f n k : ℝ) ≤ (C * k * Real.log n) ^ n := by sorry
end Erdos20

Source

T. Bell, S. Chueluecha, L. Warnke, Note on sunflowers, Discrete Mathematics 344 (2021), arXiv:2009.09327, Theorem 1 (p. 1)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent that drafted the statements; non-blind

Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted the Lean statements of this proposal (not by a blind auditor with a fresh context), and that agent had seen the source material and knew the intended meaning while writing it. Reviewers should not treat it as independent evidence of faithfulness; compare the Lean code against the source directly.

The statement asserts: there exists a real number $C$ with $C \ge 4$ such that for all natural numbers $n, k$ with $2 \le n$ and $2 \le k$ ,

f(n,k) \le \bigl(C \cdot k \cdot \ln n\bigr)^n,

where $f(n,k)$ is regarded as a real number, $\ln$ is the natural logarithm (positive since $n\ge2$ ), and the power has natural-number exponent $n$ . Here $f(n,k)$ is the sunflower threshold: the least $m\in\mathbb N$ (with $\inf\emptyset := 0$ ) such that for every type $\alpha$ and every family $\mathcal F$ of subsets of $\alpha$ all of whose members have $\operatorname{ncard} = n$ and with $m \le \operatorname{ncard}(\mathcal F)$ , some subfamily $\mathcal S\subseteq\mathcal F$ with $\operatorname{ncard}(\mathcal S)=k$ has all pairwise intersections of distinct members equal to one common set ( $\operatorname{ncard}$ counts elements of finite sets and is $0$ on infinite sets).

Human review

Endorsed by Shuze Chen · Sep 26, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Sep 26, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Bell–Chueluecha–Warnke bound f(n,k)≤(Cklog⁡n)nf(n,k) \le (Ck\log n)^nf(n,k)≤(Cklogn)n

Bell–Chueluecha–Warnke bound $f(n,k) \le (Ck\log n)^n$