claimroutineinferred_dep

Approximants chosen with center-independent weight thresholds

Picks approximants pi/qip_i/q_i with weights wiw_i whose margin is below ε0/3\varepsilon_0/3
last parameter choice; distinct centers for interpolation
Claim·§4 Choice of parameters and proof of Theorem~thm:main·inside thmIrrationality exponent of pi is 2

Statement (paper)

With mm, KK, w0w_0, v0v_0 fixed, one can choose approximations pi/qip_i/q_i satisfying , with wi=⌈log⁡qi⌉w_i=\lceil\log q_i\rceil, successively sufficiently large for Theorem  and such that holds, i.e. Λ∑i=1m1wi+θ+log⁡4+log⁡(2K)+ν+log⁡(200K)w∗<ε03\Lambda\sum_{i=1}^m\frac1{w_i}+\frac{\theta+\log4+\log(2K)+\nu+\log(200K)}{w_*}<\frac{\varepsilon_0}{3} with w∗=min⁡i>0wiw_*=\min_{i>0}w_i. The thresholds for weight separation are independent of the centers, and for sufficiently large qiq_i one has pi≠0p_i\ne0, so that cji=jric_{ji}=jr_i, ri=2ipi/qir_i=2\ii p_i/q_i, are distinct across jj in each coordinate, with no independence between different coordinates required.

In plain English

Once mm, KK, w0w_0, v0v_0 are fixed, one can pick approximations pi/qip_i/q_i of π\pi with wi=⌈log⁡qi⌉w_i=\lceil\log q_i\rceil, each successively large enough for the interpolation theorem and satisfying the weight-margin inequality Λ∑i=1m1wi+θ+log⁡4+log⁡(2K)+ν+log⁡(200K)w∗<ε03\Lambda\sum_{i=1}^m\frac1{w_i}+\frac{\theta+\log4+\log(2K)+\nu+\log(200K)}{w_*}<\frac{\varepsilon_0}{3}. The weight-separation thresholds do not depend on the centers, and for large qiq_i we have pi≠0p_i\ne0, so the centers cji=jric_{ji}=jr_i are distinct in each coordinate.

Why it's here

This is the last parameter choice: it picks the approximants and weights after F0F_0, mm, KK, w0w_0, v0v_0 are fixed. Because the interpolation theorem's weight thresholds do not depend on the points or centers, the wiw_i can be taken large in advance, and pi≠0p_i\ne0 makes the centers jrijr_i pairwise distinct in each coordinate, which is exactly the hypothesis that theorem needs. The weight-margin bound uses the last third of ε0\varepsilon_0 in the combined error budget used by the next claim.
Classified routine:
This is a parameter-choice step: under the assumed existence of arbitrarily large good approximants, their weights can be made successively large enough to meet the center-independent thresholds of geom-interpolation and the stated error margin. The distinctness of the centers follows directly from p_i ≠ 0.

Uses

thmInterpolation with separated weightsclaimChoose F_0 so nu/F_0 is smallclaimDimension choice makes errors small, savings large

Used by

claimCombined error margins contradict determinant comparison

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Approximants meet center-independent weight thresholds" rests on claim-thm-main-1
  • info
    inferred_dep
    outline: "Approximants meet center-independent weight thresholds" rests on claim-thm-main-2