3. Irreducibility of the mod-p representation of the Frey curve

theorem FreyPackage.Mazur_Frey (P : FreyPackage) : GaloisRepIsIrreducible (K := AlgebraicClosure ℚ) ℚ P.freyCurve P.p

GaloisRepIsIrreducible (Definitions/Def_FLTPrelim_GaloisRep.lean) is basis-free: the $p$-torsion of $E_P(\overline{\mathbb{Q}})$ is nontrivial and its only Galois-stable $\mathbb{Z}/p$-submodules are $0$ and everything. The proof module first splits off the case $a\equiv 3(\mathrm{mod}8)$, which has its own argument at the prime 2 (FreyPackage.Mazur_Frey_of_a_mod_eight), and otherwise argues by contradiction: a reducible $E_P[p]$ has a Galois-stable line with trivial Galois action on the quotient — a cofixed line, HasGaloisStableCofixedLine (Definitions/Def_FLTPrelim_CofixedLine.lean) — by FreyPackage.frey_reducible_hasCofixedLine (Serre's observation that a stable line in $E_P[p]$ is fixed or cofixed, using that $E_P[p]$ is unramified away from $2p$ and that $E_P$ has no rational point of order $p$), and a cofixed line is ruled out separately in three ranges of $p$:

• p ≥ 17 — FreyPackage.frey_no_cofixed_large. This is Mazur's Eisenstein-ideal argument, and by far the largest part of this step: about 5,400 theorems lie below it, some 2,400 of them in the ModularCurve namespace. Its 1,400-line proof module cites 43 theorems: multiplicative reduction of the integral Frey model at every prime dividing $abc$; a local analysis of torsion points on and off the identity component at multiplicative primes and at $p$ (WeierstrassCurve.InZeroComponentAt, Definitions/Def_EllipticCurve_ZeroComponentAt.lean); Frobenius elements and the determinant of the torsion representation; and the one global input, WeierstrassCurve.mazurStepThree_not_inZeroComponentAt (Mazur's "Step 3": a rational point of prime order $p\notin \{2,3,5,7,13\}$ that is off the identity component at 2 and 3 is off it at every other multiplicative prime $\ell \ne p$), below which sit $X_0(N)$, its Jacobian, the cuspidal subgroup and the Eisenstein quotient (ModularCurve.eisensteinQuotientInvariantsFiniteAt_heckeModuleBar, ModularCurve.mazurQuotientSpecialization_heckeModuleBar, …), developed in the ModularCurve, AlgebraicGeometry and AlgebraicCurve namespaces.
• p = 11 — FreyPackage.frey_no_cofixed_eleven, and p ∈ {5, 7, 13} — FreyPackage.frey_no_cofixed_small. These are not arguments about elliptic curves: each is discharged by proving Fermat's Last Theorem for that exponent outright (fermatLastTheoremFive, …Seven, …Eleven, …Thirteen, each of type FermatLastTheoremFor n), so that no Frey package with that $p$ exists and the conclusion holds vacuously.
• fermatLastTheoremFive is a self-contained 2,000-line descent in $\mathbb{Z}[\frac{1+\sqrt{5}}{2}]$ citing only Mathlib.
• fermatLastTheoremSeven, …Eleven and …Thirteen each combine Kummer's theorem for regular primes, flt_regular {p : ℕ} [Fact p.Prime] (hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 (CyclotomicField p ℚ))))) (hodd : p ≠ 2) : FermatLastTheoremFor p (Theorems/Thm_flt_regular.lean; the proof module P2M/Sol/S_flt_regular.lean, about 4,200 lines citing only Mathlib, is a port of the flt-regular project — case I, case II, Kummer's lemma via Hilbert's theorems 90–94), with a proof that the ring of integers of the $p$-th cyclotomic field is a principal ideal domain: IsCyclotomicExtension.Rat.seven_pid, ….eleven_pid, ….thirteen_pid (the last about 730 lines).