What question did this study set out to answer?

This work aims to establish a certified bound for Khinchin's constant and a conditional theorem that rules out integer relations.

May 25, 2026Open Access

A Certified Bound and a Conditional Lean Theorem for a Bounded-Height Algebraicity Exclusion for Khinchin's Constant

Read Full Paperexternally

Key Points

This work aims to establish a certified bound for Khinchin's constant and a conditional theorem that rules out integer relations.
Employed an interval-arithmetic verification chain and applied the Bailey-Borwein-Crandall series identity.
Developed a conditional theorem in Lean 4/Mathlib to rigorously verify bounds matching specific hypotheses.
Introduced a lemma that extends outcomes to a degree-≤6 pure-power sub-block at the same bound.
Established a certified Hermite/LLL bound of 578 digits for Khinchin's constant.
The conditional theorem identifies that no nonzero integer relation exists for specified norms among the 15-element basis.
The lemma successfully extends these findings to a pure-power sub-block of degree-≤6.

Abstract

We deposit two complementary artifacts concerning Khinchin's constant K₀ ≈ 2. 6854520010…: 1. **A certified Hermite/LLL bound `Mcertified`** (578-digit integer; SHA-256 of decimal-string form `c51099378e8c199c70d4543fb6b69f4de80986af34b628f6d9619f2181f6ab8e`) emitted by an interval-arithmetic verification chain (FLINT/Arb) anchored against OEIS A002210 via the BBC (Bailey–Borwein–Crandall, 1997) series identity at precision 8663 decimal places (M1 top rung Pbits = 28712). 2. **A formally-verified `conditional` Lean 4 / Mathlib v4. 14. 0 theorem** (`noₑuclideanᵣelationconditional`) that, under three explicit hypotheses matching the certified-bound + GS-lower-bound supplied numerically by the bound emission chain, **rules out** any nonzero integer relation of squared Euclidean norm ≤ Mₛq among the committed 15-element basis `BD (C) = 1, K₀, K₀², …, K₀⁶, log K₀, K₀·π, K₀·e, K₀·ln2, K₀·γ, K₀·ζ (2), K₀·ζ (3), K₀·G`. A companion lemma (`c1fromc2ᵦeroₑxtension`, this session's R-0 deliverable) extends this to the degree-≤6 pure-power sub-block at the same bound, via a norm-preserving zero-extension.

Connected Papers

Building similarity graph...

Analyzing shared references across papers

Discussion

Authors

Papanokechi

Actions

References and Citations

Connected Papers

Building similarity graph...

Analyzing shared references across papers

Discussion

Cite this study

Papanokechi (Sat,) studied this question.

synapsesocial.com/papers/6a13e88c0e02ee3982d33406 — DOI: https://doi.org/10.5281/zenodo.20355904

Also consider

Synapse has enriched 5 closely related papers on similar clinical questions. Consider them for comparative context:

Analysis of PSLQ, an integer relation finding algorithm· 1999 · 299 citations
Ratio in early Greek mathematics· 1979 · 40 citations
A Fortran 90-based multiprecision system· 1995 · 212 citations
On the rapid computation of various polylogarithmic constants· 1997 · 331 citations
Multidimensional Euclidean algorithms.· 1982 · 9 citations

A Certified Bound and a Conditional Lean Theorem for a Bounded-Height Algebraicity Exclusion for Khinchin's Constant

Key Points

Abstract

Citation Network

Connected Papers

Discussion

Authors

Actions

References and Citations

Citation Network

Connected Papers

Discussion

Cite this study

Also consider

Also consider