GlobalPeriod.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 10 curated AI-written annotations and 7190 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, Formal Conjectures paper, arXiv v1

4 declarations, 0 contain sorry, 0 declared as axioms

The real and complex periods of an elliptic curve as integrals

Let $E$ be an elliptic curve with Weierstrass equation $y^2 + a_1 xy + a_3 y = x^3 + a_2 x^2 + a_4 x + a_6$ and invariant differential $\omega = \frac{dx}{2y + a_1 x + a_3}$. Completing the square, $(2y + a_1 x + a_3)^2 = 4x^3 + b_2 x^2 + 2 b_4 x + b_6 =: F(x)$, the 2-division polynomial WeierstrassCurve.Ψ₂Sq, so $|\omega| = |dx| / \sqrt{|F(x)|}$ on the $x$-line.

Over $\mathbb{R}$ (a curve W : WeierstrassCurve ℝ), the real locus $E(\mathbb{R})$ lies over $\{F \geq 0\}$ with two branches $2y + a_1 x + a_3 = \pm\sqrt{F(x)}$, so the real period is $\Omega_{\mathbb{R}} = \int_{E(\mathbb{R})} |\omega| = 2 \int_{\mathbb{R}} dx / \sqrt{F(x)}$ (WeierstrassCurve.realPeriod).
Over $\mathbb{C}$ (a curve W : WeierstrassCurve ℂ), the $x$-coordinate is a double cover $E(\mathbb{C}) \to \mathbb{P}^1(\mathbb{C})$ and $|\omega \wedge \bar\omega| = 4\, dA(x) / |F(x)|$ on each sheet, so the complex period is $\Omega_{\mathbb{C}} = \int_{E(\mathbb{C})} |\omega \wedge \bar\omega| = 4 \int_{\mathbb{C}} dA(x) / |F(x)|$ (WeierstrassCurve.complexPeriod).

References:

LMFDB, knowl ec.period
[Sil09] Silverman, J. H., The Arithmetic of Elliptic Curves, 2nd ed., Graduate Texts in Mathematics 106, Springer, 2009. Chapter III §1 (Weierstrass equations, the invariant differential) and Chapter VI (elliptic curves over $\mathbb{C}$).

Imports (4)

Imported by 1 file

FormalConjecturesForMathlib.lean

def WeierstrassCurve.realPeriodIntegrand Documented declaration: realPeriodIntegrand line 60 source
Source documentation
The density $|\omega| / dx = 1 / \sqrt{4x^3 + b_2 x^2 + 2 b_4 x + b_6}$ of the invariant differential on either branch of the real locus, as a function on $\mathbb{R}$, with the junk value $0$ where the cubic is not positive.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: WeierstrassCurve, Real
Proof uses: Inv.inv, Real.sqrt, Polynomial.eval, WeierstrassCurve.Ψ₂Sq
4 instances, coercions and auxiliary constants left out.
```
def realPeriodIntegrand (x : ℝ) : ℝ := (√(W.Ψ₂Sq.eval x))⁻¹
```
def WeierstrassCurve.realPeriod Documented declaration: realPeriod line 66 source
Source documentation
The real period as an integral: the integral of $|\omega|$ over the real locus $E(\mathbb{R})$, that is $2 \int_{\mathbb{R}} dx / \sqrt{F(x)}$ with the integrand taken to be $0$ where $F \leq 0$. This is the real period of the Birch and Swinnerton-Dyer conjecture, in the convention that absorbs the real Tamagawa number.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: WeierstrassCurve, Real
Proof uses: HMul.hMul, OfNat.ofNat, MeasureTheory.integral, MeasureTheory.MeasureSpace.volume, WeierstrassCurve.realPeriodIntegrand
12 instances, coercions and auxiliary constants left out.
```
def realPeriod : ℝ := 2 * ∫ x, W.realPeriodIntegrand x
…
```
def WeierstrassCurve.complexPeriodIntegrand The density of $\Omega_{\mathbb{C}}$ on the $x$-line: $1 / |\Psi_2^2(x)|$ line 75 source
Source documentation
The density of $\Omega_{\mathbb{C}}$ on the $x$-line: $1 / |\Psi_2^2(x)|$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: WeierstrassCurve, Complex, Real
Proof uses: Inv.inv, Norm.norm, Polynomial.eval, WeierstrassCurve.Ψ₂Sq
5 instances, coercions and auxiliary constants left out.
```
def complexPeriodIntegrand (x : ℂ) : ℝ := ‖W.Ψ₂Sq.eval x‖⁻¹
```
def WeierstrassCurve.complexPeriod The complex period as an integral: $\Omega_{\mathbb{C}}(E) = \int_{E(\mathbb{C})} |\omega \wedge \bar\omega| = 4 \int_{\mathbb{C}} dA(x) / |\Psi_2^2(x)|$ line 80 source
Source documentation
The complex period as an integral: $\Omega_{\mathbb{C}}(E) = \int_{E(\mathbb{C})} |\omega \wedge \bar\omega| = 4 \int_{\mathbb{C}} dA(x) / |\Psi_2^2(x)|$. Source: LMFDB knowl ec.period.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: WeierstrassCurve, Complex, Real
Proof uses: HMul.hMul, OfNat.ofNat, MeasureTheory.integral, MeasureTheory.MeasureSpace.volume, WeierstrassCurve.complexPeriodIntegrand
18 instances, coercions and auxiliary constants left out.
```
def complexPeriod : ℝ := 4 * ∫ x : ℂ, W.complexPeriodIntegrand x
…
```