Weierstrass.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

5 declarations, 0 contain sorry, 0 declared as axioms

Complements on Weierstrass curves

Material for Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass: ellipticity of base changes, the discriminant identity behind split multiplicative reduction, c₆ = 0 ↔ j = 1728, and a₁ ≠ 0 ∨ a₃ ≠ 0 in characteristic 2.

Imports (1)

Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Imported by 3 files

instance WeierstrassCurve.(instance at line 27) line 27 source
Source documentation
The base change of an elliptic curve is an elliptic curve. Restates the instance for WeierstrassCurve.map, which does not apply to baseChange directly since the latter is a non-reducible definition.
```
instance {R A : Type*} [CommRing R] [CommRing A] [Algebra R A] (W : WeierstrassCurve R)
    [W.IsElliptic] : (W.baseChange A).IsElliptic :=
…
```
theorem WeierstrassCurve.splitPolynomial_discrim The discriminant of the node's tangent polynomial c₄ T² + a₁ c₄ T - (54 b₆ - 3 b₂ b₄ + a₂ c₄) (the quadratic controlling split multiplicative reduction) equals -c₄ c₆ line 40 source
Source documentation
The discriminant of the node's tangent polynomial c₄ T² + a₁ c₄ T - (54 b₆ - 3 b₂ b₄ + a₂ c₄) (the quadratic controlling split multiplicative reduction) equals -c₄ c₆. Hence the tangent directions at the node are rational over the residue field exactly when -c₄ c₆ is a square there; twisting by (t, n) multiplies -c₄ c₆ by (t² - 4n)⁵ = (t² - 4n)⁴ · (t² - 4n), i.e. by the twisting parameter up to a square (see c₄_quadraticTwistOf, c₆_quadraticTwistOf).

standard axioms: Quot.sound, propext what this means
Statement uses: CommRing, WeierstrassCurve, Eq, HAdd.hAdd, HPow.hPow, Nat, HMul.hMul, WeierstrassCurve.a₁, WeierstrassCurve.c₄, OfNat.ofNat, HSub.hSub, WeierstrassCurve.b₆, WeierstrassCurve.b₂, WeierstrassCurve.b₄, WeierstrassCurve.a₂, Neg.neg, WeierstrassCurve.c₆
Proof uses: id, Mathlib.Tactic.Ring.of_eq, WeierstrassCurve.a₄, WeierstrassCurve.a₃, WeierstrassCurve.a₆, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, inferInstance, Ring, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, congrArg, Eq.symm, Eq.refl and 47 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem splitPolynomial_discrim :
    (E.a₁ * E.c₄) ^ 2 + 4 * E.c₄ * (54 * E.b₆ - 3 * E.b₂ * E.b₄ + E.a₂ * E.c₄)
      = -(E.c₄ * E.c₆) := by
…
```
lemma WeierstrassCurve.a₁_ne_zero_or_a₃_ne_zero_of_two_eq_zero In characteristic 2, an elliptic curve has a₁ ≠ 0 or a₃ ≠ 0: otherwise a₁ = a₃ = 0 makes the partial derivative ∂/∂y = 2y + a₁x + a₃ vanish identically, so Δ = 0 line 51 source
Source documentation
In characteristic 2, an elliptic curve has a₁ ≠ 0 or a₃ ≠ 0: otherwise a₁ = a₃ = 0 makes the partial derivative ∂/∂y = 2y + a₁x + a₃ vanish identically, so Δ = 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, WeierstrassCurve.IsElliptic, Eq, OfNat.ofNat, Nat, Or, Ne, WeierstrassCurve.a₁, WeierstrassCurve.a₃
Proof uses: Classical.byContradiction, Not, IsUnit.ne_zero, WeierstrassCurve.Δ, WeierstrassCurve.isUnit_Δ, Eq.mpr, HAdd.hAdd, HSub.hSub, HMul.hMul, Neg.neg, HPow.hPow, WeierstrassCurve.b₂, WeierstrassCurve.b₈, WeierstrassCurve.b₄, WeierstrassCurve.b₆, id, congrArg, WeierstrassCurve.Δ.eq_1, WeierstrassCurve.a₆, WeierstrassCurve.a₂ and 11 more
66 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma a₁_ne_zero_or_a₃_ne_zero_of_two_eq_zero [E.IsElliptic] (h2 : (2 : K) = 0) :
    E.a₁ ≠ 0 ∨ E.a₃ ≠ 0 := by
…
```
lemma WeierstrassCurve.c₆_eq_zero_iff_j_eq_1728 c₆(E) = 0 if and only if j(E) = 1728, by the relation 1728·Δ = c₄³ - c₆² line 58 source
Source documentation
c₆(E) = 0 if and only if j(E) = 1728, by the relation 1728·Δ = c₄³ - c₆². This is the analogue for j = 1728 of WeierstrassCurve.j_eq_zero_iff (j = 0 ↔ c₄ = 0).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, WeierstrassCurve.IsElliptic, Iff, Eq, WeierstrassCurve.c₆, OfNat.ofNat, WeierstrassCurve.j, Nat
Proof uses: HPow.hPow, HSub.hSub, WeierstrassCurve.c₄, HMul.hMul, WeierstrassCurve.Δ, Mathlib.Tactic.LinearCombination.eq_of_eq, WeierstrassCurve.c_relation, Mathlib.Tactic.LinearCombination.eq_rearrange, HAdd.hAdd, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.sub_congr, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl and 56 more
81 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma c₆_eq_zero_iff_j_eq_1728 [E.IsElliptic] : E.c₆ = 0 ↔ E.j = 1728 := by
…
```
lemma WeierstrassCurve.baseChange_map_algebraMap line 68 source
standard axioms: Quot.sound, propext what this means
Statement uses: Field, Algebra, IsScalarTower, WeierstrassCurve, Eq, WeierstrassCurve.map, WeierstrassCurve.baseChange, Algebra.algebraMap
Proof uses: WeierstrassCurve.map_baseChange, IsScalarTower.toAlgHom
19 instances, coercions and auxiliary constants left out.