2. The Frey package and the four-way contradiction

A Frey package (Definitions/Def_FLTPrelim_FreyPackage.lean, adapted from the Imperial College London FLT project) is a structure bundling nonzero integers $a,b,c$, a prime $p\ge 5$, the equation $a^p+b^p=c^p$, and the normalisation $\gcd (a,b)=1$, $a\equiv 3(\mathrm{mod}4)$, $2\mid b$. The same file defines the Frey curve over ℚ,

$$E_P:y^2+xy=x^3+\frac{b^p-1-a^p}{4}{x}^2-\frac{a^p{b}^p}{16}x,$$

an integral model of $y^2=x(x-a^p)(x+b^p)$ (FreyPackage.freyCurve), and the same equation read over ℤ (FreyPackage.freyCurveInt).

• FreyPackage.of_counterexample — a solution in nonzero integers with prime exponent $p\ge 5$ yields Nonempty FreyPackage (permute and rescale to reach the normalisation); 73 lines citing only Mathlib.
• FreyPackage.no_frey_package (P : FreyPackage) : False — the heart. Apart from its imports, the wrapper namespace and the p2m_* name-resolution lines, its proof module is

theorem Wiles_Frey (P : FreyPackage) :
    ¬ GaloisRepIsIrreducible (K := AlgebraicClosure ℚ) ℚ P.freyCurve P.p := fun hirr =>
  let ⟨f, hf⟩ := level_lowering_to_two P (frey_isModular P) hirr
  hf (ModularForm.S2_Gamma0_2_eq_zero f)

theorem solution (P : FreyPackage) : False :=
  FreyPackage.Wiles_Frey P (FreyPackage.Mazur_Frey P)

So the contradiction rests on exactly four theorems — FreyPackage.Mazur_Frey (§3), FreyPackage.frey_isModular (§4), FreyPackage.level_lowering_to_two (§5) and ModularForm.S2_Gamma0_2_eq_zero (§6).