Geometric Moments and Rational Lambert Values: Proofs and Further Results

Formal verification and computations.

The printed proofs of Theorems 2.2 and 2.3 use Zudilin’s construction: his Lemma 7 in its polynomial reading, together with the inputs of that lemma’s own proof, namely his Lemma 3, the exponent $M(a;b)$ of (16) proved by his Lemma 4, the group stability of his Lemma 5, and the identity (9)–(11), all in [8], and his direction and constants [8]. Proved here are the nonrationality of $F$ as a function, the identification of the polynomial coefficients in Lemma 7, the exact degrees of $U_n$ and $V_n$, positivity, the Archimedean size estimate, and the limit $(K_n-W_n)/n^2\to C_0$. That last limit rests on Zudilin’s Lemmas 1 and 2 [8], whose method goes back to [7]; Section 2.3 proves them by that method with an explicit truncation estimate. Lean proves both theorems and the measure bound of Corollary 2.4; it constructs the polynomials and proves their remainder estimates. The Lean sources also contain the finite comparisons, the rational bracket in Section 2.5 and the degree identities in Section 2.2. Appendix A distinguishes these proofs from computer algebra.

Statements for every rank or every base.

Lean constructs the cancelled polynomial forms of Section 2 and proves irrationality in the stated region, irrationality at every positive integral power of $31/4$ and the irrationality-exponent bound. It proves the first nonzero term of every transformed row of the 2016 determinant, deduces the order and leading coefficient of the determinant at every rank, and proves the fixed-base asymptotic of Section 3.2. Both constructions therefore supply their mathematical objects; neither is assumed to exist. Proposition 10.5 is checked with no additional hypothesis; its Lean proof uses stability under $z\mapsto z^2$ alone, without the theorem of Adamczewski and Bell [16] cited in the printed proof, as explained after that proof.

Statements through rank eight.

Proposition 3.9 is checked in Lean for every real $p>1$ and every rank $N\le 8$. The Lean proof includes the identity $F(p)A_N-B_N=(v_{i+j}^{\ast })$, the positivity of the eight unshifted determinants $D_{k,0}$ by the certificate described in Section 3.4, the reality of the pencil roots, their position below $F(p)$ and their interlacing. It has no all-rank coefficient-positivity or root-convergence conclusion.

Computations outside Lean.

The shifted determinants $D_{k,1}$ and the strict positivity of every coefficient rest on the sixteen-polynomial computation of Section 3.4. The reconstruction of $U_n,V_n$ for $n\le 4$ in Section 2.7, the five complete polynomial contents and the seventy-six cyclotomic residue witnesses have exact reproduction scripts and direct determinant checks. Separate exact computations certify the rational interval bounds and the finite parameter search. The historical high-precision real remainder evaluations are separate numerical reports, not reproduced by these exact computations. None of these finite computations is a Lean declaration or is needed for the proof of Theorem 2.2.

The Lambert identity and the integer case.

The cited Formal Conjectures file contains unproved declarations for the conjecture and the integer-base irrationality theorem, as well as a proved identity between the two series [29]. For $t>1$, that identity is an equality of convergent series. The file also treats a different range using Lean’s convention that an unsummable series has totalised sum zero; that convention is not used in the present argument. The proved identity should therefore not be confused with a proved irrationality statement. The rational-base formal proofs used here are those described above.