claimroutineinferred_dep
Dimension choice makes errors small, savings large
Fixes so errors are below and
second third of budget; makes collision saving large
Claim·§4 Choice of parameters and proof of Theorem~thm:main·inside thmIrrationality exponent of pi is 2
Statement (paper)
For all sufficiently large integers , the data , , satisfy and , and the quantity tends to as , while , and . Consequently, with and , one can fix so large that and .
In plain English
For large , setting , and gives , , and , while , and . Hence one can fix so large that and , with and .
Why it's here
This fixes the dimension-type parameters , , , after is chosen, so that the error terms depending on them take up only a third of the margin while the collision saving exceeds the threshold needed in the determinant comparison. The growth of beats the factor , which makes large, and the later claims on weights and the combined error budget rely on this choice of to apply the determinant comparison.
Classified routine:
This is a direct calculation from the parameter definitions and their growth inequalities: exponential growth makes the required limits and error bounds hold for sufficiently large m. The choice is bookkeeping to meet the earlier determinant-comparison conditions, rather than a new technique.