Szpiro's conjecture for Frey curves, and asymptotic Fermat

Szpiro's conjecture implies Fermat's Last Theorem for all sufficiently large exponents. This file proves that implication, TauCeti.AsymptoticFermat, for the form of Szpiro's conjecture stated against the algorithmic conductor, TauCeti.AlgorithmicSzpiroConjecture.

The link is the Frey curve y² = x (x - A) (x + B). For coprime integers A and B with A ≡ -1 (mod 4), 32 ∣ B and B ≠ 0, the Frey curve is semistable, with minimal discriminant (A B (A + B))² / 2⁸ and algorithmic conductor rad (A B (A + B)). So Szpiro's conjecture bounds (A B (A + B))² by a constant times rad (A B (A + B)) ^ (6 + ε), uniformly over such pairs.

A solution of aⁿ + bⁿ = cⁿ in nonzero coprime integers with n ≥ 5 gives such a pair with A B (A + B) = (a b c)ⁿ: of the three n-th powers, the even one, or its negative, is B, and one of the two odd ones, or its negative, is A; this is TauCeti.exists_isCoprime_and_mul_mul_add_eq_pow. Its radical is rad (a b c) ≤ |a b c|, so Szpiro's bound with ε = 1 reads |a b c| ^ (2 n) ≤ C |a b c| ^ 7, while |a b c| ≥ 2 because one of a, b, c is even. This fails once 2 ^ (2 n - 7) > C. The argument works for every exponent n ≥ 5, prime or not, and for both parities of n.

The bound on the exponent is ineffective: it depends on the unknown constant in Szpiro's conjecture for ε = 1. So the conclusion is asymptotic Fermat, which says nothing about any particular exponent.

Main results

• TauCeti.AlgorithmicSzpiroConjecture.exists_sq_le_mul_radical_rpow: under Szpiro's conjecture, for every ε > 0 there is a constant C with (A B (A + B))² ≤ C rad (A B (A + B)) ^ (6 + ε) for all coprime A and B with A ≡ -1 (mod 4), 32 ∣ B and B ≠ 0.
• TauCeti.AlgorithmicSzpiroConjecture.asymptoticFermat: Szpiro's conjecture implies asymptotic Fermat.

References

• G. Frey, Links between stable elliptic curves and certain Diophantine equations, Ann. Univ. Sarav. Ser. Math. 1 (1986), 1–40.
• J. Oesterlé, Nouvelles approches du « théorème » de Fermat, Séminaire Bourbaki 694 (1988), Astérisque 161–162 (1988), 165–186.
• H. Darmon, F. Diamond, R. Taylor, Fermat's Last Theorem, in Current Developments in Mathematics 1995, International Press (1995), 1–154.

theorem TauCeti.AlgorithmicSzpiroConjecture.exists_sq_le_mul_radical_rpow (h : AlgorithmicSzpiroConjecture) {ε : ℝ} (hε : 0 < ε) : ∃ (C : ℝ), ∀ (A B : ℤ), IsCoprime A B → 4 ∣ A + 1 → 32 ∣ B → B ≠ 0 → ↑(A * B * (A + B)) ^ 2 ≤ C * ↑(UniqueFactorizationMonoid.radical (A * B * (A + B))) ^ (6 + ε)

Szpiro's conjecture for Frey curves. Under TauCeti.AlgorithmicSzpiroConjecture, for every ε > 0 there is a constant C such that (A B (A + B))² ≤ C rad (A B (A + B)) ^ (6 + ε) for all coprime integers A and B with A ≡ -1 (mod 4), 32 ∣ B and B ≠ 0. The Frey curve y² = x (x - A) (x + B) of such a pair has minimal discriminant (A B (A + B))² / 2⁸ and algorithmic conductor rad (A B (A + B)).

theorem TauCeti.AlgorithmicSzpiroConjecture.asymptoticFermat (h : AlgorithmicSzpiroConjecture) : AsymptoticFermat

Szpiro's conjecture implies asymptotic Fermat. If TauCeti.AlgorithmicSzpiroConjecture holds, there is an N such that aⁿ + bⁿ = cⁿ has no solution in positive integers for any exponent n ≥ N. The bound N depends on the constant of Szpiro's conjecture for ε = 1, so it is ineffective.