The Hankel determinant construction of the paper "ζ(5) is irrational"

This file defines (in Lean) the objects of Section 2.1 of the paper "ζ(5) is irrational" (A. Fauzan, 17 September 2026):

• the polynomials D_m(t) = ∏_{j=1}^m (t + j²);
• the ℚ-linear functional μ_X, given on monomials by (2.2) and on the simple poles 1/(t + j²) by (2.3), extended to P / D_K by polynomial division and partial fractions;
• the Hankel matrix G_K(X) of (2.4), its determinant Δ_K(X), the scalar S_K of (2.5) and F_K = S_K Δ_K.

Throughout, K = 40 n, N = 3 n, h = 37 n as in (2.1).

Convention. Two polynomial rings ℚ[X] occur: the paper's variable t (the argument of the rational functions the functional is applied to) and the paper's indeterminate X (the value of the functional is affine in X). Both are represented by Polynomial ℚ; the docstrings say which is which.

Nothing is proved about these objects here; see Zeta5Irrational.MainEstimate for the main estimate.

noncomputable def Zeta5Irrational.D (m : ℕ) : Polynomial ℚ

D_m(t) = ∏_{j=1}^m (t + j²), a monic polynomial in t.

Equations

• Zeta5Irrational.D m = ∏ j ∈ Finset.Icc 1 m, (Polynomial.X + Polynomial.C (↑j ^ 2))

def Zeta5Irrational.μmono (e : ℕ) : ℚ

The polynomial moments (2.2): μ(t^e) = (-1)^e B_{2e+2} (2e+3)(2e+4)(2e+5) / 24. Mathlib's bernoulli uses the convention B₁ = -1/2, as does the paper.

Equations

• Zeta5Irrational.μmono e = (-1) ^ e * bernoulli (2 * e + 2) * ((2 * ↑e + 3) * (2 * ↑e + 4) * (2 * ↑e + 5)) / 24

noncomputable def Zeta5Irrational.μpoly (P : Polynomial ℚ) : ℚ

μ on polynomials in t, extended ℚ-linearly from the monomials.

Equations

• Zeta5Irrational.μpoly P = P.sum fun (e : ℕ) (c : ℚ) => c * Zeta5Irrational.μmono e

def Zeta5Irrational.H5 (j : ℕ) : ℚ

The generalized harmonic number H_j^{(5)} = ∑_{v=1}^j v⁻⁵.

Equations

• Zeta5Irrational.H5 j = ∑ v ∈ Finset.Icc 1 j, 1 / ↑v ^ 5

noncomputable def Zeta5Irrational.poleValue (j : ℕ) : Polynomial ℚ

The pole values (2.3), as polynomials in the indeterminate X: μ_X(1/(t + j²)) = j⁴ (X - H_j^{(5)}) - 1/4 + 1/(2j).

Equations

• Zeta5Irrational.poleValue j = Polynomial.C (↑j ^ 4) * (Polynomial.X - Polynomial.C (Zeta5Irrational.H5 j)) - Polynomial.C (1 / 4) + Polynomial.C (1 / (2 * ↑j))

noncomputable def Zeta5Irrational.μX (K : ℕ) (P : Polynomial ℚ) : Polynomial ℚ

μ_X(P(t) / D_K(t)) for a polynomial P in t, as a polynomial in X. Since D_K is monic with the simple roots t = -j² (1 ≤ j ≤ K), P / D_K = (P /ₘ D_K) + ∑_j (P(-j²) / D_K'(-j²)) / (t + j²), and μ_X is applied termwise.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Zeta5Irrational.G (n : ℕ) : Matrix (Fin (37 * n)) (Fin (37 * n)) (Polynomial ℚ)

The h × h Hankel matrix G_K(X) of (2.4), whose (i, j) entry is μ_X (D_N(t)^6 t^(i+j) / D_K(t)), with K = 40 n, N = 3 n, h = 37 n.

Equations

• Zeta5Irrational.G n i j = Zeta5Irrational.μX (40 * n) (Zeta5Irrational.D (3 * n) ^ 6 * Polynomial.X ^ (↑i + ↑j))

noncomputable def Zeta5Irrational.Δ (n : ℕ) : Polynomial ℚ

Δ_K(X) = det G_K(X), a polynomial in X (of degree h, by (2.9)).

Equations

• Zeta5Irrational.Δ n = (Zeta5Irrational.G n).det

noncomputable def Zeta5Irrational.S (n : ℕ) : ℚ

The scalar S_K of (2.5).

Equations

• Zeta5Irrational.S n = ↑(40 * n).factorial ^ (2 * (37 * n)) * 4 ^ (37 * n - 1) / (↑(3 * n).factorial ^ (12 * (37 * n)) * ∏ i ∈ Finset.Icc 1 (37 * n - 1), ↑(2 * i).factorial ^ 2)

noncomputable def Zeta5Irrational.F (n : ℕ) : Polynomial ℚ

F_K = S_K Δ_K of (2.5).

Equations

• Zeta5Irrational.F n = Polynomial.C (Zeta5Irrational.S n) * Zeta5Irrational.Δ n