The logarithms of rational numbers have irrationality exponent 2 [pdf]

The paper [4] proves 𝜇(𝜋) = 2 by a Roth-type argument on the exponential curve: an interpolation determinant whose rows are jets at 𝐾 centres (1, 𝑗𝜔), 𝜔 = 2𝜋𝑖, of polynomials restricted to the curve 𝑧 ↦ → (𝑒𝑧 , 𝑧 + 𝑢), whose columns are weighted monomials, whose arithmetic size is bounded below because the centres are Gaussian integer points after clearing the denominators 𝑞𝑖 of the approximations, and whose analytic size is bounded above because rows at different centres test the same entire functions and collide. The theorem is machine-verified in Lean 4 over Mathlib, and so is Theorem A below (Section 6). We cite [4] by its section, equation and result numbers throughout. Theorem A. Let 𝛼 be a positive rational number, 𝛼 ≠ 1, and 𝜔 = log 𝛼. For every real 𝜈 > 2 there is 𝑄(𝜈, 𝛼) such that 𝜔 − 𝑝 𝑞 ≥ 𝑞−𝜈 for all integers 𝑝, 𝑞 with 𝑞 ≥ 𝑄(𝜈, 𝛼). Hence 𝜇(log 𝛼) = 2; in particular 𝜇(log 2) = 2. The argument of [4] uses one property of 𝜋: 𝑒2 𝜋𝑖 𝑗 = 1, which places the centre (1, 𝑗𝜔) on the curve at 𝑧 = 𝑗𝜔 (Lemma 3.2 there). For 𝜔 = log 𝛼 the analogous fact is 𝑒 𝑗 𝜔 = 𝛼 𝑗 , which places the centre (𝛼 𝑗 , 𝑗𝜔) on the curve. The centres therefore lie in distinct fibres of the exponential coordinate 𝑌 , and the interpolation theorem of [4], stated for centres with 𝑌 = 1, must be restated for centres (𝑦 𝑗 , 𝑐 𝑗 ) with distinct 𝑦 𝑗 . Section 2 does this; the proof is that of [4], Section 2, with three local changes which we display. Section 3 carries the 𝑌 -height of 𝛼 𝑗 through the determinant estimates: it costs (𝐾 − 1) log 𝑏/𝑤0 in the arithmetic lower bound (𝛼 = 𝑎/𝑏) and replaces the radius 100𝐾 by 100𝐾 (1 + | log 𝛼|) in the collision estimate, both of the form 𝑂 𝛼 (𝐾/𝑤0), which the parameter choice of [4], Section 4, sends to zero. For Date: October 7, 2026. ∗Author of The Da Vinci Code. 1 2 DAN BROWN∗ 𝛼 = 2 the arithmetic lower bound is literally Lemma 3.1 of [4]. Section 5 records what the method gives for algebraic 𝛼 and why it gives nothing for log 3/log 2. Notation. Coordinates 𝑌 , 𝑋1, . . . , 𝑋𝑚; a positive rational weight vector 𝑊 = (𝑤0, . . . , 𝑤𝑚) gives the 𝑊-degree 𝑤0 ℎ + Í 𝑤𝑖 𝛼𝑖 of 𝑌 ℎ 𝑋 𝛼, and 𝑃𝑊 (𝐻) is the space of polynomials of 𝑊-degree at most 𝐻. For 𝑉 = (𝑣0, . . . , 𝑣𝑚), 𝐽𝑉 (𝐻) is the quotient of C[[𝑡, 𝑢1, . . . , 𝑢𝑚]] by the series all of whose monomials have 𝑉-weight at least 𝐻. We write 𝑤𝛽 = Í𝑖 𝑤𝑖 𝛽𝑖 , 𝑤∗ = min𝑖 𝑤𝑖 , Λ = 4 log 2, and all logarithms are natural. 2. Interpolation with centres in distinct fibres Theorem 2.1 (Separated-weight interpolation, general fibres). Fix integers 𝑚, 𝐾 ≥ 1 and positive rationals 𝑤0, 𝑣0, 𝜃 with 0 < 𝜃 < 1, (1) 𝐾𝜃𝑚 < 1, 𝐾 𝑤0 𝑣0 𝜃𝑚 < 1. There are successive lower thresholds for positive rationals 𝑤1, . . . , 𝑤𝑚, each depending only on these data and the previously chosen weights, with the following property. Put 𝑊 = (𝑤0, . . . , 𝑤𝑚), 𝑉 = (𝑣0, 𝑤1/𝜃, . . . , 𝑤𝑚/𝜃). For any points 𝑎 𝑗 = (𝑦 𝑗 , 𝑐 𝑗1, . . . , 𝑐 𝑗𝑚) ∈ C× × C𝑚, 0 ≤ 𝑗 < 𝐾, such that whenever 𝑦 𝑗 = 𝑦 𝑗′ with 𝑗 ≠ 𝑗′ the coordinates 𝑐 𝑗𝑖 , 𝑐 𝑗′𝑖 differ for every 𝑖, the map (2) 𝑃𝑊 (𝐻) −→ 𝐾 −1Ê 𝑗=0 𝐽𝑉 (𝐻), 𝑃 ↦ −→ 𝑃 𝑦 𝑗 (1 + 𝑡), (𝑐 𝑗𝑖 + 𝑢𝑖 + log(1 + 𝑡))𝑚 𝑖=1 𝐾 −1 𝑗=0 , is surjective for all sufficiently large, sufficiently divisible 𝐻. The divisibility can be chosen using only the weights; the remaining threshold for 𝐻 may depend on the points. For 𝑦 𝑗 = 1 this is Theorem 2.1 of [4]. When the 𝑦 𝑗 are pairwise distinct the condition on the 𝑐 𝑗𝑖 is empty. Proof. We follow [4], Section 2, and indicate the changes. The weights are chosen as in (2.7)–(2.9) there: 𝜎 > 0 small with (1 + 3𝜎)𝑚+1𝐾 (𝑤0/𝑣0)𝜃𝑚 < 1, (1 + 3𝜎)𝑚𝐾𝜃𝑚 < 1, (1 + 𝜎)𝜃 < 1; 𝑣𝑖 = 𝑤𝑖 /𝜃; 𝐿0 = 𝑚 + 2; 𝐶∗ as in (2.8); and 𝑤1, . . . , 𝑤𝑚 successively so large that Î𝑎∈ 𝐴 𝑤𝑎 > 𝐶∗ Î𝑏∈ 𝐵 𝑣𝑏 for all index sets 𝐴, 𝐵 of equal size whose largest differing index lies in 𝐴. This involves no point. Let 𝐶 be an irreducible curve with generic point in the affine chart, with smooth projective model, 𝑊-degree deg𝑊 𝐶 =∑ 𝑃 max 0, − ord𝑃 𝑌 𝑤0 , − ord𝑃 𝑋1 𝑤1 , . . . , − ord𝑃 𝑋𝑚 𝑤𝑚 as in (2.10), and, at a branch 𝑃 through 𝑎 𝑗 , (3) ℎ𝑃 = min ord𝑃 (𝑌 − 𝑦 𝑗 ) 𝑣0 , ord𝑃 (𝑋1 − 𝑐 𝑗1 − log(𝑌 /𝑦 𝑗 )) 𝑣1 , . . . , ord𝑃 (𝑋𝑚 − 𝑐 𝑗𝑚 − log(𝑌 /𝑦 𝑗 )) 𝑣𝑚 , where log(𝑌 /𝑦 𝑗 ) is its formal expansion at 𝑌 = 𝑦 𝑗 , well defined along the branch since 𝑌 − 𝑦 𝑗 has positive order there. This replaces (2.11), where 𝑦 𝑗 = 1. In the local coordinate 𝑡 = 𝑌 /𝑦 𝑗 − 1 at 𝑎 𝑗 the jet (2) is 𝑃(𝑦 𝑗 (1 + 𝑡), 𝑐 𝑗 + 𝑢 + log(1 + 𝑡)), so ℎ𝑃 measures, in 𝑉-weight, the contact of the branch with the jet. The frame 𝐷0 = 𝑌 𝜕𝑌 + Í𝑖 𝜕𝑋𝑖 , 𝐷𝑖 = 𝜕𝑋𝑖 of [4] is unchanged. In the coordinates (𝑡, 𝑢) at 𝑎 𝑗 , where 𝑌 = 𝑦 𝑗 (1 + 𝑡) and 𝑋𝑖 = 𝑐 𝑗𝑖 + 𝑢𝑖 + log(1 + 𝑡), the chain rule gives 𝜕𝑡 = 𝑦 𝑗 𝜕𝑌 + (1 + 𝑡)−1 Í𝑖 𝜕𝑋𝑖 , hence (1 + 𝑡)𝜕𝑡 = 𝐷0 and 𝜕𝑢𝑖 = 𝐷𝑖 : the action of the frame on jets is the same at every centre, which is all that the order bookkeeping of [4] (the display after (2.13), “each monomial has order at least its weight times ℎ𝑃 ”) uses. LOGARITHMS OF RATIONAL NUMBERS HAVE IRRATIONALITY MEASURE 2 3 Curve inequality. We claim (4) deg𝑊 𝐶 ≥ (1 + 𝜎)∑ 𝑃↦ →𝑎 𝑗 ℎ𝑃 , the sum over all branches through prescribed points. Suppose it fails.