lemmaroutine

Existence of admissible parameters for exponent nu

Gives rationals θ<A<B<1\theta<A<B<1, C>1C>1 and η\eta making g>0g>0 for each ν>2\nu>2
fixes the numerical parameters for the main proof
Lemma·par:constants·§4 Choice of parameters and proof of Theorem~thm:main

Statement (paper)

For every real ν>2\nu>2, there are positive rational numbers θ,A,B,C\theta,A,B,C such that 0<θ<A<B<1,ν(A−θ)>1−θ,C>1,B<1/C,B<Cθ<1. 0<\theta<A<B<1,\qquad \nu(A-\theta)>1-\theta,\qquad C>1,\quad B<1/C,\quad B<C\theta<1. One can then choose 0<η<10<\eta<1 such that g:=ν(A(1−η)−θ)−(1−θ)>0. g:=\nu\bigl(A(1-\eta)-\theta\bigr)-(1-\theta)>0.

In plain English

For every real ν>2\nu>2 there exist positive rationals θ<A<B<1\theta<A<B<1 and C>1C>1 with ν(A−θ)>1−θ\nu(A-\theta)>1-\theta, B<1/CB<1/C and B<Cθ<1B<C\theta<1. Then some η∈(0,1)\eta\in(0,1) makes g=ν(A(1−η)−θ)−(1−θ)g=\nu(A(1-\eta)-\theta)-(1-\theta) positive.

Why it's here

This lemma fixes the numerical parameters used in the proof of the main theorem, so that all later inequalities have room to hold. The strict inequality ν(A−θ)>1−θ\nu(A-\theta)>1-\theta is open in AA, so shrinking AA slightly by a factor 1−η1-\eta keeps it true and gives a positive gap gg.
Classified routine:
This is a direct feasibility argument for strict numerical inequalities: choose the rational parameters within an open admissible region, then take η small enough to preserve the positive gap. It uses no result specific to π.

Uses

Nothing else in the paper

Used by

thmIrrationality exponent of pi is 2claimChoose F_0 so nu/F_0 is small

Sources

PaperOpen
Section
§4 Choice of parameters and proof of Theorem~thm:main
Page
—
Label
par:constants
Line
sections/conclusion.tex:9
Leannot aligned

Phase 2 aligns this node to a Lean declaration.