Arithmetic lower bounds for Thue's auxiliary polynomials

Suppose (X - α)^r divides P - α Q, where P, Q are integer polynomials, not both zero, of degree at most N < d r, and α has degree d ≥ 2. For any rational approximants x, y, the nonvanishing theorem supplies an order k with k + d (r - 1) ≤ 2 N and DᵏP(x) - y DᵏQ(x) ≠ 0. Clearing denominators then gives the lower bound

|DᵏP(x) - y DᵏQ(x)| ≥ (H(x)^(N-k) H(y))⁻¹.

Here H is the rational multiplicative height Height.mulHeight₁. The exponent retains the degree drop from Hasse differentiation. This is the arithmetic half of the gap argument: analytic smallness of the same nonzero value can then contradict this bound for two sufficiently good approximants. No coefficient-length or approximation hypothesis is needed for the lower bound itself.

Main results

• TauCeti.exists_hasseDeriv_aeval_sub_lower_bound: the natural-degree form.
• TauCeti.exists_thue_hasseDeriv_lower_bound: the degree and order bounds for Thue's auxiliary construction with parameter ε.

References

• J.-H. Evertse, Diophantine Approximation, lecture notes (2019), ch. 6, proof of Theorem 6.14.

theorem TauCeti.exists_hasseDeriv_aeval_sub_lower_bound {F : Type u_1} [Field F] [CharZero F] {α : F} (hd : 2 ≤ (minpoly ℚ α).natDegree) {P Q : Polynomial ℤ} (hPQ : P ≠ 0 ∨ Q ≠ 0) {N r : ℕ} (hP : P.natDegree ≤ N) (hQ : Q.natDegree ≤ N) (hN : N < (minpoly ℚ α).natDegree * r) (hdvd : (Polynomial.X - Polynomial.C α) ^ r ∣ Polynomial.map (Int.castRingHom F) P - Polynomial.C α * Polynomial.map (Int.castRingHom F) Q) (x y : ℚ) : ∃ k ≤ N, k + (minpoly ℚ α).natDegree * (r - 1) ≤ 2 * N ∧ (Height.mulHeight₁ x ^ (N - k) * Height.mulHeight₁ y)⁻¹ ≤ |↑((Polynomial.aeval x) ((Polynomial.hasseDeriv k) P) - y * (Polynomial.aeval x) ((Polynomial.hasseDeriv k) Q))|

The nonvanishing Hasse derivative difference for two rational points has an explicit height lower bound. Its order is at most N and satisfies k + d (r - 1) ≤ 2 N; differentiation lowers the height exponent to N - k.

theorem TauCeti.exists_thue_hasseDeriv_lower_bound {F : Type u_1} [Field F] [CharZero F] {α : F} (hd : 2 ≤ (minpoly ℚ α).natDegree) {ε : ℝ} (hε₀ : 0 ≤ ε) (hε : ε < 1 / 2) {r : ℕ} (hr : 0 < r) {P Q : Polynomial ℤ} (hPQ : P ≠ 0 ∨ Q ≠ 0) (hP : P.natDegree ≤ ⌊(1 / 2 + ε) * ↑(minpoly ℚ α).natDegree * ↑r⌋₊) (hQ : Q.natDegree ≤ ⌊(1 / 2 + ε) * ↑(minpoly ℚ α).natDegree * ↑r⌋₊) (hdvd : (Polynomial.X - Polynomial.C α) ^ r ∣ Polynomial.map (Int.castRingHom F) P - Polynomial.C α * Polynomial.map (Int.castRingHom F) Q) (x y : ℚ) : ∃ k ≤ ⌊(1 / 2 + ε) * ↑(minpoly ℚ α).natDegree * ↑r⌋₊, ↑k ≤ ↑(minpoly ℚ α).natDegree * (2 * ε * ↑r + 1) ∧ (Height.mulHeight₁ x ^ (⌊(1 / 2 + ε) * ↑(minpoly ℚ α).natDegree * ↑r⌋₊ - k) * Height.mulHeight₁ y)⁻¹ ≤ |↑((Polynomial.aeval x) ((Polynomial.hasseDeriv k) P) - y * (Polynomial.aeval x) ((Polynomial.hasseDeriv k) Q))|

Arithmetic lower bound in Thue's gap argument. For the auxiliary degree N = ⌊(1/2 + ε) d r⌋, where 0 ≤ ε < 1/2 and r ≥ 1, there is an order k ≤ d (2 ε r + 1) giving a derivative difference of size at least (H(x)^(N-k) H(y))⁻¹. The estimate holds for every pair of rational points, without assuming that they approximate α.