theoremnovelinferred_dep

Irrationality exponent of pi is 2

Irrationality exponent of π\pi is 2: ∣π−p/q∣≥q−ν|\pi-p/q|\ge q^{-\nu} for large qq
the headline result
Theorem·thm:main·§1 Introduction

Statement (paper)

The irrationality exponent of π\pi is 22. More precisely, for every real ν>2\nu>2, there is an integer Q(ν)Q(\nu) such that ∣π−pq∣≥q−ν(p∈Z, q∈Z, q≥Q(ν)). \left|\pi-\frac pq\right|\ge q^{-\nu} \qquad(p\in\ZZ,\ q\in\ZZ,\ q\ge Q(\nu)).

In plain English

For every real ν>2\nu>2 there is an integer Q(ν)Q(\nu) such that ∣π−p/q∣≥q−ν|\pi-p/q|\ge q^{-\nu} for all integers pp and q≥Q(ν)q\ge Q(\nu), so the irrationality exponent of π\pi equals 22.

Why it's here

The upper bound is proved by contradiction. Assuming good approximations with arbitrarily large qq, the parameter lemma, interpolation theorem and the arithmetic and translation lemmas let all error terms be made small, and the determinant comparison then fails. The lower bound 22 is the easy Dirichlet pigeonhole argument, which needs irrationality of π\pi, itself a consequence of the contradiction argument. The result is the paper's main theorem and feeds the Flint–Hills series corollaries.
Classified novel:
The claimed upper bound of 2 for the irrationality exponent of π is the paper’s main new result; known irrationality-exponent bounds do not establish this sharp value. The matching lower bound follows from Dirichlet’s approximation theorem.

Uses

lemExistence of admissible parameters for exponent nupropDeterminant comparison with two savingsthmInterpolation with separated weightslemArithmetic lower bound on minor determinantlemRows reduce to entire-function rows

Used by

corFlint–Hills series convergescorGeneralized Flint–Hills series convergence criterion

Inside the proof

claimChoose F_0 so nu/F_0 is smallclaimDimension choice makes errors small, savings largeclaimApproximants chosen with center-independent weight thresholdsclaimCombined error margins contradict determinant comparisonclaimPi is irrationalclaimDirichlet pigeonhole gives lower bound exponent 2

Sources

PaperOpen
Section
§1 Introduction
Page
—
Label
thm:main
Line
main.tex:64
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    The proof invokes , the arithmetic error E_ar defined in Lemma 3.1 (det:arithmetic).
  • info
    inferred_dep
    The proof invokes , the bound from the translation lemma (Lemma 3.2, det:translation).