An eventual diagonal Ramsey bound

Theorem. For all sufficiently large integers $k$,

$$R(k,k)\le 3.49135655^k.$$

Lean comparison

Declaration excerpts; hypotheses and local notation are as in the linked source. Proof bodies are omitted.

eventual_diagonal_bound

theorem eventual_diagonal_bound :
    ∃ K : ℕ, ∀ k : ℕ, K ≤ k →
      (RamseyBasics.ramseyNumber k k : ℝ) ≤ (3.49135655 : ℝ) ^ k

This refines the method of Zhao, Booth-Clibborn and Schwahn.¹ We reuse their weighted potential, maximality machinery, finite-host closure and source/profile framework (paper sections 3–5), as well as inherited profile and control data. Their construction builds on Lu and Wang's retained-set descent,² whose finite source bound we use.

The refinement below retains the complementary-neighbourhood moment constraint, derives its scalar feasibility and envelope laws, and supplies a retuned source/root construction. The proof is an improvement within this framework.

Proof. Put

$$\begin{aligned} z&=\frac{625145177}{500000000},\\ \gamma&=z+10^{-9}=\frac{250058071}{200000000},\\ b&=\frac{69827131}{20000000}=3.49135655. \end{aligned}$$

Lean comparison

Declaration excerpts; hypotheses and local notation are as in the linked source. Proof bodies are omitted.

rawExponent

def rawExponent : ℚ := 625145177 / 500000000

exponent

def exponent : ℚ := 250058071 / 200000000

base

def base : ℚ := 69827131 / 20000000

We construct constants $C\ge1$ and $k_0$ such that every graph on $N\ge Ce^{zk}$ vertices with red edge density at least $1/2$ contains a monochromatic $K_k$, whenever $k\ge k_0$.

1. Potential and admissible bounds. For disjoint nonempty vertex sets $X,Y$, write $g_y=|N_R(y)\cap X|/|X|$ and $a_+=\max(a,0)$. For $\beta,r>0$, use

$$\Phi_c(X,Y)=|X|^w|Y| \left(\frac1{|Y|}\sum_{y\in Y}(g_y-c)_+^{\beta r}\right)^{1/\beta}.$$

Lean comparison

Inherited definitions, with s = β * r. The displayed exponent 1 / β is the algebraic simplification of the nested positive powers in these definitions.

momentNorm

noncomputable def momentNorm (G : SimpleGraph V) (X Y : Finset V) (c s : ℝ) : ℝ :=
  ((∑ y ∈ Y, (max (colDensity G X y - c) 0) ^ s) / (Y.card : ℝ)) ^ (1 / s)

potential

noncomputable def potential (G : SimpleGraph V) (X Y : Finset V) (c w r s : ℝ) : ℝ :=
  (X.card : ℝ) ^ w * (Y.card : ℝ) * (momentNorm G X Y c s) ^ r

Maximize over restrictions of either set. Source bounds have the form $R(k,\ell)\le C_s e^{A_s k+B_s\ell}$; dense profiles record clique-forcing bounds under a density hypothesis.

2. Consequences of maximality. For positive column excesses, normalize $(g_y-c)^{\beta r}$ to a probability measure $\nu$. For a blue-neighbourhood restriction of fraction $0<q<1$, let $Z$ denote the relative change in excess red density. Blue-move failure and maximality of the complementary restriction give, respectively,

$$\begin{aligned} \mathbb{E}_{\nu}\left[(1+Z)_+^{\beta r}\right] &\le\left(\frac{\mu}{q}\right)^{\beta w},\\ \mathbb{E}_{\nu}\left[\left(1-\frac{q}{1-q}Z\right)_+^{\beta r}\right] &\le(1-q)^{-\beta w}. \end{aligned}$$

Lean comparison

The first declaration gives the strict blue bound, which implies the displayed non-strict inequality. The second gives the complementary bound. Local graph variables and notation are defined in the linked files.

blue_lt

lemma blue_lt {μ w β : ℝ} (hY : Y.Nonempty) (hpos : ∀ y ∈ Y, c < colDensity G X y) (hμ0 : 0 < μ)
    (i : V) (hq0 : 0 < graphFrac B X i)
    (hblue : SharpBlueFailure G B X Y c μ w β s i) :
    ∑ y ∈ Y, nuW G X Y c s y * (max (1 + ZR G B X c i y) 0) ^ s < certU μ w β (graphFrac B X i)

complementary_row_moment

theorem complementary_row_moment
    {V : Type*} [Fintype V] [DecidableEq V]
    (G B : SimpleGraph V) (X Y : Finset V) (c w r β : ℝ)
    (hX : X.Nonempty) (hY : Y.Nonempty) (hr : 0 < r) (hβ : 0 < β)
    (hpos : ∀ y ∈ Y, c < colDensity G X y)
    (hmax : RowColMaximal G X Y c w r (β * r))
    (i : V) (hq : 0 < graphFrac B X i ∧ graphFrac B X i < 1) :
    ∑ y ∈ Y, nuW G X Y c (β * r) y *
      (max (1 - graphFrac B X i / (1 - graphFrac B X i) * ZR G B X c i y) 0) ^
        (β * r) ≤ (1 - graphFrac B X i) ^ (-β * w)

Maximality controls exceptional rows; ordering rows by retained fraction bounds accumulated drift.

3. Reduction to two cells. Conditional Jensen reduces both moments to two conditional means. A density cap excludes a degenerate cell mass; boundedness and compactness give limiting exponential constraints. After the density transfer of Section 4, these take the form

$$\begin{aligned} A_0(q)&\le A,\\ pe^{\beta A}+(1-p)e^{\beta C}&\le U(q),\\ pe^{-\beta tA}+(1-p)e^{-\beta tC}&\le V(q), \end{aligned}$$

Lean comparison

The displayed constraints are exactly Complement.Feasible with the stated budgets and threshold. Section 3 proves their limiting derivation; Section 4 proves density transfer.

Feasible

def Feasible (p β t U V A₀ A C : ℝ) : Prop :=
  A₀ ≤ A ∧
  p * Real.exp (β * A) + (1 - p) * Real.exp (β * C) ≤ U ∧
  p * Real.exp (-β * t * A) + (1 - p) * Real.exp (-β * t * C) ≤ V

where $t=q/(1-q)$, $U(q)=(\mu/q)^{\beta w}$ and $V(q)=(1-q)^{-\beta w}$.

4. Scalar optimization. For each feasible retained fraction $q\in F_p$, let $M_p(q)$ be the maximum of $pA+(1-p)C$ subject to these constraints. The optimizer either has $A=C=\log U(q)/\beta$, or has $A=A_0(q)$ with the positive exponential constraint saturated. Concavity and affine majorants give an explicitly integrable envelope

$$qM_p(q)+wq(1+\log u)\le E(u) \qquad(q\in F_p,\ 0<u\le1).$$

Lean comparison

The displayed majorization is one field of this definition; it also requires regularity, a nonempty feasible set, and a negative integral.

ComplementEnvelope

def ComplementEnvelope (p μ w β x : ℝ) : Prop :=
  (complementDegrees p μ w β x).Nonempty ∧
  ∃ E : ℝ → ℝ, ContinuousOn E (Set.Ioc 0 1) ∧ MonotoneOn E (Set.Ioc 0 1) ∧
    IntervalIntegrable E MeasureTheory.volume 0 1 ∧
    (∀ u ∈ Set.Ioc 0 1, ∀ q ∈ complementDegrees p μ w β x,
      q * certM p μ w β x q + w * q * (1 + Real.log u) ≤ E u) ∧
    (∫ u in (0 : ℝ)..1, E u) < 0

5. The local red–blue alternative. The chosen envelope satisfies $\int_0^1E(u),du&lt;0$. If every useful red and blue move failed, the moment bounds and ordered drift inequality would force the opposite inequality in the limit. Uniform finite approximations preserve the strict gap for sufficiently large $r$. Hence every relevant maximal configuration admits a useful move.

6. Iteration and source admissibility. Iterate these moves along retained-set routes. Prove the source bounds and supporting profiles simultaneously by induction on host order: recursive invocations concern smaller hosts. Terminal controls, support inequalities and interval covers close the construction.

7. The concrete construction. The specified rational parameters, envelope, source family and route covers satisfy those hypotheses. Four child profiles and a twelve-call root construction yield the dense profile at exponent $z$ stated above. This section supplies the finite numerical witnesses and their assembly. Uniform profile samples are specified by affine equations; inherited envelope partitions are generated from tangent intersections and slope changeovers. Concavity derives their global support inequalities from adjacent slope brackets.

8. The Ramsey bound. One colour has density at least $1/2$. Apply the dense profile to $N=\lceil(C+2)e^{zk}\rceil$ and absorb the fixed prefactor:

$$R(k,k)\le\lceil(C+2)e^{zk}\rceil\le e^{\gamma k}$$

Lean comparison

These statements implement the displayed chain: the dense-profile theorem supplies the Ramsey bound, and the ceiling lemma absorbs the prefactor.

eventual_exponent_of_dense_profile

theorem eventual_exponent_of_dense_profile
    {z γ : ℝ} (hz : 0 ≤ z) (hgap : z < γ)
    (hprofile : DenseProfile z) :
    ∀ᶠ k : ℕ in Filter.atTop,
      (RamseyBasics.ramseyNumber k k : ℝ) ≤ Real.exp (γ * k)

eventually_ceiling_exp_le

theorem eventually_ceiling_exp_le {C z γ : ℝ}
    (hC : 1 ≤ C) (hz : 0 ≤ z) (hgap : z < γ) :
    ∀ᶠ k : ℕ in Filter.atTop,
      (⌈C * Real.exp (z * (k : ℝ))⌉₊ : ℝ) ≤ Real.exp (γ * k)

for sufficiently large $k$. With $u=\gamma/2$, exact rational arithmetic gives

$$e^\gamma\le \left(\sum_{j=0}^{13}\frac{u^j}{j!} +\frac{15u^{14}}{14\cdot14!}\right)^2<b.$$

Lean comparison

With exponent and base defined above, the complete Taylor-bound proof is:

exponent_gap

theorem exponent_gap : Real.exp (exponent : ℝ) < (base : ℝ) := by
  have h := Real.exp_bound' (x := (exponent : ℝ) / 2)
    (by norm_num [exponent]) (by norm_num [exponent]) (n := 14) (by norm_num)
  norm_num [exponent, Finset.sum_range_succ, Nat.factorial] at h
  have hdouble : Real.exp (exponent : ℝ) = Real.exp ((exponent : ℝ) / 2) ^ 2 := by
    rw [pow_two, ← Real.exp_add]
    congr 1
    ring
  rw [hdouble]
  norm_num [exponent, base]
  nlinarith [Real.exp_pos (250058071 / 400000000 : ℝ)]

Thus $R(k,k)\le b^k$. $\square$

The independent challenge states the bound directly for finite graphs. Comparator checks its proved solution with permitted axioms propext, Classical.choice and Quot.sound.

For setup, build commands and CI, see verification.

References

See sources and attribution for the foundational formalizations and inherited libraries, and the section READMEs for specific uses.

Footnotes

1. Zhipu Zhao, William Booth-Clibborn and Casper Schwahn, A (3.49…)ᵏ bound for diagonal Ramsey numbers (2026). Paper · Lean code. ↩

2. Zhipeng Lu and Sichen Wang, Retained-Set Descent for Diagonal Ramsey Numbers (2026). arXiv:2609.14525 · Lean code. ↩