Roth's auxiliary polynomial

Let α be an algebraic number of degree d, let b ≥ 1 be an integer with b α integral, and let ε ≥ 0. If the number n of variables satisfies 2 d ≤ exp (ε² n / 2), then for all positive integers r₁, …, rₙ there is a nonzero P ∈ ℤ[X₁, …, Xₙ] with deg_{Xᵢ} P ≤ rᵢ, whose index at the diagonal point (α, …, α) with weights r is at least (n / 2) (1 - ε), and whose coefficients are bounded in absolute value by C ^ (r₁ + ⋯ + rₙ), where C = 12 b max(1, ⌈α⌉) and ⌈α⌉ is the house of α.

This is the auxiliary polynomial in the proof of Roth's theorem. It vanishes to high index at (α, …, α); evaluated at a tuple of very good rational approximations of α, a suitable Hasse derivative of it is a nonzero rational number which is too small to have the denominator forced by the coefficients, unless the approximations have bounded height.

The coefficients of P are the ∏ᵢ (rᵢ + 1) unknowns. Index at least (n / 2) (1 - ε) means that the jets ∂^d P (α, …, α) vanish for every d in the box ∏ᵢ {0, …, rᵢ} with ∑ᵢ dᵢ / rᵢ < (n / 2) (1 - ε); the other jets vanish because of the degree bounds. After multiplication by b ^ (r₁ + ⋯ + rₙ) these are linear equations with coefficients in the ring of integers of ℚ(α). By TauCeti.card_filter_sum_div_le_mul_one_sub_le there are at most ∏ᵢ (rᵢ + 1) exp (-ε² n / 2) of them, so d times their number is at most half the number of unknowns, and Siegel's lemma NumberField.exists_ne_zero_int_vec_abs_le_of_house_le gives a small nonzero integer solution.

Main results

• TauCeti.exists_roth_auxiliary_polynomial: Roth's auxiliary polynomial, for an element α of any field of characteristic zero.

Implementation notes

Pottmeyer assumes 0 < ε < 1 and exp (ε² n / 4) ≥ 2 d. The counting estimate used here has the exponent ε² n / 2, so the weaker hypothesis exp (ε² n / 2) ≥ 2 d suffices, and no upper bound on ε is needed.

References

• L. Pottmeyer, Diophantine Approximation (2022), §2.6, Theorem 2.6.5.
• J.-H. Evertse, Diophantine Approximation, lecture notes (2019), ch. 3, Theorem 3.20 (Siegel's lemma), and ch. 6, Lemma 6.10 (Thue's one-variable auxiliary polynomials, whose reduction to ℚ(α) is followed here).

theorem TauCeti.exists_roth_auxiliary_polynomial {ι : Type u_2} [Fintype ι] {F : Type u_3} [Field F] [CharZero F] {α : F} {b : ℕ} (hb : 0 < b) (hbα : IsIntegral ℤ (↑b * α)) {ε : ℝ} (hε : 0 ≤ ε) (hn : 2 * ↑(minpoly ℚ α).natDegree ≤ Real.exp (ε ^ 2 * ↑(Fintype.card ι) / 2)) {r : ι → ℕ} (hr : ∀ (i : ι), r i ≠ 0) : ∃ (P : MvPolynomial ι ℤ), P ≠ 0 ∧ (∀ (i : ι), MvPolynomial.degreeOf i P ≤ r i) ∧ ENNReal.ofReal (↑(Fintype.card ι) / 2 * (1 - ε)) ≤ MvPolynomial.weightedIndex r (fun (x : ι) => α) ((MvPolynomial.map (Int.castRingHom F)) P) ∧ ∀ (m : ι →₀ ℕ), |↑(P.coeff m)| ≤ (12 * ↑b * max 1 (house α)) ^ ∑ i : ι, r i

Roth's auxiliary polynomial (Pottmeyer, Theorem 2.6.5). Let α be an algebraic number of degree d in a field of characteristic zero, and let b ≥ 1 be an integer such that b α is integral over ℤ. Let ε ≥ 0 and let ι be a finite set of n variables with 2 d ≤ exp (ε² n / 2). For all positive integers rᵢ, i ∈ ι, there is a nonzero P ∈ ℤ[Xᵢ : i ∈ ι] with deg_{Xᵢ} P ≤ rᵢ, whose index at (α, …, α) with weights r is at least (n / 2) (1 - ε), and whose coefficients have absolute value at most (12 b max(1, ⌈α⌉)) ^ (∑ᵢ rᵢ), where ⌈α⌉ is the house of α.