Szpiro's conjecture implies the abc conjecture with exponent 3 / 2

Let a + b = c be coprime integers. The Frey curve y² = x (x - a) (x + b) has discriminant 16 (a b c)², and away from 2 its reduction is good or multiplicative, bad exactly at the primes dividing a b c. So its minimal discriminant is about (a b c)² and its conductor about rad (a b c), and Szpiro's conjecture |Δ_min| ≪_ε N ^ (6 + ε) gives (a b c)² ≪_ε rad (a b c) ^ (6 + ε). As the largest of |a|, |b|, |c| is the sum of the other two, its square is at most 2 |a b c|, and this is the abc conjecture with exponent 3 / 2: max (|a|, |b|, |c|) ≪_ε rad (a b c) ^ (3 / 2 + ε). The exponent 3 / 2 is the one this argument gives; it is not claimed to be optimal.

Only the prime 2 needs care. Exactly one of a, b, c is even.

• If 16 divides it, the triple can be reordered and its signs changed so that the Frey curve is semistable, with minimal discriminant (a b c)² / 2⁸ and algorithmic conductor dividing rad (a b c) (TauCeti.isSemistable_freyCurve, TauCeti.minimalDiscriminantIdeal_freyCurve).
• Otherwise the Frey equation is globally minimal, with minimal discriminant 16 (a b c)² (TauCeti.minimalDiscriminantIdeal_freyCurve_of_not_dvd). Its reduction at 2 may be additive, but its algorithmic conductor still divides 2¹¹ rad (a b c) (TauCeti.algorithmicConductor_freyCurve_dvd).

Either way some elliptic curve over ℚ has (a b c)² ≤ 2⁸ |Δ_min| and N ≤ 2¹¹ rad (a b c), which is all that Szpiro's conjecture needs.

The conjectures are stated against the algorithmic conductor of Tate's algorithm, as in TauCeti/AlgebraicGeometry/EllipticCurve/Szpiro.lean, and neither is proved here.

Main results

• TauCeti.AlgorithmicSzpiroConjecture.exists_sq_le: under Szpiro's conjecture, (A B (A + B))² ≪_ε rad (A B (A + B)) ^ (6 + ε) for all coprime A and B with A B (A + B) ≠ 0.
• TauCeti.AlgorithmicSzpiroConjecture.abcConjectureWithExponent: Szpiro's conjecture implies the abc conjecture with exponent 3 / 2.

References

• J. Oesterlé, Nouvelles approches du « théorème » de Fermat, Séminaire Bourbaki 694 (1988), Astérisque 161–162 (1988), 165–186.
• G. Frey, Links between stable elliptic curves and certain Diophantine equations, Ann. Univ. Sarav. Ser. Math. 1 (1986), 1–40.

Szpiro's conjecture for all Frey curves

theorem TauCeti.exists_natAbs_sq_le_absNorm_minimalDiscriminantIdeal {A B : ℤ} (hAB : IsCoprime A B) (hP : A * B * (A + B) ≠ 0) : ∃ (E : WeierstrassCurve ℚ) (x : E.IsElliptic), (A * B * (A + B)).natAbs ^ 2 ≤ 2 ^ 8 * Ideal.absNorm (WeierstrassCurve.minimalDiscriminantIdeal ℤ E) ∧ Ideal.absNorm (WeierstrassCurve.algorithmicConductor ℤ E) ≤ 2 ^ 11 * UniqueFactorizationMonoid.radical (A * B * (A + B)).natAbs

Some Frey curve of a coprime triple has small conductor against its discriminant. For coprime integers A and B with A B (A + B) ≠ 0 there is an elliptic curve E over ℚ, the Frey curve of A, B and -(A + B) in a suitable order and with suitable signs, with (A B (A + B))² ≤ 2⁸ |Δ_min| and algorithmic conductor of norm at most 2¹¹ rad (A B (A + B)). If 16 ∣ A B (A + B) the curve can be chosen semistable; otherwise the Frey equation of A and B is globally minimal (TauCeti.minimalDiscriminantIdeal_freyCurve_of_not_dvd, TauCeti.algorithmicConductor_freyCurve_dvd).

theorem TauCeti.AlgorithmicSzpiroConjecture.exists_sq_le (h : AlgorithmicSzpiroConjecture) {ε : ℝ} (hε : 0 < ε) : ∃ (C : ℝ), ∀ (A B : ℤ), IsCoprime A B → A * B * (A + B) ≠ 0 → ↑(A * B * (A + B)) ^ 2 ≤ C * ↑(UniqueFactorizationMonoid.radical (A * B * (A + B)).natAbs) ^ (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 B (A + B) ≠ 0. This applies Szpiro's conjecture to the curve of TauCeti.exists_natAbs_sq_le_absNorm_minimalDiscriminantIdeal.

theorem TauCeti.AlgorithmicSzpiroConjecture.abcConjectureWithExponent (h : AlgorithmicSzpiroConjecture) : AbcConjectureWithExponent (3 / 2)

Szpiro's conjecture implies the abc conjecture with exponent 3 / 2: under TauCeti.AlgorithmicSzpiroConjecture, for every ε > 0 there is a constant C with max (|a|, |b|, |c|) ≤ C rad (a b c) ^ (3 / 2 + ε) for all coprime a + b = c. For coprime positive integers a + b = c, Szpiro's bound for Frey curves gives (a b c)² ≪_ε rad (a b c) ^ (6 + 4 ε) (TauCeti.AlgorithmicSzpiroConjecture.exists_sq_le), and c² ≤ 2 a b c because a + b ≤ 2 a b.