Retained-Set Descent for Diagonal Ramsey Numbers

We use disjoint sets $X,Y\text{,}$ keeping $Y$ fixed and requiring each vertex of $X$ to have at least a fixed positive fraction of $Y$ as red neighbors. The red target $k$ and the blue target $\ell$ in $Y$ stay fixed while the blue target $t$ in $X$ decreases. When $X$ is large enough for a conditional bound at density $q\text{,}$ we either finish at red density at least $q$ or descend to a blue neighborhood of size greater than $(1-q)(|X|-1)\text{.}$ Restricting $X$ to this neighborhood preserves its red degrees into $Y$ and reduces $t$ by one: a blue $K_{t-1}$ there extends through the chosen vertex.

Write the required size of $X$ at $s=t/k$ as $\exp(kg(s))\text{,}$ with $g$ piecewise affine. On a cell of slope $d\text{,}$ the threshold falls by a factor $\mathrm{e}^{-d}$ per step, so we take $d>-\log(1-q)$ to allow for the neighborhood loss. The profile $g$ must also exceed the exponents of the bounds used inside $X\text{.}$ With slopes and calls fixed, optimizing its vertical shift under these conditions and the initial and terminal inequalities gives the cost in Equation 12.

Reusing these bounds and iterating from the source gives a decreasing sequence of exponents whose limit is a greatest fixed point (Theorem 3). Strict inequalities persist on neighborhoods of ratios; compactness selects finitely many neighborhoods and hence a common finite depth for a whole descent. Hence every exponent strictly above the limit has a finite proof, uniformly near its target ratio.

For the lower bound, a concave polygon $F$ assigns exponent $F(s)$ at densities up to $1-\mathrm{e}^{-d}$ on a segment of slope $d\text{.}$ Where a descent using bounds that respect this estimate has $g<F\text{,}$ its call density must exceed $1-\mathrm{e}^{-d}\text{,}$ forcing the slope of $g$ above $d\text{.}$ Thus $g-F$ decreases as the descent moves to smaller ratios. We choose $F$ so that the terminal weighted inequality cannot hold below it. The supporting-line formula reduces this requirement to one-variable inequalities at its vertices (Theorem 4); the certificates in Section 6 complete the proof of Theorem 1.

The Lean 4 formalization and the Python code for exact certificate checks are available in the accompanying repository.¹¹ 1 https://github.com/sichen-wang/diagonal-ramsey-numbers

The weighted inequality uses bounds of the form $R(a,b)\leq x^{-a}y^{-b}\text{.}$ We say that $(x,y)\in(0,1)^{2}$ is an admissible Ramsey pair if this bound holds for all sufficiently large $a+b\text{.}$ Color symmetry in Equation 4 leads to the extension

The source exponent for arbitrary positive targets $a,b$ is then $b\widehat{f}(a/b)\text{.}$ We call $(x,y)\in(0,1)^{2}$ a source pair if $b\widehat{f}(a/b)\leq-a\log x-b\log y$ for all $a,b>0\text{,}$ and write $\mathcal{B}_{f}$ for their set. Every interior point of $\mathcal{B}_{f}$ is admissible: choose a slightly larger pair still in $\mathcal{B}_{f}$ and apply Equation 4 with color symmetry. The resulting error is $o(a+b)\text{,}$ which the strict coordinate gaps absorb.

Supporting lines give a convenient description of these pairs. The source verification shows that $f$ is continuous on $[0,1]$ and is $C^{1}$ on $(0,1]\text{,}$ where it is strictly concave and increasing. It also gives $f(0)=0$ and $2f^{\prime}(1)>f(1)\text{.}$ It follows that $\widehat{f}$ is increasing and concave. On each smooth piece with $t>1\text{,}$ $\widehat{f}^{\prime\prime}(t)=t^{-3}f^{\prime\prime}(1/t)<0\text{;}$ its first derivative is continuous at the reflected source partition points. At $t=1\text{,}$ the derivative drops from $f^{\prime}(1)$ to $f(1)-f^{\prime}(1)\text{.}$ Strict concavity and $f(0)=0$ give $f(s)-sf^{\prime}(s)>0\text{,}$ so the reflected branch is increasing. The expression in Equation 3 gives $\widehat{f}^{\prime}(0+)=\infty\text{,}$ $\widehat{f}^{\prime}(\infty)=0\text{,}$ and $\widehat{f}(t)/t\to 0$ as $t\to\infty\text{.}$

For $A>0\text{,}$ define the intercept of the supporting line with slope $A$ by

For fixed $A>0\text{,}$ $\widehat{f}(t)-At\to-\infty$ as $t\to\infty\text{,}$ while $f(t)/t\to\infty$ as $t\downarrow 0$ makes this expression positive for small positive $t\text{.}$ By continuity, the supremum is positive and attained at some $t>0\text{.}$ At each $t>0\text{,}$ concavity supplies a supporting slope $A>0\text{:}$ use the derivative, or any slope between the one-sided derivatives at $t=1\text{.}$ For this slope $b(A)=\widehat{f}(t)-At\text{,}$ proving the second identity.

Writing $x=\mathrm{e}^{-A}$ and $y=\mathrm{e}^{-B}\text{,}$ the source-pair condition becomes $B\geq b(A)\text{,}$ so

The finite convex function $b$ is continuous on $A>0\text{,}$ so interior source pairs correspond to $B>b(A)\text{.}$ Taking $(a,b)=(1,s)$ in the support inequality gives

Write $N_{\chi}(v)$ for the neighborhood of $v$ in color $\chi\in\{R,B\}$ and $\deg_{\chi}(v,Z)=|N_{\chi}(v)\cap Z|\text{.}$ For disjoint nonempty vertex sets $X,Y\text{,}$ let $e_{R}(X,Y)$ be the number of red edges between them and write $d_{R}(X,Y)=e_{R}(X,Y)/(|X||Y|)\text{.}$ Following [GNNW], a candidate is an ordered pair $(X,Y)$ of such sets. We say that a candidate is $(k,\ell,t)$-good if $X\cup Y$ contains a red $K_{k}\text{,}$ or $X$ contains a blue $K_{t}\text{,}$ or $Y$ contains a blue $K_{\ell}\text{.}$ The target in the retained set $Y$ is $\ell\text{,}$ while the target $t$ in $X$ may decrease.

To reuse a bound during a descent, we need it for an interval of blue-to-red target ratios, with a single size constant and a single threshold for $k\text{.}$

We call $(w,\mu,x,y)$ a strict control at density $p$ when it satisfies the parameter conditions of Lemma 2.1. Write $A=-\log x\text{,}$ $B=-\log y\text{,}$ and $\beta=-\log\mu\text{.}$ Apply the weighted candidate bound with $t=\ell$ to a balanced partition whose red cross-density is at least $p\text{;}$ such a partition exists by averaging. Both set sizes are a constant fraction of the graph’s order, so the corresponding exponent is

Choose $y_{1}>y$ with $(x,y_{1})\in\operatorname{int}\mathcal{B}_{f}\text{.}$ For $\ell=\lfloor rk\rfloor$ and a host of order $N\geq\mathrm{e}^{kL(r)}\text{,}$ the partition satisfies

The first inequality uses $kr\geq\ell$ and $B+w\beta>0\text{;}$ the second holds once $(y_{1}/y)^{\ell}\geq 3^{w+1}\text{.}$ Applying Lemma 2.1 at $(x,y_{1})$ proves $\mathsf{D}(p,L,I)$ with $C=1$ on every compact $I\subset(0,1]\text{.}$ The threshold is uniform in $r\in I\text{,}$ since $\ell\geq k\min I-1\text{.}$ These weighted source bounds are the starting points of our finite derivations, and we call them source leaves.

Fix the partition, calls, slopes, and terminal controls, and vary the vertical position of $g\text{.}$ Put

The quantity $S(s)$ is the cumulative logarithmic loss in descending from $\lambda$ to $s\text{.}$ Every $g$ with the specified slopes has the form $g(s)=H-S(s)$ on $[\theta,\lambda]\text{.}$ The internal conditions are exactly $H>M\text{;}$ they also make $g$ positive, since $M\geq L_{1}(\theta)+S(\theta)>S(\theta)\text{.}$ The conditions in Equation 8 now read

There is such an $H>M$ exactly when

Necessity follows from $z>H>M$ and $(1+w)z>z+wH\text{.}$ Conversely, if $z>Z\text{,}$ choose $H<z$ sufficiently close to $z$ to satisfy both inequalities. Thus $Z$ is the infimum output exponent over these vertical positions. The term $M$ accounts for every internal call together with the loss needed to reach it; the other term is the least exponent compatible with the weighted terminal inequality.

For one call $\mathsf{D}(q,L,[\theta,\lambda])$ with affine $L\text{,}$ choose a slope $d>c(q)\text{.}$ Here $S(s)=d(\lambda-s)\text{,}$ so $L+S$ is affine and its maximum occurs at an endpoint. Substitution in Equation 12 gives

The first two terms require enough vertices to use the call at both ends of the interval; the second includes all the loss incurred before reaching $\theta\text{.}$ The third requires enough vertices to apply the weighted bound at $\theta\text{.}$ Every $z>Z$ therefore gives a new conditional bound at $\lambda\text{.}$

To obtain bounds at smaller target ratios, keep the same calls and terminal controls. For $\theta\leq r\leq\lambda\text{,}$ restrict the profile $g$ to $[0,r]$ and allow a nonnegative vertical shift. Such a shift preserves the inequalities $g>L_{j}\text{.}$ The resulting infimum is

For every $\varepsilon>0\text{,}$ the whole family $\mathsf{D}(p,E+\varepsilon,[\theta,\lambda])$ holds with the constant in Equation 9. To check strictness uniformly, use the shift $H_{r}=E(r)-g(r)+\varepsilon/2$ and output $z_{r}=E(r)+\varepsilon\text{.}$ The endpoint gap is $\varepsilon/2\text{,}$ and

Theorem 2 applies uniformly.

A source leaf is affine, and $E$ is the maximum of two affine functions on each affine piece of $g\text{.}$ When a new route uses one of these bounds as a call, refine its cell at the partition points of the called profile. On each resulting piece, adding the affine loss $S$ preserves convexity. The maximum in Equation 11 is therefore attained at an endpoint of a call cell or a partition point of the called profile inside that cell.

At each positive partition point, we maximize over the stopping ratio and combine the terminal inequalities with the supporting-line formula. This gives a test in the single parameter $\mu\text{.}$ For $0<\mu<1\text{,}$ write $\tau=-\log(1-\mu)$ and $\beta=-\log\mu\text{,}$ and define

For the supplied polygon, the remaining variable is $\tau\in(0,\infty)\text{,}$ with $\mu=1-\mathrm{e}^{-\tau}$ and $\beta(\tau)=-\log(1-\mathrm{e}^{-\tau})\text{.}$ We verify the criterion analytically near zero and infinity, leaving a compact interval for the finite computation. Let $L=1/10$ and $H=10\text{.}$ The supplied data satisfy

For $\tau\leq L\text{,}$ concavity gives $F_{j}\leq d_{1}s_{j}<\beta s_{j}$ for $j>0\text{,}$ so $D_{i}=0\text{.}$ For $\tau\geq H\text{,}$ concavity gives $F_{i}/s_{i}\geq F_{N}$ and hence $D_{i}\geq F_{i}-s_{i}\beta\geq F_{i}/2\text{.}$ Also $D_{i}\leq F_{N}<\tau\text{.}$ The source term in Equation 17 is nonnegative, so

Thus only the closed interval $[L,H]$ requires subdivision.

On each control cell, outward interval arithmetic first encloses $\beta\text{.}$ The function $D_{i}$ is nonincreasing in $\beta\text{,}$ so its two endpoint evaluations enclose the finite maximum in Equation 19. The source $\widehat{f}$ increases, so its endpoint values enclose the source term in Equation 17. A cell is accepted if it proves $D_{i}=0$ throughout, or a nonpositive numerator in Equation 17 wherever $D_{i}>0\text{.}$ Points with $D_{i}=0$ already satisfy the terminal condition, since $F_{i}<A+s_{i}B\text{.}$ Otherwise the checker requires a positive lower bound for $\kappa_{i}$ before division, and accepts the cell only if it proves $P_{i}-\Psi>0\text{.}$ All other cells are subdivided. The checker verifies an exact closed cover of $[L,H]$ for every positive partition point. Theorem 4 then covers all weights, source supports, stopping ratios, endpoint ratios, and finite depths.

Transcendental quantities are enclosed by intervals whose endpoints are integers divided by a fixed power of two. Rational inputs and arithmetic operations are rounded outward. For logarithms, reduce to $y\in[1,2]$ and put $u=(y-1)/(y+1)\in[0,1/3]\text{.}$ Then

The tail is at most $2u^{2m+1}/((2m+1)(1-u^{2}))\text{.}$ The same formula encloses $\log 2$ for reversing the scaling.

For the exponential, put $S_{m}(z)=\sum_{j=0}^{m}z^{j}/j!$ for integers $m\geq 0\text{.}$ Successive terms after degree $m$ have ratio at most $z/(m+2)\text{,}$ so a geometric sum gives

At zero the sum is exact. The interval backend reduces a nonnegative argument to $0\leq y\leq 1/8\text{,}$ where this tail is at most $2y^{m+1}/(m+1)!\text{.}$ Repeated squaring reverses the scaling; negative arguments use outward reciprocals. A logarithm or division is accepted only after its domain is checked. For the final exponential bound, a separate rational calculation applies Equation 23 directly with $m=140$ and compares the upper enclosure with $3.69507\text{.}$

The file data/upper.json contains an ordered list of routes. A call names either a weighted source bound or an earlier route with a terminal control. All 2,932 routes are reachable from the root. The density, height, and output margins are all $10^{-12}\text{;}$ rounding is upward to multiples of $10^{-12}\text{.}$ The source pairs use the inward factor $1-10^{-9}\text{,}$ and we put $\rho=1-2\cdot 10^{-5}\text{.}$

For each control, let $\pi$ be its leaf density when it defines a source bound, and $\rho p$ when it ends a route at outer density $p\text{.}$ The checker computes

and an explicit boundary pair $(\xi,\zeta)$ with $\xi\geq x_{\rm cap}\text{.}$ It uses $x=(1-10^{-9})x_{\rm cap}$ and $y=(1-10^{-9})\zeta\text{.}$ Both coordinates are strictly below a supporting pair, and $x<x_{\rm cap}\text{,}$ so the control is strict. Source supports are given explicitly in the data and checked by interval inequalities. For a source leaf, the coefficients $A/(1+w)$ and $(B+w\beta)/(1+w)$ are rounded upward, giving a rational affine upper bound for Equation 7.

For a reused child with stored profile $g$ and stopping ratio $\theta\text{,}$ upward enclosures of its terminal parameters give rational coefficients

Its called family is

This dominates Equation 13 with a strict allowance; rounding $t^{+}$ upward is valid because $g(s)-g(\theta)\geq 0\text{.}$

With these calls established, the parent route can be evaluated. Each slope is an upward-rounded enclosure of $c(q_{j})+10^{-12}\text{,}$ so the sums defining $S$ are rational. The endpoint rule in Equation 11 gives $M$ by checking the parent cell endpoints and the child profiles’ partition points inside each cell. With $Q=10^{12}\text{,}$ the parent stores

The checker also verifies the full partitions, density implications, child-domain containment, and strict ordering of child indices. Induction through the ordered list and Theorem 2 prove all its conditional families.

The root has

It has 65 cells and uses the left source support in data/upper.json, at $t\approx 0.383\text{.}$ Exact reconstruction gives $g(1)>1.3\text{,}$ while the second term in Equation 13 is less than $1.2\text{.}$ Adding the output margin yields the constant conditional exponent

Thus $U_{\infty}(1/2,1)\leq z_{+}\text{.}$

The file data/lower.json specifies the 2,049 rational partition points and values of $F\text{.}$ Exact rational comparisons establish positive decreasing slopes and $F(0)=0\text{.}$ Interval comparisons establish Equation 18, the tail bounds in Equation 21, and $d_{N}>\log 2\text{.}$ The 853,082 closed control cells verify Equation 20. Theorem 4 and Proposition 5.1 therefore give

The resulting interval for the finite-proof optimum has width less than $0.0016\text{.}$