Basic.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 1204 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned FLT blueprint introduction

13 declarations, 0 contain sorry, 0 declared as axioms

The Frey curve associated to a Frey package

Recall that a Frey package is a triple of nonzero integers a, b, c and a prime p satisfying some conditions, most notably that a^p+b^p=c^p.

In this file we define the elliptic curve E : Y^2=X(X-a^p)(X+b^p) associated to the Frey package.

All the results in Section 4.1 of Serre's 1987 Duke paper [Serre] apply to this elliptic curve Y^2=X(X-a^p)(X+b^p).

Main definition

FreyPackage.freyCurve : The Frey curve associated to a Frey package.

Main theorem

FreyCurve.j_valuation_of_bad_prime : The q-adic valuation of the j-invariant of the Frey curve is a multiple of q if 2 < q is a prime of bad reduction.

Imports (1)

FLT.FreyCurve.FreyPackage

Imported by 4 files

def FreyPackage.freyCurveInt The Weierstrass curve over ℤ associated to a Frey package line 47 source
Source documentation
The Weierstrass curve over ℤ associated to a Frey package. The conditions imposed upon a Frey package guarantee that the running hypotheses in Section 4.1 of [Serre] all hold. We put the curve into the form where the equation is semistable at 2, rather than the usual Y^2=X(X-a^p)(X+b^p) form. The change of variables is X=4x and Y=8y+4x, and then divide through by 64. The fact that p is odd, a=3 mod 4 and b is even are enough to show that this new curve still has coefficients in ℤ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: FreyPackage, WeierstrassCurve, Int
Proof uses: WeierstrassCurve.mk, OfNat.ofNat, HDiv.hDiv, HSub.hSub, HPow.hPow, Nat, FreyPackage.b, FreyPackage.p, FreyPackage.a, HMul.hMul, Neg.neg
12 instances, coercions and auxiliary constants left out.
```
def freyCurveInt (P : FreyPackage) : WeierstrassCurve ℤ where
…
```
Mentions: FreyPackage
def FreyPackage.freyCurve The elliptic curve over ℚ associated to a Frey package line 60 source
Source documentation
The elliptic curve over ℚ associated to a Frey package. The conditions imposed upon a Frey package guarantee that the running hypotheses in Section 4.1 of [Serre] all hold. We put the curve into the form where the equation is semistable at 2, rather than the usual Y^2=X(X-a^p)(X+b^p) form. The change of variables is X=4x and Y=8y+4x, and then divide through by 64.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: FreyPackage, WeierstrassCurve, Rat
Proof uses: WeierstrassCurve.mk, OfNat.ofNat, HDiv.hDiv, HSub.hSub, HPow.hPow, Nat, FreyPackage.b, FreyPackage.p, FreyPackage.a, HMul.hMul, Neg.neg
12 instances, coercions and auxiliary constants left out.
```
def freyCurve (P : FreyPackage) : WeierstrassCurve ℚ where
…
```
Mentions: FreyPackage
theorem FreyCurve.map line 74 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: FreyPackage, Eq, WeierstrassCurve, Rat, WeierstrassCurve.map, Int, FreyPackage.freyCurveInt, Algebra.algebraMap, FreyPackage.freyCurve
Proof uses: Dvd.dvd, OfNat.ofNat, FreyPackage.b, Iff.mp, ZMod, Nat, ZMod.intCast_zmod_eq_zero_iff_dvd, FreyPackage.hb2, WeierstrassCurve.ext, Eq.refl, WeierstrassCurve.a₁, id, WeierstrassCurve.a₂, Eq.mpr, HDiv.hDiv, HSub.hSub, HPow.hPow, FreyPackage.p, FreyPackage.a, congrArg and 98 more
137 instances, coercions and auxiliary constants left out.

Tactic trace: 38 steps
Open to load the checked before-and-after goal states.
lemma FreyCurve.Δ line 104 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: FreyPackage, Eq, Rat, WeierstrassCurve.Δ, FreyPackage.freyCurve, HDiv.hDiv, HPow.hPow, Nat, HMul.hMul, FreyPackage.a, FreyPackage.b, FreyPackage.c, OfNat.ofNat, FreyPackage.p
Proof uses: Trans.simple, Eq.mpr, inferInstance, CommGroupWithZero, GroupWithZero, id, Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq, Mathlib.Tactic.FieldSimp.NF.eval, Mathlib.Tactic.FieldSimp.NF.cons, Prod.mk, Int, Neg.neg, List.nil, Prod, Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul, rfl, Eq.trans, Eq.refl, Mathlib.Tactic.FieldSimp.NF.atom_eq_eval, Eq.symm and 157 more
157 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
instance FreyCurve.(instance at line 112) line 112 source
lemma FreyCurve.b₂ line 120 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: FreyPackage, Eq, Rat, WeierstrassCurve.b₂, FreyPackage.freyCurve, HSub.hSub, HPow.hPow, Nat, FreyPackage.b, FreyPackage.p, FreyPackage.a
Proof uses: Eq.mpr, HAdd.hAdd, OfNat.ofNat, HMul.hMul, HDiv.hDiv, id, congrFun', congrArg, congr, WeierstrassCurve.a₁, WeierstrassCurve.a₂, Eq.trans, WeierstrassCurve, WeierstrassCurve.mk, Neg.neg, neg_mul, one_pow, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne' and 68 more
78 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma FreyCurve.b₄ line 125 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: FreyPackage, Eq, Rat, WeierstrassCurve.b₄, FreyPackage.freyCurve, HDiv.hDiv, Neg.neg, HPow.hPow, Nat, HMul.hMul, FreyPackage.a, FreyPackage.b, FreyPackage.p, OfNat.ofNat
Proof uses: Eq.mpr, id, congrFun', congrArg, Eq.trans, HAdd.hAdd, WeierstrassCurve.a₄, WeierstrassCurve.a₁, WeierstrassCurve.a₃, congr, WeierstrassCurve, WeierstrassCurve.mk, HSub.hSub, neg_mul, MulZeroClass.mul_zero, add_zero, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Rat.rawCast, Int.negOfNat and 54 more
80 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma FreyCurve.c₄ line 130 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: FreyPackage, Eq, Rat, WeierstrassCurve.c₄, FreyPackage.freyCurve, HAdd.hAdd, HPow.hPow, Nat, FreyPackage.a, FreyPackage.p, OfNat.ofNat, HMul.hMul, FreyPackage.b
Proof uses: Eq.mpr, HSub.hSub, HDiv.hDiv, Neg.neg, id, congrFun', congrArg, congr, WeierstrassCurve.b₂, WeierstrassCurve.b₄, FreyCurve.b₂, FreyCurve.b₄, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, inferInstance, Ring, Mathlib.Tactic.Ring.Common.sub_congr, Int.rawCast, Int.negOfNat and 70 more
77 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma FreyCurve.c₄' line 135 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: FreyPackage, Eq, Rat, WeierstrassCurve.c₄, FreyPackage.freyCurve, HSub.hSub, HPow.hPow, Nat, FreyPackage.c, HMul.hMul, OfNat.ofNat, FreyPackage.p, FreyPackage.a, FreyPackage.b
Proof uses: Eq.mpr, HAdd.hAdd, id, congrArg, FreyCurve.c₄, Int, Eq.trans, congr, congrFun', pow_mul', Eq.symm, FreyPackage.hFLT, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.refl, Mathlib.Tactic.Ring.Common.pow_add and 48 more
68 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma FreyCurve.Δ'inv line 141 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: FreyPackage, Eq, Rat, Inv.inv, Units, WeierstrassCurve.Δ', FreyPackage.freyCurve, HDiv.hDiv, HPow.hPow, Nat, OfNat.ofNat, HMul.hMul, FreyPackage.a, FreyPackage.b, FreyPackage.c, FreyPackage.p
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Units.val_inv_eq_inv_val, FreyCurve.Δ, inv_div, eq_self
49 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma FreyCurve.j line 145 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: FreyPackage, Eq, Rat, WeierstrassCurve.j, FreyPackage.freyCurve, HDiv.hDiv, HMul.hMul, HPow.hPow, Nat, OfNat.ofNat, HSub.hSub, FreyPackage.c, FreyPackage.p, FreyPackage.a, FreyPackage.b
Proof uses: Eq.mpr, id, congrArg, mul_div_right_comm, Inv.inv, Units, WeierstrassCurve.Δ', WeierstrassCurve.c₄, WeierstrassCurve.j.eq_1, FreyCurve.Δ'inv, FreyCurve.c₄', Eq.refl
52 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma FreyCurve.j_pos_aux line 149 source
lemma FreyCurve.j_valuation_of_bad_prime The q-adic valuation of the j-invariant of the Frey curve is a multiple of p if 2 < q is a prime of bad reduction line 157 source
Source documentation
The q-adic valuation of the j-invariant of the Frey curve is a multiple of p if 2 < q is a prime of bad reduction.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: FreyPackage, Nat, Nat.Prime, Dvd.dvd, Int, HMul.hMul, FreyPackage.a, FreyPackage.b, FreyPackage.c, LT.lt, OfNat.ofNat, FreyPackage.p, padicValRat, WeierstrassCurve.j, Rat, FreyPackage.freyCurve
Proof uses: Fact, Fact.mk, Prime, Iff.mp, Nat.prime_iff_prime_int, Ne, HPow.hPow, HSub.hSub, Eq.mpr, Not, Eq, id, Eq.trans, congrArg, Eq.symm, Nat.cast_zero, congrFun', congr, Int.cast_zero, pow_mul' and 69 more
151 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
```
lemma j_valuation_of_bad_prime (P : FreyPackage) {q : ℕ} (hqPrime : q.Prime)
    (hqbad : (q : ℤ) ∣ P.a * P.b * P.c) (hqodd : 2 < q) :
    (P.p : ℤ) ∣ padicValRat q P.freyCurve.j := by
…
```
Mentions: FreyPackage