\documentclass[a4paper,11pt,twoside]{amsart} \usepackage[english]{babel} \usepackage[utf8]{inputenc} \usepackage[a4paper,inner=3cm,outer=3cm,top=4cm,bottom=4cm]{geometry} \usepackage{fancyhdr} \pagestyle{fancy} \renewcommand{\headrulewidth}{0pt} \fancyhf{} \fancyhead[LE]{\thepage} \fancyhead[RO]{\thepage} \setlength{\headheight}{13.6pt} \usepackage{amsmath} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsthm} \usepackage{mathtools} \usepackage{booktabs} \usepackage[citecolor=green,linkcolor=red]{hyperref} \newtheorem{theorem}{Theorem}[section] \newtheorem{conjecture}[theorem]{Conjecture} \newtheorem{lemma}[theorem]{Lemma} \newtheorem{proposition}[theorem]{Proposition} \theoremstyle{definition} \newtheorem{remark}[theorem]{Remark} \numberwithin{equation}{section} \newcommand\N{\mathbb{N}} \newcommand\Z{\mathbb{Z}} \newcommand\C{\mathbb{C}} \newcommand\eps{\varepsilon} \newcommand{\Log}{\operatorname{Log}} \renewcommand{\Re}{\operatorname{Re}} \renewcommand{\Im}{\operatorname{Im}} \newcommand{\disc}{\mathcal{D}} \newcommand{\Sol}{\mathcal{S}} \newcommand{\Lag}{\mathcal{L}} \newcommand{\lean}[1]{\texttt{#1}} \begin{document} \title{An improved upper bound on the number of representations of an integer as a binomial coefficient} \author{Ben Whitmore} \begin{abstract} Let $N(t)$ be the number of pairs of integers $(n,m)$ with $\binom nm=t$. Singmaster conjectured that $N(t)=O(1)$, and the best bounds in the literature are $N(t)=O(\log t\,\log\log\log t/(\log\log t)^3)$ unconditionally, and $N(t)=O((\log t)^{2/3+\eps})$ conditional on Cram\'er's conjecture. We show that $N(t)=O((\log t)^{1/2+o(1)})$ unconditionally. Solutions with $m\ge\exp((\log n)^{2/3+\eps})$ are handled by a theorem of Matom\"aki, Radziwi\l\l, Shao, Tao and Ter\"av\"ainen. For smaller $m$ we show, using an interpolation determinant in the spirit of Bombieri and Pila, that the solutions with $m$ in a short interval lie on a single algebraic curve of low degree in $n$, and we bound the number of solutions on such a curve by a zero estimate for exponential polynomials. \end{abstract} \maketitle \section{Introduction} For an integer $t\ge2$ let \[ N(t)=\#\Big\{(n,m)\in\N^2:\binom nm=t\Big\}. \] Every pair counted here has $1\le m\le n-1$ and $n\le t$, so $N(t)$ is finite. In 1971 Singmaster~\cite{singmaster} made the following conjecture. \begin{conjecture}[Singmaster's conjecture]\label{conj:singmaster} $N(t)=O(1)$. \end{conjecture} The largest known value is $N(3003)=8$, which comes from \[ 3003=\binom{3003}1=\binom{78}2=\binom{15}5=\binom{14}6 \] and the symmetry $\binom nm=\binom n{n-m}$. Singmaster~\cite{singmaster-2} showed that $N(t)\ge6$ for infinitely many $t$, using the solutions $n=F_{2j+2}F_{2j+3}-1$, $m=F_{2j}F_{2j+3}-1$ of $\binom{n+1}{m+1}=\binom n{m+2}$, where $F_i$ is the $i$-th Fibonacci number. De Weger~\cite{deweger} conjectured that every equality $\binom nm=\binom{n'}{m'}$ arises from either $m=0$, $m=1$, symmetry or Singmaster's infinite family, with 7 exceptional cases. Blokhuis, Brouwer and de Weger~\cite{bbw} verified this for $t\le10^{60}$. By symmetry it suffices to count solutions with $2m\le n$. For these, $t\ge\binom{2m}m\ge2^m$, so $m\le\log t/\log2$, and $n$ is determined by $m$ because $n\mapsto\binom nm$ is increasing. This gives Singmaster's bound $N(t)=O(\log t)$~\cite{singmaster}. It was improved to $O(\log t/\log\log t)$ by Abbott, Erd\H{o}s and Hanson~\cite{aeh}, to $O(\log t\,\log\log\log t/(\log\log t)^2)$ by Kane~\cite{kane-1}, and to $O(\log t\,\log\log\log t/(\log\log t)^3)$ by Kane~\cite{kane-2}. The last bound remains the best unconditional bound in the literature. Abbott, Erd\H{o}s and Hanson also observed that Cram\'er's conjecture~\cite{cramer} on gaps between consecutive primes implies $N(t)=O_\eps((\log t)^{2/3+\eps})$ for every $\eps>0$. Matom\"aki, Radziwi\l\l, Shao, Tao and Ter\"av\"ainen~\cite{mrstt} proved that for fixed $\eps>0$ and $t$ sufficiently large there are at most two solutions with $\exp((\log n)^{2/3+\eps})\le m\le n/2$ (Theorem~\ref{thm:mrstt} below). This reduces Conjecture~\ref{conj:singmaster} to solutions with $m<\exp((\log n)^{2/3+\eps})$, roughly those with $m\le\log t/(\log\log t)^{3/2-\eps}$~\cite[Remark~1.5]{mrstt}, but it gives no bound for the number of these solutions. Our main result is the following. \begin{theorem}\label{thm:main} For all sufficiently large $t$, \[ N(t)\le(\log t)^{\frac12+51\frac{\log\log\log\log t}{\log\log\log t}}. \] \end{theorem} Theorem~\ref{thm:main} follows from the next family of bounds by letting $k$ grow slowly with $t$. \begin{theorem}\label{thm:fixedk} For an integer $k\ge1$ put \[ a_0(k)=10\,(16k+12)^{2k+3/2}\,e^{10.75k+5.5}. \] There is an absolute constant $c_0$ such that for every integer $k\ge1$ and every integer $t$ with \[ \log\log\log t\ge\max\left\{c_0,\tfrac52\log\left(40(k+1)^2a_0(k)\right)\right\} \] we have \[ N(t)\le50\,e^{2a_0(k)+1}\,(\log t)^{\frac{k+1}{2k+1}}. \] \end{theorem} The cases $k=1$ and $k=2$ give $N(t)\ll(\log t)^{2/3}$ and $N(t)\ll(\log t)^{3/5}$. The constants are very large: $\log a_0(1)>30$, so the case $k=1$ applies only when $\log\log\log t>88$. All constants are explicit except $c_0$, which depends on the threshold in Theorem~\ref{thm:mrstt}; that threshold is effective~\cite[Remark~1.7]{mrstt} but has not been computed. \subsection{Formal verification} The proofs of Theorems~\ref{thm:main} and~\ref{thm:fixedk} have been formalised in the Lean~4 proof assistant~\cite{lean4} using Mathlib~\cite{mathlib}, conditional on the statement of Theorem~\ref{thm:mrstt}. The latter theorem, due to Matom\"aki, Radziwi\l\l, Shao, Tao, Ter\"av\"ainen, is included as a hypothesis and is not formalised here. The constants and inequalities in this paper match those of the formal proof, and Section~\ref{sec:lean} describes the correspondence between this paper and the formalisation. The source code is available at \url{https://github.com/benwh1/singmaster-bound}. \subsection{Strategy of proof} Fix $k\ge1$, write $L=\log t$, and put $\theta=\frac{k+1}{2k+1}$ and $\alpha=\frac k{k+1}$. It suffices to count solutions with $2m\le n$, and each of them is determined by $m$. There are at most $L^\theta$ of them with $m\le L^\theta$. If $m\ge L/(\log L)^{7/5}$, then $\log n\le2(\log L)^{7/5}$ while $\log m\ge\log L-\frac75\log\log L$, so $m\ge\exp((\log n)^{7/10})$ once $t$ is large, and Theorem~\ref{thm:mrstt} leaves at most two solutions. The main work concerns the range $L^\theta\le m\le L/(\log L)^{7/5}$. We cover a dyadic range $[M,2M]$ by windows $|m-x_0|\le r_M$ with $r_M=(M/2)^\alpha e^{-2a_0-1}$ and show that each window contains at most $L/M$ solutions (Lemma~\ref{lem:window}). This gives $O_k(LM^{-\alpha})$ solutions with $M\le m\le2M$, and summing over $M=2^iL^\theta$ gives $O_k(L^{1-\theta\alpha})=O_k(L^\theta)$, which is Theorem~\ref{thm:fixedk}. Taking $k\asymp\log\log\log t/\log\log\log\log t$ then gives Theorem~\ref{thm:main}. The window bound has three ingredients. Write $\ell=L/x_0$, so that $\log n\approx\ell$ for solutions with $m$ near $x_0$. From $n(n-1)\cdots(n-m+1)=t\cdot m!$ one expects $n\approx\frac{m-1}2+(t\,m!)^{1/m}$; compare~\cite[(3.1)]{kane-1} and~\cite[Remark~1.2]{mrstt}. In Section~\ref{sec:F} we construct a function $F$, holomorphic on the disc $|z-x_0|\le x_0/2$, such that $|F(m)-n|\le e^{-L/8}$ for every solution $(n,m)$ with $|m-x_0|\le x_0/2$, such that $|F|\le3x_0e^{2\ell}$, and such that in the variable $u=1/z$ \begin{equation}\label{eq:uform-outline} F(1/u)=u^{-1}\left(\frac{1-u}2+\frac{e^{Lu+\kappa(u)}}e\right), \end{equation} where $\kappa$ is holomorphic and nearly constant near $u_0=1/x_0$. Next let $d\ge0$ and $D=(k+1)(d+1)$, and take $D$ solutions $(n_i,m_i)$ in a window. The determinant $\det[(m_i-x_0)^an_i^b]$, with columns indexed by $0\le a\le d$ and $0\le b\le k$, is an integer. Replacing each $n_i$ by $F(m_i)$ changes it by at most $\frac12$, and the Schwarz lemma for interpolation determinants bounds the modified determinant by $e^{-1}$, provided the window radius is at most about $(x_0/2)^{k/(k+1)}e^{-2\ell/d}$. Hence the determinant vanishes, and all solutions in the window lie on one curve $\sum_bA_b(m)n^b=0$ with $\deg A_b\le d$ (Section~\ref{sec:det}). This is the determinant method of Bombieri and Pila~\cite{bp}. The exponent $k/(k+1)$ comes from comparing the saving $(r/R)^{D(D-1)/2}$ in the Schwarz lemma, where $R=x_0/2$, with the cost $R^{(k+1)d(d+1)/2}$ of the monomials $(m-x_0)^a$. To absorb the factor $e^{O(\ell)}$ that comes from the size of $F$ we need $d\gg\ell/a_0$, and we take $d=\lfloor L/(a_0M)\rfloor$. Finally, we show that such a curve passes through few points $(n,m)$ with $n\approx F(m)$ (Sections~\ref{sec:exppoly} and~\ref{sec:zero}). By~\eqref{eq:uform-outline}, \[ u^{d+k}\sum_bA_b(1/u)F(1/u)^b=\sum_{j=0}^kQ_j(u)E(u)^j,\qquad E(u)=e^{Lu+\kappa(u)}, \] where the $Q_j$ are polynomials of degree at most $d+k$. After the substitution $u=u_0+u_0s/a_0$, the function $E(u)^j$ becomes a constant multiple of $e^{jTs}K(s)^j$, where $T=L/(a_0x_0)\approx d$ and $K$ is close to $1$ on a disc of radius $a_0/2$. Truncating the Taylor series of $K^j$ at degree $\lceil2T\rceil$ produces an exponential polynomial $\sum_jR_j(s)e^{jTs}$ with $\sum_j(\deg R_j+1)\le(4k+3)T$. Lemma~\ref{lem:exppoly}, proved by Laplace inversion, bounds such an exponential polynomial and each of its components on $|s|\le5$ in terms of its maximum on $|s|\le\frac12$, and Jensen's formula then shows that it has at most $17(4k+3)T$ zeros near $0$. The solutions only give near-zeros, so we first subtract a Lagrange interpolation polynomial, which is small because the near-zeros are well separated. Since $T\le L/(a_0M)$ and $a_0\ge17(4k+3)$, each window contains at most $L/M$ solutions. The constant $a_0(k)$ is dictated by the last step: the truncation error $(10/a_0)^{2T}$ has to beat the factor $e^{O(kT\log k)}$ in Lemma~\ref{lem:exppoly}, which forces $\log a_0\asymp k\log k$; see~\eqref{eq:a0design}. The windows then have radius $(M/2)^\alpha e^{-2a_0-1}$, and this is the source of the factor $e^{2a_0+1}$ in Theorem~\ref{thm:fixedk}. \begin{remark}\label{rem:F} Fix a real $x>0$. The function $y\mapsto\Gamma(y+1)/\Gamma(y-x+1)$ is increasing on $[2x,\infty)$, since its logarithmic derivative $\psi(y+1)-\psi(y-x+1)$ is positive, where $\psi=\Gamma'/\Gamma$ is increasing; it also tends to infinity as $y\to\infty$. Hence, if $\Gamma(2x+1)\le t\,\Gamma(x+1)^2$, there is a unique real number $f(x)\ge2x$ with \[ \Gamma(f(x)+1)=t\,\Gamma(x+1)\,\Gamma(f(x)-x+1), \] that is, $\binom{f(x)}x=t$ with the binomial coefficient written in terms of the Gamma function. Let $(n,m)$ be a solution with $2m\le n$. Then $m\ge1$, since $t\ge2$, and $\binom{2m}m\le\binom nm=t$, so $f(m)$ is defined and $f(m)=n$. Kane~\cite{kane-1} continues $f$ holomorphically to a sector. This continuation is not suitable here. Suppose that $f$ has been continued to complex $z$, and write $c=f(z)-\frac{z-1}2$. Then $f(z)+1=c+\frac{z+1}2$ and $f(z)-z+1=c+\frac{1-z}2$, so the defining equation becomes $\Gamma(c+\frac{z+1}2)/\Gamma(c+\frac{1-z}2)=t\,\Gamma(z+1)$. Stirling's formula identifies the left side with $c^z$ only when $\arg c$ stays away from $\pm\pi$. Taking logarithms in $c^z\approx t\,\Gamma(z+1)$ shows that $\arg c$ is approximately $\Im\left((L+\log\Gamma(z+1))/z\right)$, and this ranges over an interval of length $\asymp\ell$ on the discs of radius $\asymp x_0$ that the determinant method requires. The function $F$ of Proposition~\ref{prop:F} interpolates $n$ only at the integers, and it depends on $c$ only through the powers $c^{-2j}$, so no branch of $\log c$ has to be chosen. \end{remark} \begin{remark}\label{rem:limits} The exponent $\frac12$ is the limit of the method. A window cannot be longer than the range $[M,2M]$ itself, and about $T\asymp L/(a_0M)$ points per window is the true order for the number of zeros of exponential polynomials of the above shape in a disc of bounded radius. The bound for the range $[M,2M]$ would therefore remain $\gg L/M$, and balancing $L/M_0$ against the trivial bound $M_0$ for $m\le M_0$ gives $M_0=L^{1/2}$. The growth $a_0(k)=e^{\Theta(k\log k)}$ comes from the factor $(4\nu/T)^\nu$ in Lemma~\ref{lem:exppoly}(b), that is, from Cauchy's estimates for the derivatives of an exponential polynomial at $0$. If this factor could be removed, $a_0(k)=e^{O(k)}$ would suffice, one could take $k\asymp\log\log\log t$, and the exponent in Theorem~\ref{thm:main} would become $\frac12+O(1/\log\log\log t)$. Finally, Proposition~\ref{prop:F} requires $\ell\ge100\log x_0$, roughly $\log n\ge100\log m$, so the argument does not reach solutions in which $n$ is bounded by a power of $m$; in our proof these are covered by Theorem~\ref{thm:mrstt}. \end{remark} \subsection{Notation}\label{sec:notation} We write $X\ll Y$ or $X=O(Y)$ for $|X|\le CY$ with an absolute constant $C$, and $X\asymp Y$ for $X\ll Y\ll X$; subscripts indicate dependence of $C$ on parameters. We use $\N=\{0,1,2,\dots\}$, write $\log$ for the natural logarithm and $\Log$ for the principal branch of the logarithm on $\C\setminus(-\infty,0]$, and write $\log\Gamma(z+1)$ for the branch that is holomorphic on $\Re z>-1$ and real on $(-1,\infty)$. For $\Re z>0$ we have $\Re\Log z=\log|z|$ and $\Log(1/z)=-\Log z$, and for $|z|\ge1$ we have $|\Log z|\le\log|z|+\pi$. We write $\disc(c,r)=\{z\in\C:|z-c|\le r\}$, and a function is holomorphic on a closed set if it is holomorphic on an open set containing it. The Bernoulli polynomials are defined by $\frac{we^{xw}}{e^w-1}=\sum_{p\ge0}B_p(x)\frac{w^p}{p!}$, and $B_p=B_p(0)$. For an integer $t\ge2$ we write $L=\log t$ and \[ \Sol(t)=\Big\{(n,m)\in\N^2:\binom nm=t,\ 2m\le n\Big\}. \] The map $(n,m)\mapsto(n,n-m)$ sends the solutions with $2m>n$ injectively into $\Sol(t)$, so \begin{equation}\label{eq:sym} N(t)\le2|\Sol(t)|. \end{equation} Every $(n,m)\in\Sol(t)$ has $m\ge1$, and $n\mapsto\binom nm$ is strictly increasing on $n\ge m$, so \begin{equation}\label{eq:inj} \text{an element $(n,m)$ of $\Sol(t)$ is determined by $m$.} \end{equation} Finally, $n(m-i)\le m(n-i)$ for $0\le i0$ and $|z|\ge1$, \[ |\log\Gamma(z+1)-\sigma(z)|\le\frac1{|z|}. \] \end{lemma} This follows from Binet's error bound~\cite[\S5.11(ii)]{dlmf}. \begin{lemma}\label{lem:bernoulli} \textup{(a)} For every integer $j\ge1$ the polynomial \[ P_{2j}(z)=\frac{B_{2j+1}\left(\frac{z+1}2\right)-B_{2j+1}\left(\frac{1-z}2\right)}{2j+1} \] satisfies $P_{2j}(m)=\sum_{i=0}^{m-1}\left(i-\frac{m-1}2\right)^{2j}$ for every $m\in\N$. \textup{(b)} If $p\in\N$, $y\in\C$ and $p\le\pi|y|$, then $|B_p(y)|\le8|y|^p$. \end{lemma} Part~(a) follows from $B_p(x+1)-B_p(x)=px^{p-1}$~\cite[\S24.4]{dlmf}. Part~(b) follows from $B_p(y)=\sum_i\binom piB_iy^{p-i}$ and $|B_i|\le4\,i!/(2\pi)^i$, which is a consequence of Euler's formula for $\zeta(2j)$~\cite[\S25.6]{dlmf}. \begin{theorem}[Matom\"aki, Radziwi\l\l, Shao, Tao, Ter\"av\"ainen~{\cite[Theorem~1.3]{mrstt}}]\label{thm:mrstt} Let $0<\eps<1$. There is $t_1(\eps)$ such that for every integer $t\ge t_1(\eps)$ there are at most two pairs $(n,m)\in\N^2$ with \[ \binom nm=t\qquad\text{and}\qquad\exp\left((\log n)^{2/3+\eps}\right)\le m\le n/2. \] \end{theorem} \section{The interpolating function}\label{sec:F} Throughout this section $t\ge2$ and $x_0\ge1$ are integers. We put \[ \ell=\frac L{x_0},\qquad u_0=\frac1{x_0},\qquad\Delta=\disc\left(x_0,\frac{x_0}2\right), \] \[ \qquad U=\disc\left(u_0,\frac{u_0}2\right),\qquad\eta_0=\frac{2(\log x_0+4)}{x_0}+2e^{-\ell/5}. \] \begin{proposition}\label{prop:F} Suppose that $x_0\ge e^{30}$ and $\ell\ge100\log x_0$. Then there are a function $F$ holomorphic on $\Delta$ and a function $\kappa$ holomorphic on $U$ with the following properties. \begin{enumerate} \item[(a)] $|F(m)-n|\le e^{-L/8}$ for every $(n,m)\in\Sol(t)$ with $|m-x_0|\le x_0/2$. \item[(b)] $|F(z)|\le3x_0e^{2\ell}$ for $z\in\Delta$. \item[(c)] $F(1/u)=u^{-1}\left(\frac{1-u}2+e^{Lu+\kappa(u)}/e\right)$ for every $u\in U$ with $1/u\in\Delta$. \item[(d)] $|\kappa(u)-\kappa(u_0)|\le\eta_0$ for $u\in U$, and $|\kappa(u_0)|\le1$. \end{enumerate} \end{proposition} \begin{proof} We start from an exact identity at the integers. Let $(n,m)\in\Sol(t)$ and put $c=n-\frac{m-1}2$, so that $c\ge m$. The numbers $n-i$ with $0\le i\frac{x_0}3,\ |z|<\frac{5x_0}2\Big\},\qquad a_j(z)=\frac{P_{2j}(z)\,e^{-2jg(z)}}{2j\,z}, \] \[ \qquad\Phi_z(w)=\sum_{j=1}^{N_0}a_j(z)e^{-2jw}. \] The open set $\Omega$ contains $\Delta$ and the image of $U$ under $u\mapsto1/u$, which is the disc with diameter $[2x_0/3,2x_0]$. Every $z\in\Omega$ satisfies $1\le|z|\le8\Re z$. The hypotheses imply $x_0\ge1000$, $\ell\ge3000$ and $q\le\min(\frac14,\frac1{x_0})$. By Lemma~\ref{lem:stirling}, for $\Re z>0$ and $|z|\ge1$, \begin{equation}\label{eq:Dbound} \Big|\frac{\log\Gamma(z+1)}z-\Log z+1\Big|\le\frac{1+\frac12(\log|z|+\pi)+\frac12\log(2\pi)}{|z|}, \end{equation} and the right side is at most $\frac12$ if $|z|\ge20$. On $\Omega$ we have $\Re(L/z)=L\Re z/|z|^2>\frac4{75}\ell\ge\ell/19$, and on $\Delta$ we have $\Re(L/z)\le L/|z|\le2\ell$. Since $\Re\Log z=\log|z|$, it follows that \begin{equation}\label{eq:reg} \Re g(z)\ge\frac\ell{19}+\log|z|-\frac32\quad(z\in\Omega),\qquad\Re g(z)\le2\ell+\log|z|-\frac12\quad(z\in\Delta). \end{equation} Let $z\in\Omega$ and $1\le j\le N_0$. Then $|(1\pm z)/2|>x_0/6-\frac12$ and $2j+1\le x_0/4+1\le\pi(x_0/6-\frac12)$, so Lemma~\ref{lem:bernoulli}(b) gives $|P_{2j}(z)|\le16|z|^{2j+1}$. Together with~\eqref{eq:reg} this gives $2je^{2j}|a_j(z)|\le16e^{5-2\ell/19}$, and since $N_0\le x_0\le e^{\ell/100}$, \[ \sum_{j=1}^{N_0}2j\,e^{2j}|a_j(z)|\le16N_0e^{5-2\ell/19}\le q. \] As $|\frac d{dw}e^{-2jw}|\le2je^{2j}$ for $|w|\le1$, each $\Phi_z$ maps $\disc(0,1)$ into $\disc(0,q)$ and is $q$-Lipschitz there. By the contraction mapping principle the iterates $v_0=0$, $v_{i+1}(z)=\Phi_z(v_i(z))$ converge uniformly on $\Omega$. Their limit $v$ is holomorphic on $\Omega$ and satisfies $v(z)=\Phi_z(v(z))$ and $|v|\le q$. Moreover, since $q\le\frac14$, \begin{equation}\label{eq:stab} |w-v(z)|\le2|w-\Phi_z(w)|\qquad(z\in\Omega,\ |w|\le1). \end{equation} We define \[ F(z)=\frac{z-1}2+e^{g(z)+v(z)},\qquad\mu(u)=u\log\Gamma(1/u+1)+\Log u+1,\qquad\kappa(u)=\mu(u)+v(1/u). \] Then $F$ is holomorphic on $\Omega\supseteq\Delta$, and $\kappa$ is holomorphic on $U$. To prove~(a), let $(n,m)\in\Sol(t)$ with $|m-x_0|\le x_0/2$, and let $c$, $\rho$ and $v^*$ be as in~\eqref{eq:exact}. Then $m\in\Omega$ and $0\le v^*\le\rho\le\frac14$. Since $e^{-2j(g(m)+v^*)}=c^{-2j}$, the number $\Phi_m(v^*)$ is the sum of the first $N_0$ terms of the series for $v^*$, so $0\le v^*-\Phi_m(v^*)\le\rho^{N_0+1}$, and~\eqref{eq:stab} gives $|v(m)-v^*|\le2\rho^{N_0+1}$. As $n-F(m)=c(1-e^{v(m)-v^*})$ and $\log c\ge g(m)\ge L/m$, we get \[ |n-F(m)|\le4c\rho^{N_0+1}\le m^{2N_0+2}c^{-(2N_0+1)}\le m^{2N_0+2}e^{-(2N_0+1)L/m}. \] Since $L/m\ge2\ell/3$, $2N_0+1\ge x_0/4-1$, $\log m\le\log x_0+\frac12$ and $x_0\log x_0\le L/100$, the right side is at most $e^{-L/8}$. For~(b), let $z\in\Delta$. By~\eqref{eq:reg} and $|v|\le\frac14$, \[ |F(z)|\le\frac{|z|+1}2+e^{2\ell+\log|z|-1/4}\le3x_0e^{2\ell}. \] For~(c), let $u\in U$ with $z=1/u\in\Delta$. Since $\Log u=-\Log z$ we have $g(z)=Lu+\mu(u)-\Log u-1$, so $e^{g(z)+v(z)}=u^{-1}e^{Lu+\kappa(u)}/e$, while $(z-1)/2=(1-u)/(2u)$. For~(d), let $u\in U$ and $z=1/u$. Then $\mu(u)=\log\Gamma(z+1)/z-\Log z+1$ and $2x_0/3\le|z|\le2x_0$, so~\eqref{eq:Dbound} gives $|\mu(u)|\le(9+\frac34\log x_0)/x_0$. Since $|v|\le q\le1/x_0$ and $\log x_0\ge30$, it follows that \[ |\kappa(u)-\kappa(u_0)|\le|\mu(u)|+|\mu(u_0)|+2q\le\frac{20+1.5\log x_0}{x_0}\le\eta_0 \] and $|\kappa(u_0)|\le|\mu(u_0)|+q\le1$. \end{proof} \section{Solutions in a short window lie on a curve}\label{sec:det} \begin{proposition}\label{prop:det} Let $k\ge1$, $d\ge0$ and $x_0\ge2$ be integers, and let $\ell\ge0$. Put $D=(k+1)(d+1)$, $R=x_0/2$, $B_F=3x_0e^{2\ell}$, \[ r=R^{k/(k+1)}\exp\left(-\frac{2\ell+\log(3x_0)+2\log D+1}{d+1}\right), \] \[ \delta_3=\left(2\cdot D!\cdot D\cdot k\cdot R^{dD}(B_F+1)^{kD}\right)^{-1}. \] Let $F$ be holomorphic on $\disc(x_0,R)$ with $|F|\le B_F$ there, let $0\le\delta\le\delta_3$, and let $\mathcal T$ be a finite set of pairs of integers $(n,m)$ with $|m-x_0|\le r$ and $|F(m)-n|\le\delta$. Then there are polynomials $A_0,\dots,A_k\in\C[X]$ of degree at most $d$, not all zero, such that \[ \sum_{b=0}^kA_b(m)\,n^b=0\qquad\text{for every }(n,m)\in\mathcal T. \] \end{proposition} Note that the relation holds for the integers $n$ themselves and not only for their approximations $F(m)$. \begin{proof} Consider the integer matrix with rows indexed by $\mathcal T$, columns indexed by the pairs $(a,b)$ with $0\le a\le d$ and $0\le b\le k$, and entries $(m-x_0)^an^b$. It suffices to show that every $D\times D$ matrix formed from $D$ of its rows, repetitions allowed, has determinant $0$. The matrix then has rank less than $D$, so it has a nonzero kernel vector $(c_{a,b})$, and $A_b(X)=\sum_ac_{a,b}(X-x_0)^a$ has the required properties. Fix rows $(n_1,m_1),\dots,(n_D,m_D)$, and let $\Delta_0=\det[(m_i-x_0)^an_i^b]$ and $\widetilde\Delta_0=\det[(m_i-x_0)^aF(m_i)^b]$. We apply the Schwarz lemma for interpolation determinants (see, e.g., \cite{laurent,waldschmidt}) on $\disc(x_0,R)$ to the functions $(z-x_0)^aF(z)^b$, which are bounded by $R^aB_F^b$ there; note that $r\le R$. With \[ W=\frac{D(D-1)}2,\qquad S_a=\sum_{(a,b)}a=\frac{(k+1)d(d+1)}2, \] \[ S_b=\sum_{(a,b)}b=\frac{(d+1)k(k+1)}2,\qquad\Lambda=\log B_F, \] this gives, since $\log D!\le D\log D$, \[ \log|\widetilde\Delta_0|\le D\log D-W\log\frac Rr+S_a\log R+S_b\Lambda . \] Write $\log r=\frac k{k+1}\log R-\xi$ with $\xi=(\Lambda+2\log D+1)/(d+1)$. A direct computation gives $\frac W{k+1}-S_a=\frac{k(d+1)}2\ge0$, so the terms involving $\log R$ contribute at most $0$. Moreover $W\xi=\frac{(k+1)(D-1)}2(\Lambda+2\log D+1)$, and $D-1\ge k(d+1)$, so $W\xi\ge S_b\Lambda+(D-1)(2\log D+1)$. Hence \[ \log|\widetilde\Delta_0|\le D\log D-(D-1)(2\log D+1)\le-1, \] as $D\ge2$. Since $\delta\le1$ we have $|n_i|\le B_F+1$. The entries of both matrices are therefore bounded by $R^d(B_F+1)^k$, and corresponding entries differ by at most $R^dk(B_F+1)^{k-1}\delta$. Expanding both determinants by the Leibniz formula gives \[ |\Delta_0-\widetilde\Delta_0|\le D!\cdot D\cdot k\cdot R^{dD}(B_F+1)^{kD}\delta=\frac\delta{2\delta_3}\le\frac12 . \] Hence $|\Delta_0|\le e^{-1}+\frac12<1$, and since $\Delta_0\in\Z$, it vanishes. \end{proof} \section{Growth of exponential polynomials}\label{sec:exppoly} \begin{lemma}\label{lem:exppoly} Let $k\ge1$ be an integer and $T>0$. Let $\nu_0,\dots,\nu_k\ge1$ be integers, and put $\nu=\sum_j\nu_j$ and $\nu_{\max}=\max_j\nu_j$. Let $G_0(s)=\sum_{j=0}^kR_j(s)e^{jTs}$ with $R_j\in\C[s]$ and $\deg R_j<\nu_j$, and let $m_0\ge\max_{|s|\le1/2}|G_0(s)|$. Put \[ \varrho=\max(2kT,2\nu),\qquad C_a=\nu\,3^\nu e^{5\varrho}, \] \[ C_b=2\nu\left((k+1)2^{4k+2}\right)^{\nu_{\max}}e^{(4k+2)T}\max\left(1,(4\nu/T)^\nu\right). \] Then \begin{enumerate} \item[(a)] $|G_0(s)|\le C_a\,m_0$ for $|s|\le5$; \item[(b)] $|R_j(s)e^{jTs}|\le C_b\,m_0$ for $|s|\le4$ and $0\le j\le k$. \end{enumerate} \end{lemma} \begin{proof} Let $\chi(w)=\prod_{h=0}^k(w-hT)^{\nu_h}=\sum_{l=0}^\nu a_lw^l$, and for $0\le i<\nu$ let $\chi_i(w)=\sum_{l>i}a_lw^{l-i-1}$ and $y_i=G_0^{(i)}(0)$. The function $G_0$ satisfies the differential equation \[ \chi\left(\frac d{ds}\right)G_0=0, \] and integration by parts shows that its Laplace transform is \[ Y(w)=\sum_{i<\nu}\frac{y_i\,\chi_i(w)}{\chi(w)}. \] Writing $R_j(s)=\sum_pr_{jp}s^p$, the same computation identifies $Y(w)$ with $\sum_j\sum_pr_{jp}\,p!\,(w-jT)^{-p-1}$, so Cauchy's integral formula gives \begin{equation}\label{eq:inversion} G_0(s)=\frac1{2\pi i}\oint_{|w|=\varrho}e^{sw}Y(w)\,dw,\qquad R_j(s)e^{jTs}=\frac1{2\pi i}\oint_{|w-jT|=T/2}e^{sw}Y(w)\,dw, \end{equation} since all poles $hT$ of $Y$ lie inside the first circle and only $jT$ lies inside the second. By Cauchy's estimates on $|s|=\frac12$ we have $|y_i|\le i!\,2^im_0$. On $|w|=\varrho$ we have $|w-hT|\ge\varrho/2$, so $|\chi(w)|\ge(\varrho/2)^\nu$. The coefficients of $\chi$ are dominated by those of $(w+kT)^\nu$, so $|\chi_i(w)|\le\varrho^{-i-1}(3\varrho/2)^\nu$ and hence $|\chi_i/\chi|\le3^\nu\varrho^{-i-1}$. Using~\eqref{eq:inversion} and $|e^{sw}|\le e^{5\varrho}$, we obtain \[ |G_0(s)|\le3^\nu e^{5\varrho}m_0\sum_{i<\nu}i!\left(\frac2\varrho\right)^i\le\nu\,3^\nu e^{5\varrho}m_0, \] because $i!(2/\varrho)^i\le i!/\nu^i\le1$. This proves~(a). For~(b), fix $j$ and let $C_j$ be the circle $|w-jT|=T/2$. On $C_j$ we have $T/2\le|w|\le(k+\frac12)T$, so $|e^{sw}|\le e^{(4k+2)T}$ for $|s|\le4$, and $|w-hT|\ge\max(|h-j|-\frac12,\frac12)T$ for every $h$. Write $w^{i+1}\chi_i(w)=\chi(w)-\sum_{l\le i}a_lw^l$. The coefficients of $\chi$ are dominated by those of $\prod_h(w+hT)^{\nu_h}$, so on $C_j$ \[ \frac{|\sum_{l\le i}a_lw^l|}{|\chi(w)|}\le\prod_{h=0}^k\rho_h^{\nu_h}\le\left(\prod_{h=0}^k\rho_h\right)^{\nu_{\max}},\qquad\rho_h=\frac{h+j+\frac12}{\max(|h-j|-\frac12,\frac12)}\ge1 . \] Since $\max(r-\frac12,\frac12)\ge r/2$ for every integer $r\ge1$, \[ \prod_h\rho_h\le\frac{2^{k+1}(k+j+1)!}{j!\,j!\,(k-j)!}=2^{k+1}(k+1)\binom{k+j+1}j\binom kj\le(k+1)2^{4k+2}. \] With $\Xi=((k+1)2^{4k+2})^{\nu_{\max}}$ this gives $|\chi_i/\chi|\le|w|^{-i-1}(1+\Xi)\le2\Xi(2/T)^{i+1}$ on $C_j$, and by~\eqref{eq:inversion} \[ |R_j(s)e^{jTs}|\le2\Xi e^{(4k+2)T}m_0\sum_{i<\nu}i!\left(\frac4T\right)^i\le C_bm_0, \] because $i!(4/T)^i\le(4\nu/T)^i\le\max(1,(4\nu/T)^\nu)$ for $i<\nu$. \end{proof} \section{A zero estimate}\label{sec:zero} \begin{proposition}\label{prop:zero} Let $k\ge1$ and $d\ge0$ be integers, and let $L>0$, $x_0\ge1$ and $\eta\ge0$ be real numbers. Let $a_0=a_0(k)$, $u_0=1/x_0$, $\Delta=\disc(x_0,x_0/2)$ and $U=\disc(u_0,u_0/2)$, and put \[ T=\frac L{a_0x_0},\qquad\delta_5=\exp\left(-1000(k+1)^2(T+1)\log(6x_0+6)\right). \] Suppose that $T\ge10(k+1)^2$, $d\le2T$ and $k\eta\le0.09$. Let $\kappa$ be holomorphic on $U$ with $|\kappa(u)-\kappa(u_0)|\le\eta$ for $u\in U$ and $|\kappa(u_0)|\le1$, and let $F:\Delta\to\C$ satisfy $F(1/u)=u^{-1}\left(\frac{1-u}2+e^{Lu+\kappa(u)}/e\right)$ whenever $u\in U$ and $1/u\in\Delta$. Let $A_0,\dots,A_k\in\C[X]$ be polynomials of degree at most $d$, not all zero, and let $0\le\delta\le\delta_5$. Let $Z\subseteq\disc(x_0,x_0/(4a_0))$ be a finite set of points at mutual distance at least $1$ such that every $z\in Z$ admits some $w_z\in\C$ with \[ \sum_{b=0}^kA_b(z)w_z^b=0\qquad\text{and}\qquad|F(z)-w_z|\le\delta . \] Then $|Z|\le17(4k+3)T$. \end{proposition} \begin{proof} Put $\hat A_b(u)=u^dA_b(1/u)$ and \[ Q_j(u)=e^{-j}\sum_{b=j}^k\binom bj\,u^{k-b}\left(\frac{1-u}2\right)^{b-j}\hat A_b(u)\qquad(0\le j\le k). \] These are polynomials of degree at most $d+k$, and the binomial theorem gives, for $u\ne0$ and $Y\in\C$, \begin{equation}\label{eq:cv} u^{d+k}\sum_{b=0}^kA_b(1/u)\left(u^{-1}\left(\frac{1-u}2+\frac Ye\right)\right)^b=\sum_{j=0}^kQ_j(u)Y^j . \end{equation} If $b^*$ is the largest $b$ with $A_b\ne0$, then $Q_{b^*}=e^{-b^*}u^{k-b^*}\hat A_{b^*}\ne0$. We now rescale. Put $h=u_0/a_0$ and $u(s)=u_0+hs$, so that $T=Lh$ and $u(s)\in U$ for $|s|\le a_0/2$. Let \[ E(u)=e^{Lu+\kappa(u)},\qquad K(s)=e^{\kappa(u(s))-\kappa(u_0)},\qquad q_j(s)=e^{j(Lu_0+\kappa(u_0))}Q_j(u(s)). \] Then $\deg q_j\le d+k$, and the function \begin{equation}\label{eq:G} G(s)=\sum_{j=0}^kQ_j(u(s))E(u(s))^j=\sum_{j=0}^kq_j(s)e^{jTs}K(s)^j \end{equation} is holomorphic on $|s|0$. The same inequalities give $4k\nu\le e^T$, $((k+1)2^{4k+2})^{\nu_{\max}}\le e^{(17.5k+7)T}$ and $(4\nu/T)^\nu\le(16k+12)^{(4k+3)T}$, hence \begin{equation}\label{eq:Cb} C_b\le2kC_b\le\exp\left((21.5k+10)T+(4k+3)T\log(16k+12)\right). \end{equation} By the definition of $a_0$, \begin{equation}\label{eq:a0design} \log(a_0/10)=(2k+\tfrac32)\log(16k+12)+10.75k+5.5, \end{equation} and since $J+1\ge2T$, we deduce from~\eqref{eq:Cb} that $2kC_b\delta'\le e^{-T}\le\frac12$. By Lemma~\ref{lem:exppoly}(b) and~\eqref{eq:trunc}, $|q_je^{jTs}|=|R_je^{jTs}|/|\Pi_j|\le2C_bm_0$ on $\disc(0,4)$, and therefore \begin{equation}\label{eq:GG0} |G-G_0|=\Big|\sum_{j=1}^kq_je^{jTs}(K^j-\Pi_j)\Big|\le2kC_b\delta'm_0\le\frac{m_0}2\qquad\text{on }\disc(0,4). \end{equation} The points of $Z$ give near-zeros of $G$: we claim that \begin{equation}\label{eq:nearzero} |G(s_z)|\le\gamma:=2.2\,(k+1)\,3^k\cdot2e^3\,C_b\,m_0\,\delta\qquad(z\in Z). \end{equation} Let $z\in Z$, $u=1/z$ and $E=E(u)$, and define $Y'$ by $w_z=u^{-1}(\frac{1-u}2+Y'/e)$. By~\eqref{eq:cv} with $Y=Y'$ we have $\sum_jQ_j(u)Y'^j=u^{d+k}\sum_bA_b(z)w_z^b=0$, while $G(s_z)=\sum_jQ_j(u)E^j$ by~\eqref{eq:G}. Hence $G(s_z)=\sum_jQ_j(u)E^j\left(1-(Y'/E)^j\right)$. By hypothesis $F(z)=u^{-1}(\frac{1-u}2+E/e)$, so $E-Y'=eu(F(z)-w_z)$. Since $|u|\le2$ and $|E|\ge e^{-2}$, this gives $|Y'/E-1|\le2e^3\delta\le1$, and so $|1-(Y'/E)^j|\le3^j\cdot2e^3\delta$. Finally, $Q_j(u)E^j=q_j(s_z)e^{jTs_z}K(s_z)^j$ has absolute value at most $2.2\,C_bm_0$, because $|K^j|\le1.1$. Summing over $j$ gives~\eqref{eq:nearzero}. Suppose now that $|Z|>17(4k+3)T$. Let $N_1=\lfloor17(4k+3)T\rfloor+1$, choose $Z'\subseteq Z$ with $N_1$ elements, and let $\Lag$ be the Lagrange interpolation polynomial of $G$ at the points $s_z$, $z\in Z'$, which are distinct by~\eqref{eq:sep}. For $|s|\le4$ each factor $(s-s_{z'})/(s_z-s_{z'})$ in $\Lag$ has absolute value at most $\frac{13}3\cdot\frac{x_0}5\le x_0$, so $|\Lag|\le N_1\gamma x_0^{N_1}$ on $\disc(0,4)$ by~\eqref{eq:nearzero}. A short computation using~\eqref{eq:Cb}, $\delta\le\delta_5$, $N_1\le17(4k+3)T+1$ and $T\ge10(k+1)^2$ shows that $4N_1\gamma x_0^{N_1}\le m_0$, so that \begin{equation}\label{eq:Lsmall} |\Lag|\le\frac{m_0}4\qquad\text{on }\disc(0,4). \end{equation} Choose $s_*$ with $|s_*|\le\frac12$ and $|G_0(s_*)|=m_0$, and let $f=G-\Lag$. By~\eqref{eq:GG0} and~\eqref{eq:Lsmall}, $|f-G_0|\le\frac34m_0$ on $\disc(0,4)$. Hence $|f(s_*)|\ge\frac14m_0$, and by Lemma~\ref{lem:exppoly}(a), $|f|\le(C_a+\frac34)m_0$ on the circle $|s-s_*|=3$. The function $f$ vanishes at the $N_1$ points $s_z$ with $z\in Z'$, which lie in $\disc(0,\frac13)\subseteq\disc(s_*,\frac32)$. By Jensen's formula, \[ N_1\log2\le\log(4C_a+3). \] Since $C_a=\nu\,3^\nu e^{10\nu}$ and $\nu\ge80$, the right side is at most $17\nu\log2$. Hence $N_1\le17\nu\le17(4k+3)T0$, $a_0=a_0(k)$, and \[ \theta=\frac{k+1}{2k+1},\qquad\alpha=\frac k{k+1}, \] \[ M_0=L^\theta,\qquad M_1=\frac L{(\log L)^{7/5}},\qquad r_M=\left(\frac M2\right)^\alpha e^{-2a_0-1}. \] The main hypothesis on $k$ and $t$ is \begin{equation}\label{eq:SA} 40(k+1)^2a_0\le(\log L)^{2/5}. \end{equation} Since $(k+1)^2\ge4$, it implies $k+1\le(\log L)^{1/5}$ and $160a_0\le(\log L)^{2/5}$. \begin{lemma}\label{lem:large} There is an absolute constant $\Lambda_1$ such that, if $\log L\ge\Lambda_1$, then \[ \#\{(n,m)\in\Sol(t):m\ge M_1\}\le2. \] \end{lemma} \begin{proof} Let $(n,m)\in\Sol(t)$ with $m\ge M_1$. By~\eqref{eq:binlow} and $n\ge2m$ we have $m\log2\le m(\log n-\log m)\le L$, so $\log m\le\log L+\log2$ and $\log n\le\log m+L/m\le2(\log L)^{7/5}$. On the other hand $\log m\ge\log L-\frac75\log\log L$. Hence $(\log n)^{7/10}\le2(\log L)^{49/50}\le\log m$ once $\log L$ is large, that is, $m\ge\exp((\log n)^{2/3+1/30})$. Since also $m\le n/2$, Theorem~\ref{thm:mrstt} with $\eps=1/30$ gives the claim as soon as $t\ge t_1(1/30)$. \end{proof} \begin{lemma}\label{lem:window} Assume that $\log L\ge2\cdot10^7$ and that~\eqref{eq:SA} holds. Let $M\in[M_0,M_1]$, and let $x_0\in[M,2M]$ be an integer. Then \[ \#\{(n,m)\in\Sol(t):|m-x_0|\le r_M\}\le\frac LM . \] \end{lemma} \begin{proof} Let $\mathcal T$ be the set on the left, and put \[ \ell=\frac L{x_0},\qquad\beta=\frac LM,\qquad d=\Big\lfloor\frac L{a_0M}\Big\rfloor,\qquad D=(k+1)(d+1),\qquad T=\frac L{a_0x_0}. \] Since $\theta\ge\frac12$ we have $L^{1/2}\le M_0\le M\le x_0\le2M\le2L$, so $\log x_0\le\log L+\log2$. Also $\ell\ge L/(2M_1)=(\log L)^{7/5}/2$ and $\beta\ge(\log L)^{7/5}$. We first check that Proposition~\ref{prop:F} applies. We have $x_0\ge L^{1/2}\ge e^{30}$, and since $(\log L)^{2/5}\ge400$, \[ \ell\ge\tfrac12(\log L)^{7/5}\ge200\log L\ge100\log x_0 . \] Let $F$ and $\kappa$ be the functions given by Proposition~\ref{prop:F}. Next we check the hypotheses of Proposition~\ref{prop:zero} on the parameters. Since $x_0\in[M,2M]$ we have $T\le L/(a_0M)\le2T$, so $d\le2T$ and $d+1>L/(a_0M)$. By~\eqref{eq:SA}, $L/(a_0M)\ge(\log L)^{7/5}/a_0\ge40(k+1)^2\log L$, so $T\ge10(k+1)^2$ and $d+1>40(k+1)^2\log L$. Since $x_0\ge L^{1/2}$ and $\ell\ge\frac12\log L$, we have $\eta_0\le12L^{-1/4}+2L^{-1/10}$, and with $k\le(\log L)^{1/5}$ this gives $k\eta_0\le0.09$. We now compare radii. Since $(M/2)^\alpha\le x_0/2$ and $2a_0e^{-2a_0-1}\le1$, we have $r_M\le x_0/(4a_0)\le x_0/2$. Let $r$ be the radius of Proposition~\ref{prop:det} for $(x_0,k,d,\ell)$. Since $(M/2)^\alpha\le(x_0/2)^\alpha$, the inequality $r_M\le r$ follows from \[ 2\ell+\log(3x_0)+2\log D+1\le(2a_0+1)(d+1), \] which holds because $\ell\le\beta40(k+1)^2\log L$. Next we show that the tolerances of Propositions~\ref{prop:det} and~\ref{prop:zero} exceed $e^{-L/8}$. We first note that \begin{equation}\label{eq:MLbound} 16000(k+1)^2(19+4\log M)\le\frac{M^2}L . \end{equation} Indeed, the left side is at most $368000(\log L)^{7/5}$, which is at most $\exp(\frac12(\log L)^{4/5})$ since $\log L\ge2\cdot10^7$, while $M^2/L\ge L^{2\theta-1}=L^{1/(2k+1)}\ge\exp(\frac12(\log L)^{4/5})$ since $2k+1<2(\log L)^{1/5}$. Let $\delta_3$ be as in Proposition~\ref{prop:det} for $(x_0,k,d,\ell)$ with $B_F=3x_0e^{2\ell}$. Using $D!\le e^{D^2}$, $B_F+1\le8Me^{2\beta}$, $d\le\beta$ and $D\le2(k+1)\beta$, we find \[ \log\frac1{\delta_3}\le(k+1)^2\beta^2(19+4\log M)\le\frac{\beta^2M^2}{16000L}\le\frac L8 \] by~\eqref{eq:MLbound}. Let $\delta_5$ be as in Proposition~\ref{prop:zero}. Since $T+1\le2\beta$ and $\log(6x_0+6)\le3+\log M$, and since $16000(k+1)^2(3+\log M)\le M^2/L\le M$ by~\eqref{eq:MLbound}, we have \[ \log\frac1{\delta_5}\le2000(k+1)^2\beta(3+\log M)\le\frac{\beta M}8=\frac L8 . \] Every $(n,m)\in\mathcal T$ satisfies $|m-x_0|\le r_M\le x_0/2$, so $|F(m)-n|\le e^{-L/8}$ by Proposition~\ref{prop:F}(a). If $|\mathcal T|1.0974$. Since $k\le y\le s/100$ we have $k+2\le s$, so $k\log(k+2)\le y\log s=s/100$. By~\eqref{eq:a0bound}, \[ \tfrac52\log\left(40(k+1)^2a_0\right)\le\tfrac52\cdot37.5\cdot\frac s{100}\le s, \] and Theorem~\ref{thm:fixedk} gives $N(t)\le50e^{2a_0+1}L^\theta$ with $\theta=\frac{k+1}{2k+1}$. Since $y0$, takes the value $\log m!$ at every $m\in\N$, and satisfies the bound of Lemma~\ref{lem:stirling}. The table lists the Lean declarations corresponding to the results of this paper. All names are in the namespace \lean{Singmaster}. \begin{center} \footnotesize \begin{tabular}{@{}p{0.36\textwidth}p{0.58\textwidth}@{}} \toprule Result&Lean declaration\\ \midrule Theorem~\ref{thm:main}&\lean{MainBound}, \lean{mainBound\_of\_fixedKBound}, \lean{main\_pointwise}\\ Theorem~\ref{thm:fixedk}&\lean{FixedKBound}, \lean{fixedKBound\_of\_mrstt}\\ \eqref{eq:sym}&\lean{N\_le\_two\_mul\_card\_halfSolutions}\\ Lemma~\ref{lem:stirling}&\lean{StirlingFormula}, \lean{stirlingFormula}\\ Lemma~\ref{lem:bernoulli}&\lean{powSumPoly\_eval\_nat}, \lean{bernC\_eval\_norm\_le}\\ Theorem~\ref{thm:mrstt}&\lean{MRSTT} (a hypothesis)\\ Proposition~\ref{prop:F}&\lean{InterpolatingFunction}, \lean{interpolatingFunction}\\ Contraction mapping step in Proposition~\ref{prop:F}&\lean{analytic\_fixed\_point}\\ Proposition~\ref{prop:det}&\lean{solutions\_on\_curve}\\ Schwarz lemma in Proposition~\ref{prop:det}&\lean{interpolation\_det\_le}\\ Lemma~\ref{lem:exppoly}&\lean{expPoly\_bound}\\ Proposition~\ref{prop:zero}&\lean{zero\_estimate}\\ \eqref{eq:trunc}&\lean{taylor\_trunc}\\ Jensen's formula in Proposition~\ref{prop:zero}&\lean{card\_zeros\_le\_of\_jensen}\\ Lemma~\ref{lem:large}&\lean{card\_halfSolutions\_large\_le}\\ Lemma~\ref{lem:window}&\lean{ct\_window}, \lean{ct\_delta3}, \lean{ct\_delta5}\\ Proof of Theorem~\ref{thm:fixedk}&\lean{ct\_block}, \lean{ct\_middle}, \lean{ct\_final}\\ \eqref{eq:a0bound}&\lean{log\_a$_0$\_bound}\\ \bottomrule \end{tabular} \end{center} \section{Acknowledgements}\label{sec:ack} All of the proofs presented in this paper, their Lean~4 formalisations, and most of the text content of this paper were generated by Claude Opus 5.5. \begin{thebibliography}{10} \bibitem{aeh} H.~L. Abbott, P.~Erd\H{o}s, and D.~Hanson. \newblock On the number of times an integer occurs as a binomial coefficient. \newblock {\em Amer. Math. Monthly}, 81:256--261, 1974. \bibitem{bbw} Aart Blokhuis, Andries Brouwer, and Benne de~Weger. \newblock Binomial collisions and near collisions. \newblock {\em Integers}, 17:Paper No. A64, 8, 2017. \bibitem{bp} E.~Bombieri and J.~Pila. \newblock The number of integral points on arcs and ovals. \newblock {\em Duke Math. J.}, 59(2):337--357, 1989. \bibitem{cramer} Harald Cram\'er. \newblock On the order of magnitude of the difference between consecutive prime numbers. \newblock {\em Acta Arith.}, 2:23--46, 1936. \bibitem{deweger} Benjamin M.~M. de~Weger. \newblock Equal binomial coefficients: some elementary considerations. \newblock {\em J. Number Theory}, 63(2):373--386, 1997. \bibitem{lean4} Leonardo de~Moura and Sebastian Ullrich. \newblock The {L}ean 4 theorem prover and programming language. \newblock In {\em Automated Deduction -- CADE 28}, volume 12699 of {\em Lecture Notes in Comput. Sci.}, pages 625--635. Springer, Cham, 2021. \bibitem{dlmf} F.~W.~J. Olver, A.~B. Olde~Daalhuis, D.~W. Lozier, B.~I. Schneider, R.~F. Boisvert, C.~W. Clark, B.~R. Miller, B.~V. Saunders, H.~S. Cohl, and M.~A. McClain, editors. \newblock {\em NIST Digital Library of Mathematical Functions}. \newblock \url{https://dlmf.nist.gov/}. \bibitem{kane-1} Daniel Kane. \newblock New bounds on the number of representations of {$T$} as a binomial coefficient. \newblock {\em Integers}, 4:A7, 10, 2004. \bibitem{kane-2} Daniel~M. Kane. \newblock Improved bounds on the number of ways of expressing {$t$} as a binomial coefficient. \newblock {\em Integers}, 7:A53, 7, 2007. \bibitem{laurent} Michel Laurent. \newblock Sur quelques r\'esultats r\'ecents de transcendance. \newblock {\em Ast\'erisque}, 198-200:209--230, 1991. \bibitem{mathlib} The mathlib Community. \newblock The {L}ean mathematical library. \newblock In {\em Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020)}, pages 367--381. ACM, New York, 2020. \bibitem{mrstt} Kaisa Matom\"{a}ki, Maksym Radziwi{\l\l}, Xuancheng Shao, Terence Tao, and Joni Ter\"{a}v\"{a}inen. \newblock Singmaster's conjecture in the interior of {P}ascal's triangle. \newblock {\em Q. J. Math.}, 73(3):1137--1177, 2022. \bibitem{waldschmidt} Michel Waldschmidt. \newblock {\em Diophantine approximation on linear algebraic groups}, volume 326 of {\em Grundlehren der Mathematischen Wissenschaften}. \newblock Springer-Verlag, Berlin, 2000. \bibitem{singmaster} David Singmaster. \newblock Research {P}roblems: {H}ow {O}ften {D}oes an {I}nteger {O}ccur as a {B}inomial {C}oefficient? \newblock {\em Amer. Math. Monthly}, 78(4):385--386, 1971. \bibitem{singmaster-2} David Singmaster. \newblock Repeated binomial coefficients and {F}ibonacci numbers. \newblock {\em Fibonacci Quart.}, 13(4):295--298, 1975. \end{thebibliography} \end{document}