Even-index Zeilberger–Zudilin integrals are integer linear forms in and
OpenPiIrrationality.ZZEven.linearFormdiophantine-approximationnumber-theorypi
With , , , and as in the definition file PiIrrationality_ZZEvenForms, for every there are integers and with
This is the arithmetic of the Zeilberger–Zudilin construction at even index. The integrand has the even partial-fraction decomposition with . Only the term produces , through . The multiplier clears all denominators: the -adic and -adic valuations of the Laurent coefficients give the power of , and the deleted primes in divide every relevant coefficient. The -coefficient is . The residue satisfies , by the substitution , which turns into .
Preamble
import Definitions.Def_PiIrrationality_ZZEvenForms import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Formal statement
theorem PiIrrationality.ZZEven.linearForm (n : ℕ) (hn : 1 ≤ n) :
∃ U V : ℤ,
(PiIrrationality.ZZEven.M n : ℂ) * PiIrrationality.ZZEven.J n =
(U : ℂ) + (V : ℂ) * (Real.pi : ℂ) ∧
(V : ℝ) = -(PiIrrationality.ZZEven.M n * 16 ^ n *
(PiIrrationality.ZZEven.coef n : ℝ) / 4) := by
sorrySource
Y. Bai, The irrationality measure of π is at most 7.101862832357, arXiv:2609.11276 (v2, 11 Sep 2026), Section 2: Lemmas 2.1–2.6 and Proposition 2.7 (with (a,b,c)=(2,4,6), so h=5 and d0=8), and equation (4.5); D. Zeilberger and W. Zudilin, The irrationality measure of π is at most 7.103205334137…, Moscow J. Combin. Number Theory 9 (2020), no. 4, 407–419, arXiv:1912.06345, Lemmas 1–6 and Proposition 1 at index 2n.