Small positive integer-polynomial values at ζ(5)

Open

Apery.main_estimate

by tomasz · Oct 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

formalizationirrationalitynumber-theoryzeta5-mo271

There exists a real constant $c>0$ such that every sufficiently large natural number $n$ admits an integer polynomial $Q_n$ satisfying

Q_n=c'_nF_n\quad\text{for some }c'_n\in\mathbb Q_{>0},\qquad\deg Q_n=37n,

and

0<Q_n(z_5)<e^{-cn^2}.

The scalar-multiple equality is equality of polynomials after mapping integer coefficients to rational coefficients. The constant $c$ is independent of $n$ . This is the exact strength of the repository's main estimate: existence of a positive decay rate, without requiring the paper's rate $139/5$ .

Preamble

import Mathlib
import Definitions.Def_Zeta5_SourceConstruction
import Definitions.Def_Zeta5_SourceConstants
import Definitions.Def_Zeta5_SourceValue

open Polynomial Filter Topology MeasureTheory

Formal statement

namespace Apery

theorem main_estimate :
    ∃ c : ℝ, 0 < c ∧ ∀ᶠ n in atTop, ∃ Q : ℤ[X],
      (∃ c' : ℚ, 0 < c' ∧ Q.map (Int.castRingHom ℚ) = C c' * F n) ∧
      Q.natDegree = 37 * n ∧
      0 < aeval zeta5 Q ∧ aeval zeta5 Q < Real.exp (-c * (n : ℝ) ^ 2) := by sorry

end Apery

Source

https://github.com/mo271/Zeta5/blob/7fe736760f4b96bfdb4334b68e3b3124ecbe10b0/Apery/MainEstimate.lean#L64-L98

Read-back

What the Lean code literally says, in plain math · GPT-6 (Codex independent auditor)

There exist a real number $c>0$ and a natural-number threshold $N$ such that, for every natural number $n\ge N$ , there is a polynomial $Q\in\mathbb Z[x]$ for which there exists a positive rational number $a$ with the coefficientwise image of $Q$ in $\mathbb Q[x]$ exactly equal to $aF_n(x)$ , the natural degree of $Q$ is exactly $37n$ , and

0<Q(Z)<\exp(-cn^2).

Polynomial evaluation embeds the integer coefficients in $\mathbb R$ , and $n$ is embedded in $\mathbb R$ in the exponential. The number $c$ is fixed for all these indices; $Q$ and the positive rational multiplier $a$ may depend on $n$ . Natural degree is ordinary degree for a nonzero polynomial and is defined to be $0$ for the zero polynomial, which the strict evaluation inequality excludes. The real number $Z$ is $\sum_{k\in\mathbb N}1/k^5$ , with the natural numbers embedded in $\mathbb R$ and the $k=0$ summand equal to $0$ by total division. Infinite sums mean unconditional sums, assigned $0$ if no such sum exists. The rational polynomial in this assertion is $F_n(x)=s_n\det\bigl[M_{40n}(D_{3n}(t)^6t^{i+j};x)\bigr]_{0\le i,j<37n}$ . Put $r_n=\max(37n-1,0)$ , the truncated natural-number subtraction used in the code, and $s_n=\frac{((40n)!)^{2(37n)}4^{r_n}}{((3n)!)^{12(37n)}\prod_{i=1}^{r_n}((2i)!)^2}\in\mathbb Q$ . Here $D_m(t)=\prod_{r=1}^{m}(t+r^2)$ for $m\in\mathbb N$ , $H_j=\sum_{v=1}^{j}v^{-5}$ for $j\in\mathbb N$ , and $\beta_e=(-1)^eB_{2e+2}(2e+3)(2e+4)(2e+5)/24$ for $e\in\mathbb N$ , where $B_k$ are the rational Bernoulli numbers with $B_1=-1/2$ . For $K\in\mathbb N$ and $P\in\mathbb Q[t]$ , let $q_{K,P}$ be the polynomial quotient on division of $P$ by the monic polynomial $D_K$ , and put

\begin{aligned} M_K(P;x)&=\sum_e [t^e]q_{K,P}\,\beta_e\\ &\quad+\sum_{j=1}^{K}\frac{P(-j^2)}{D_K'(-j^2)} \bigl(j^4(x-H_j)-\frac14+\frac{1}{2j}\bigr). \end{aligned}

The first sum is over the finitely many nonzero coefficients of $q_{K,P}$ ; $[t^e]$ denotes a coefficient and the prime denotes formal differentiation. The variable $t$ is the input polynomial variable and $x$ is the output polynomial variable. Empty products are $1$ , empty sums are $0$ , and rational division by zero has value $0$ . In particular, $D_0=1$ , $H_0=0$ , and $M_0(P;x)=\sum_e[t^e]P\,\beta_e$ . At $n=0$ the determinant is that of the empty matrix and equals $1$ , and $s_0=F_0=1$ . The eventual assertion permits initial exceptions. Its inner conclusion cannot hold at $n=0$ , since then $Q$ would be an integer constant with $0<Q(Z)<1$ .

View graph