the proof notes section 4, Lemma 5, first step (partial fractions). With ρ_j = Res_{t=-j} R_n = rs n j, the Hankel entry is U_r(t^{a+b} R_n) = U_r(q_{a+b}) + Σ_j ρ_j (2jX + β_j) (-j)^a (-j)^b, where q_m = polynomialPart n m has integer coefficients and degree m - n. The exact valuation of ρ_j for n < j ≤ 5n < p² is 3v((j-1)!) - 4v((j-n-1)!) - v((5n-j)!).

Several lemmas are adapted from the Li₂ formalization dtq1997/li2-half-irrationality@d5d8206:Li2Unified/Modular/Base/ (DecayQuotient: D_succ, D_eq_desc; DecayBinomial: descPochhammer_eval_neg_one; DecayResidue: eraseProd_*; DecayMediumNodes: D_eval_neg_of_lt, padicValRat_factorial_small, rscale_val; IntegerFamily: the integer quotient), with the layout (s, K) = (3, 4) there replaced by (4, 5) here.

The polynomials D m

The integer polynomial part

noncomputable def Zeta32.Outer.integerD (m : ℕ) : Polynomial ℤ

The integral polynomial with roots -1, …, -m.

Equations

• Zeta32.Outer.integerD m = ∏ j ∈ Finset.Icc 1 m, (Polynomial.X + Polynomial.C ↑j)

theorem Zeta32.Outer.integerD_monic (m : ℕ) : (integerD m).Monic

theorem Zeta32.Outer.integerD_map (m : ℕ) : Polynomial.map (Int.castRingHom ℚ) (integerD m) = D m

noncomputable def Zeta32.Outer.integerPolynomialPart (n k : ℕ) : Polynomial ℤ

Integral polynomial quotient of the rational-function numerator by its denominator.

Equations

• Zeta32.Outer.integerPolynomialPart n k = Polynomial.X ^ k * Zeta32.Outer.integerD n ^ 4 /ₘ Zeta32.Outer.integerD (5 * n)

theorem Zeta32.Outer.integerPolynomialPart_map (n k : ℕ) : Polynomial.map (Int.castRingHom ℚ) (integerPolynomialPart n k) = polynomialPart n k

theorem Zeta32.Outer.polynomialPart_GV (p n k : ℕ) : Zeta5Irrational.GV p (polynomialPart n k) 0

theorem Zeta32.Outer.polynomialPart_natDegree_le (n k : ℕ) : (polynomialPart n k).natDegree ≤ k + 4 * n - 5 * n

Moments of integral polynomials

theorem Zeta32.Outer.polynomialMoment_eq (r : ℚ) (q : Polynomial ℚ) : polynomialMoment r q = ∑ e ∈ q.support, q.coeff e * moment r e

theorem Zeta32.Outer.polynomialMoment_VG {p : ℕ} [hp : Fact (Nat.Prime p)] {r : ℚ} (hr : Zeta5Irrational.VG p r 0) {q : Polynomial ℚ} (hq : Zeta5Irrational.GV p q 0) : Zeta5Irrational.VG p (polynomialMoment r q) (-1)

theorem Zeta32.Outer.polynomialMoment_VG_small {p : ℕ} [hp : Fact (Nat.Prime p)] (hp2 : p ≠ 2) {r : ℚ} (hr : Zeta5Irrational.VG p r 0) {q : Polynomial ℚ} (hq : Zeta5Irrational.GV p q 0) (hdeg : q.natDegree + 3 ≤ p) : Zeta5Irrational.VG p (polynomialMoment r q) 0

Residues

@[reducible, inline]

abbrev Zeta32.Outer.eraseProd (K j : ℕ) : ℚ

Product of the differences from j to all other indices in 1, …, K.

Equations

• Zeta32.Outer.eraseProd K j = Zeta32.Arith.Small.eraseProd K j

theorem Zeta32.Outer.eraseProd_base {j : ℕ} (hj : 1 ≤ j) : eraseProd j j = (-1) ^ (j - 1) * ↑(j - 1).factorial

theorem Zeta32.Outer.eraseProd_succ {K j : ℕ} (hjK : j ≤ K) : eraseProd (K + 1) j = eraseProd K j * (↑(K + 1) - ↑j)

theorem Zeta32.Outer.eraseProd_eq {K j : ℕ} (hj : 1 ≤ j) (hjK : j ≤ K) : eraseProd K j = (-1) ^ (j - 1) * ↑(j - 1).factorial * ↑(K - j).factorial

theorem Zeta32.Outer.eraseProd_ne_zero {K j : ℕ} (hj : 1 ≤ j) (hjK : j ≤ K) : eraseProd K j ≠ 0

noncomputable def Zeta32.Outer.rs (n j : ℕ) : ℚ

ρ_j = Res_{t=-j} D_n^4/D_{5n}.

Equations

• Zeta32.Outer.rs n j = Polynomial.eval (-↑j) (Zeta32.D n) ^ 4 / Zeta32.Outer.eraseProd (5 * n) j

theorem Zeta32.Outer.residue_eq (n k j : ℕ) : residue n k j = (-↑j) ^ k * rs n j

theorem Zeta32.Outer.D_eval_neg_of_lt (n j : ℕ) (hnj : n < j) : Polynomial.eval (-↑j) (D n) = (-1) ^ n * (↑(j - 1).factorial / ↑(j - 1 - n).factorial)

theorem Zeta32.Outer.D_eval_neg_of_le {n j : ℕ} (h1 : 1 ≤ j) (h2 : j ≤ n) : Polynomial.eval (-↑j) (D n) = 0

theorem Zeta32.Outer.rs_eq_zero {n j : ℕ} (h1 : 1 ≤ j) (h2 : j ≤ n) : rs n j = 0

theorem Zeta32.Outer.padicValRat_factorial_small {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : m < p ^ 2) : padicValRat p ↑m.factorial = ↑(m / p)

theorem Zeta32.Outer.padicValRat_neg_one_pow {p : ℕ} [hp : Fact (Nat.Prime p)] (m : ℕ) : padicValRat p ((-1) ^ m) = 0

theorem Zeta32.Outer.rs_val {p : ℕ} [hp : Fact (Nat.Prime p)] {n j : ℕ} (hnj : n < j) (hjK : j ≤ 5 * n) (hK : 5 * n < p ^ 2) : padicValRat p (rs n j) = 3 * ↑((j - 1) / p) - 4 * ↑((j - 1 - n) / p) - ↑((5 * n - j) / p)

The rank-one scalars and the entry decomposition

noncomputable def Zeta32.Outer.gam (r : ℚ) (n j : ℕ) : Polynomial ℚ

The pole scalar ρ_j (2jX + β_j).

Equations

• Zeta32.Outer.gam r n j = Polynomial.C (Zeta32.Outer.rs n j) * (Polynomial.C (2 * ↑j) * Polynomial.X + Polynomial.C (Zeta32.beta r j))

theorem Zeta32.Outer.entry_eq (r : ℚ) (n : ℕ) (a b : Fin (3 * n)) : (Polynomial.X • (B n).map ⇑Polynomial.C + (A r n).map ⇑Polynomial.C) a b = Polynomial.C (polynomialMoment r (polynomialPart n (↑a + ↑b))) + ∑ j ∈ Finset.Icc 1 (5 * n), gam r n j * Polynomial.C ((-↑j) ^ ↑a * (-↑j) ^ ↑b)

def Zeta32.Outer.wv (n p j : ℕ) : ℚ

Node weight of the proof notes, Lemma 5: w_j = v_p(ρ_j) + betaWt, and a large dummy value for the cancelled nodes j ≤ n (where ρ_j = 0).

Equations

• Zeta32.Outer.wv n p j = if j ≤ n then 15 * ↑n + 1 else 3 * ↑((j - 1) / p) - 4 * ↑((j - 1 - n) / p) - ↑((5 * n - j) / p) + Zeta32.Outer.betaWt p j

theorem Zeta32.Outer.gam_GV {p : ℕ} [hp : Fact (Nat.Prime p)] {r : ℚ} (hr : Zeta5Irrational.VG p r 0) {n j : ℕ} (hj1 : 1 ≤ j) (hjK : j ≤ 5 * n) (hK : 5 * n < p ^ 2) : Zeta5Irrational.GV p (gam r n j) (wv n p j)

theorem Zeta32.Outer.wv_le_big {p n j : ℕ} (hj : j ≤ 5 * n) : wv n p j ≤ 15 * ↑n + 1