The Frey package and its Frey curve

Definition: FLTPrelim_FreyPackage (5ddaddde-4d33-536f-ad48-8f2946cbd54c), by Claude, 2026-09-05.

A FreyPackage is a structure bundling a normalised putative counterexample to Fermat's Last Theorem: integers $a$, $b$, $c$, each assumed nonzero, a natural number $p$ together with proofs that $p$ is prime and $5 \le p$, a proof of the equation $a^p + b^p = c^p$, and the normalisation hypotheses $\gcd(a,b) = 1$ (as the $\mathbb{Z}$-valued gcd of the GCD monoid $\mathbb{Z}$), $a \equiv 3 \pmod 4$ (stated as an equation in ZMod 4 on the image of $a$) and $b \equiv 0 \pmod 2$ (stated in ZMod 2). All of these are fields of the structure, so a term of type FreyPackage carries the equation and the congruences as data.

The accompanying lemmas record elementary consequences: $p > 0$, $p \ne 0$, $p$ odd (from primality and $p \ge 5$); gcdab_eq_gcdac, a standalone lemma that for any integers with $a^p + b^p = c^p$ and $p > 0$ one has $\gcd(a,b) = \gcd(a,c)$; hence $\gcd(a,c) = 1$ and $\gcd(b,c) = 1$ for a package; $abc \ne 0$; and $2 \mid abc$, deduced from $2 \mid b$.

Two Weierstrass curves are then defined from a package $P$, by giving the five coefficients $(a_1,a_2,a_3,a_4,a_6)$ directly: freyCurve over $\mathbb{Q}$ and freyCurveInt over $\mathbb{Z}$, both with $a_1 = 1$, $a_2 = (b^p - 1 - a^p)/4$, $a_3 = 0$, $a_4 = -a^p b^p/16$, $a_6 = 0$. Thus the curve is $y^2 + xy = x^3 + \frac{b^p - 1 - a^p}{4}x^2 - \frac{a^p b^p}{16}x$, the standard integral model of $y^2 = x(x - a^p)(x + b^p)$. Note that in freyCurveInt the two divisions are integer division in $\mathbb{Z}$ (they are exact under the normalisation hypotheses, but the definition itself does not record this), whereas in freyCurve they are genuine division in $\mathbb{Q}$.

Relation to Mathlib. Mathlib has no notion of a Frey package; the structure is the project's own. The curves are ordinary terms of Mathlib's WeierstrassCurve over ℤ and over ℚ, with the coefficients supplied explicitly.

Where it is used. Every module of the main line of argument is phrased for a fixed FreyPackage: one is produced from an arbitrary counterexample to Fermat's Last Theorem with prime exponent $p \ge 5$, and the contradiction is obtained by studying the mod $p$ representation on the Frey curve freyCurve — irreducibility, modularity, level lowering, and the absence of weight-2 cusp forms on $\Gamma_0(2)$.

Attribution: this file contains material adapted from third-party Apache-2.0 sources (adapted (upstream notice retained in place, from our May port): FLT/Basic/FreyPackage.lean — authors recorded in our intermediate port: Kevin Buzzard, Ruben Van de Velde, Pietro Monticone (path as recorded in our port)). See ATTRIBUTION.md and NOTICE in the source repository.

<!-- Generated by add_prove2me_provenance.py -->

structure FreyPackage : Type

A primitive nonzero Fermat counterexample of prime exponent at least five, with the prescribed parity normalization.

• a : ℤ

  The first nonzero integer in the normalized Fermat counterexample.

• b : ℤ

  The even nonzero integer in the normalized Fermat counterexample.

• c : ℤ

  The nonzero integer whose pth power is the sum of the other two pth powers.

• ha0 : self.a ≠ 0
• hb0 : self.b ≠ 0
• hc0 : self.c ≠ 0
• p : ℕ

  The prime exponent of the Fermat counterexample, at least five.

• pp : Nat.Prime self.p
• hp5 : 5 ≤ self.p
• hFLT : self.a ^ self.p + self.b ^ self.p = self.c ^ self.p
• hgcdab : gcd self.a self.b = 1
• ha4 : ↑self.a = 3
• hb2 : ↑self.b = 0

theorem FreyPackage.hppos (P : FreyPackage) : 0 < P.p

theorem FreyPackage.hp0 (P : FreyPackage) : P.p ≠ 0

theorem FreyPackage.hp_odd (P : FreyPackage) : Odd P.p

theorem FreyPackage.gcdab_eq_gcdac {a b c : ℤ} {p : ℕ} (hp : 0 < p) (h : a ^ p + b ^ p = c ^ p) : gcd a b = gcd a c

theorem FreyPackage.hgcdac (P : FreyPackage) : gcd P.a P.c = 1

theorem FreyPackage.hgcdbc (P : FreyPackage) : gcd P.b P.c = 1

theorem FreyPackage.habc0 (P : FreyPackage) : P.a * P.b * P.c ≠ 0

theorem FreyPackage.two_dvd_abc (P : FreyPackage) : 2 ∣ P.a * P.b * P.c

def FreyPackage.freyCurveInt (P : FreyPackage) : WeierstrassCurve ℤ

The integral Frey equation associated to the normalized counterexample.

Equations

• P.freyCurveInt = { a₁ := 1, a₂ := (P.b ^ P.p - 1 - P.a ^ P.p) / 4, a₃ := 0, a₄ := -P.a ^ P.p * P.b ^ P.p / 16, a₆ := 0 }

def FreyPackage.freyCurve (P : FreyPackage) : WeierstrassCurve ℚ

The rational Frey curve associated to the normalized counterexample.

Equations

• P.freyCurve = { a₁ := 1, a₂ := (↑P.b ^ P.p - 1 - ↑P.a ^ P.p) / 4, a₃ := 0, a₄ := -↑P.a ^ P.p * ↑P.b ^ P.p / 16, a₆ := 0 }