claimroutine
Choose F_0 so nu/F_0 is small
Picks so that
first third of the error budget
Claim·§4 Choice of parameters and proof of Theorem~thm:main·inside thmIrrationality exponent of pi is 2
Statement (paper)
Fix and suppose that there are arbitrarily large positive integers for which some satisfies . Then, with fixed from Lemma and , one can choose so large that .
In plain English
Assume, for a fixed , that arbitrarily large admit with . With the constants from the parameter lemma and , one can pick large enough that .
Why it's here
This sets the first parameter in the contradiction argument, by which the term of the total error becomes a small fraction of the margin , which is positive because . The later claims on dimension, weights and the combined error margin build on this choice of .
Classified routine:
Follows directly from the positivity of \varepsilon_0 supplied by Lemma : choosing F_0>\max\{2/\theta,3\nu/\varepsilon_0\} gives both inequalities.