Integral normalization with the repository’s effective growth bound

Open

Apery.normalization

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

formalizationirrationalitynumber-theoryzeta5-mo271

There exists a sequence of positive rational numbers $m_n$ , positive for every $n\in\mathbb N$ , such that $m_nF_n$ has integer coefficients for all sufficiently large $n$ . Moreover, for every real $\varepsilon>0$ , eventually

\log m_n\le(A_{\rm eff}+\varepsilon)K_n^2,\qquad A_{\rm eff}=1.36,\quad K_n=40n.

The index after which the growth inequality holds may depend on $\varepsilon$ . This is the existential normalization interface proved by the repository using its explicit factor $m_N$ , local prime estimates, and the prime number theorem. It records the repository's modified constants, rather than the paper's stronger normalization rate.

Preamble

import Mathlib
import Definitions.Def_Zeta5_SourceConstruction
import Definitions.Def_Zeta5_SourceConstants

open Polynomial Filter Topology MeasureTheory

Formal statement

namespace Apery

theorem normalization :
    ∃ m : ℕ → ℚ, (∀ n, 0 < m n) ∧
      (∀ᶠ n in atTop, ∃ Q : ℤ[X], Q.map (Int.castRingHom ℚ) = C (m n) * F n) ∧
      ∀ ε : ℝ, 0 < ε → ∀ᶠ n in atTop, Real.log (m n) ≤ ((Aeff : ℝ) + ε) * Kr n ^ 2 := by sorry

end Apery

Source

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

Read-back

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

There exists a single function $m:\mathbb N\to\mathbb Q$ with $m(n)>0$ for every natural number $n$ , such that there is a natural-number threshold $N_0$ for which every $n\ge N_0$ admits a polynomial $Q\in\mathbb Z[x]$ whose coefficientwise image in $\mathbb Q[x]$ is exactly $m(n)F_n(x)$ , and such that for every real number $\varepsilon>0$ there is a natural-number threshold $N_\varepsilon$ for which every $n\ge N_\varepsilon$ satisfies

\log(m(n))\le\left(\frac{136}{100}+\varepsilon\right)(40n)^2.

The logarithm uses the positive rational $m(n)$ embedded in $\mathbb R$ , and $n$ is also embedded in $\mathbb R$ in this inequality. The polynomial $Q$ may depend on $n$ , the bound threshold may depend on $\varepsilon$ , and the same function $m$ serves all positive $\varepsilon$ . 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 positivity requirement includes $n=0$ ; the two eventual requirements allow finitely many initial exceptions.

View graph