A closed-form law for the Salikhov-Zeilberger-Zudilin-Bai family, and computational evidence that Bai's point is optimal

Abstract

Salikhov (2008), Zeilberger-Zudilin (2020) and Bai (2026) all bound the irrationality measure of pi with the same shape of complex contour integral, differing only in three exponents. We give one closed-form expression for the resulting bound as a function of those exponents. The saddle-point data come from an explicit cubic; the arithmetic factor -- the power of 2, the range of the lcm, and the prime-elimination window generalising Zeilberger-Zudilin's Lemma 2 -- is written down for arbitrary exponents, so no arithmetic lemma has to be redone for a new choice. The law returns 7.1032053341370017 at (2,2,3), agreeing with Zeilberger-Zudilin to 17 digits, and 7.1018628323563507 at Bai's point (1857,1857,2785), agreeing with his published 7.101862832357; it reproduces Salikhov's 7.606308 from his own two-branch window. We prove that the window measure is exactly homogeneous, W = a1.Jhat(a0/a1, b/a1), so the bound depends only on two ratios and the three-parameter lattice collapses to a two-dimensional object; that the pi-coefficient is a single coefficient extraction; and that at j = 0 the divisibility criterion is exact, a super-Catalan number appearing and Kummer's theorem then giving ord_p with equality rather than inequality. On that two-dimensional search we give computational evidence that Bai's point is the global minimum of the family: on the slice a0 = a1 the bound is a function of Q = 2a0/(3a0-2b) alone, with a sharp vertex at Q = 3714, realised primitively only by (1857,1857,2785). This rests on three finite computations and is labelled verified, not proved; the resulting floor 7.101862832356 is stated as a conjecture. An ancillary Python script (standard library only) re-derives every claim in about half a minute.