Geometric Moments and Rational Lambert Values: Proofs and Further Results

Will Cook

Long paper

Geometric Moments and Rational Lambert Values: Proofs and Further Results

Erdős #1049 By Will Cook September 2026 Authorship, AI use and citation

PDFOpen the PDF, 80 pages TeXLaTeX source Source on GitHub Problem page

Summary. The record proves the fixed-base Hankel asymptotic for Zudilin's normalised moments and the rational-base irrationality criterion log b/log a<0.4056830213840605…. The determinant proof separates geometric node configurations from positive weights; the irrationality proof instead specialises Zudilin's 2004 polynomial forms after cancellation. Coefficient moments, evaluated lattices and congruence conditions distinguish integer divisibility from nonzero remainder decay. A broader ratio-limit argument and a rational-value model remain unformalised. None of these arguments settles $F (3 / 2)$ .

This paper covers the sharp fixed-base Hankel asymptotic and rational-base irrationality proofs, coefficient moments and arithmetic obstructions, with ordinary ratio-limit and rational-value models distinguished from checked results.

It does not establish the validity of claims tagged Lean, which belongs to the cited kernel-checked source, or a solution to Erdős #1049, which remains open.

Start here, by the editorial route

In this paper

The height criterion at $7 / 2$

The base $7 / 2$ already lies in the irrationality region of Bundschuh and Väänänen [6]. We check their height condition in their notation, with $q$ denoting the base. At $α = - 1$ it reads

λ < {(\frac{1}{2} + \frac{1}{π^{2}})}^{- 1} .

At $q = 7 / 2$ the Archimedean parameter is $λ = \log 7 / \log (7 / 2)$ . The criterion therefore applies once the following strict inequality is checked.

Theorem 8.1 (the $7 / 2$ height condition).

\frac{\log 7}{\log (7 / 2)} < {(\frac{1}{2} + \frac{1}{π^{2}})}^{- 1} .

Proof. Since $2^{18} = 262144 < 823543 = 7^{7}$ , we have $\log 2 / \log 7 < 7 / 18$ . Also $π > 3$ gives $1 / 2 + 1 / π^{2} < 11 / 18$ . Hence

\frac{\log 7}{\log (7 / 2)} = \frac{1}{1 - \log 2 / \log 7} < \frac{18}{11} < {(\frac{1}{2} + \frac{1}{π^{2}})}^{- 1} .

Every denominator is positive, so the reciprocal inequalities have the displayed directions. ◻

Numerically the two sides are $1.5533 \dots$ and $1.6630 \dots$ , so the condition holds with a margin of about $0.11$ . The Lean proof factors the estimate through the explicit height-region predicate and the integer certificate $2^{18} < 7^{7}$ , the resulting logarithmic ratio bound $\log 2 / \log 7 < 7 / 18$ , the $π$ -bound $1 / π^{2} < 1 / 9$ , and the strict margin

\frac{\log 2}{\log 7} < \frac{1}{2} - \frac{1}{π^{2}} .

The final height inequality then rewrites $\log (7 / 2) = \log 7 - \log 2$ and closes the displayed condition.

This formalises the complete elementary parameter check at $q = 7 / 2$ ; it does not formalise Bundschuh and Väänänen’s analytic irrationality theorem, whose proof occupies pp. 189–193 of the source. The conclusion that $F (7 / 2)$ is irrational is consequently cited from that theorem, not claimed as a Lean theorem here.

The criterion does not cover $3 / 2$ , and the results of Sections 6 and 7 give no evidence either way about whether $F (3 / 2)$ is irrational.

The $81 / 200$ logarithmic region

Consider the rational-height region

\frac{\log b}{\log a} < \frac{81}{200} (a > b > 0) .

The number $81 / 200$ is the rational lower bound on $θ^{*}$ proved earlier. The bracket $81 / 200 < θ^{*} < 1 / 2$ in Section 2.5 puts this entire smaller region inside Theorem 2.2. Membership of the smaller region is an integer comparison. The Lean module of this library treats the displayed inequality as a definition and proves elementary memberships and exclusions. In particular,

\frac{2}{5} < \frac{\log 4}{\log 31} < \frac{81}{200} < \frac{\log 2}{\log 3} .

The first two comparisons come respectively from $31^{2} < 4^{5}$ and $4^{200} < 31^{81}$ ; the last comes from $3^{81} < 2^{200}$ . Lean checks the lower bound. Consequently $31 / 4$ lies in the enlarged region, and so does every positive power $(31 / 4)^{r}$ . The same base lies strictly outside the earlier Bundschuh–Väänänen region, so the $81 / 200$ inequality defines a strict set-theoretic enlargement of the earlier recorded logarithmic region. Combined with the bracket $81 / 200 < θ^{*}$ , these memberships are exactly the finite input to Theorem 2.3, which is where the irrationality of $F (31 / 4)$ and of every $F ((31 / 4)^{r})$ is proved.

It still does not approach $3 / 2$ . The exact comparison

3^{81} < 2^{200} ⟹ \frac{81}{200} < \frac{\log 2}{\log 3}

is Lean-checked, as is the conclusion that $3 / 2$ belongs to neither height region (comparison with $\log 2 / \log 3$ , $3 / 2$ fails the condition). Thus $81 / 200$ is the larger of the two explicitly defined cutoffs used below, while a cutoff that includes $3 / 2$ must be strictly larger than $\log 2 / \log 3 \approx 0.6309$ .

About this paper

Authorship and AI use. Will Cook built and directed the research infrastructure and maintains the public release. He reviewed claims when he could. AI agents did most of the research and drafting. Cook did not independently verify every claim.

Cite and contact. Cite this paper by its title, author and date above, with its PDF; cite the earlier sources it uses for a mathematical result. For software, use the release citation and give the commit used. Contact Will with questions or corrections.

Prefer the manuscript?

PDFOpen the PDF, 80 pages TeXOpen the LaTeX source Problem page

Equations typeset from the exact TeX. Rendered from the LaTeX manuscript source with file fingerprint sha256:1f04580702ed8f8c. Its file fingerprint matched the published source record, so the PDF above, the LaTeX, and this page are one manuscript. Redeploying the site regenerates this page from whatever the public repository holds at that moment.

The height criterion at 7/27/2

The 81/20081/200 logarithmic region

About this paper

The height criterion at $7 / 2$

The $81 / 200$ logarithmic region