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

9 declarations, 1 contain sorry, 0 declared as axioms

Sato–Tate conjecture

The Sato–Tate conjecture describes the distribution of the normalized Frobenius traces $a_p(E)/(2\sqrt{p})$ of a non-CM elliptic curve $E$ over $\mathbb{Q}$, as $p$ ranges over the primes of good reduction: they equidistribute in $[-1,1]$ with respect to the Sato–Tate measure $$ \frac{2}{\pi}\sqrt{1-x^2}\,dx. $$

Originally conjectured independently by Mikio Sato and John Tate around 1960, it is now a theorem: the case of elliptic curves over totally real fields with nonintegral $j$-invariant was established through the work of Clozel, Harris, and Taylor [CHT08], Taylor [Tay08], and Harris, Shepherd-Barron, and Taylor [HST10]. The remaining non-CM case was settled by Barnet-Lamb, Geraghty, Harris, and Taylor [BGHT11]. In particular, it holds unconditionally for every non-CM elliptic curve over $\mathbb{Q}$.

We use ModularityConjecture.WeierstrassCurve.ap, which agrees with the Frobenius trace at every prime where the supplied Weierstrass equation has integral coefficients and nonsingular reduction. Only finitely many primes are exceptional. Including these primes does not change the limiting density, so the formal statement averages over all primes below $N$.

The non-CM hypothesis is expressed using the classification of rational CM $j$-invariants. Complex multiplication here means complex multiplication over $\overline{\mathbb{Q}}$.

References

[CHT08] L. Clozel, M. Harris, R. Taylor, Automorphy for some $l$-adic lifts of automorphic mod $l$ Galois representations, Publications Mathématiques de l'IHÉS 108 (2008), 1–181. https://doi.org/10.1007/s10240-008-0016-1
[Tay08] R. Taylor, Automorphy for some $l$-adic lifts of automorphic mod $l$ Galois representations. II, Publications Mathématiques de l'IHÉS 108 (2008), 183–239. https://doi.org/10.1007/s10240-008-0015-2
[HST10] M. Harris, N. Shepherd-Barron, R. Taylor, A family of Calabi-Yau varieties and potential automorphy, Annals of Mathematics 171 (2010), no. 2, 779–813. https://doi.org/10.4007/annals.2010.171.779
[BGHT11] T. Barnet-Lamb, D. Geraghty, M. Harris, R. Taylor, A family of Calabi-Yau varieties and potential automorphy II, Publications of the Research Institute for Mathematical Sciences 47 (2011), no. 1, 29–98. https://doi.org/10.2977/PRIMS/31
Wikipedia

Imports (2)

def SatoTateConjecture.cmJInvariants The thirteen rational CM $j$-invariants, corresponding respectively to the imaginary quadratic orders of discriminants $-3,-4,-7,-8,-11,-12,-16,-19,-27,-28,-43,-67,-163$ line 76 source
Source documentation
The thirteen rational CM $j$-invariants, corresponding respectively to the imaginary quadratic orders of discriminants $-3,-4,-7,-8,-11,-12,-16,-19,-27,-28,-43,-67,-163$.

standard axioms: Quot.sound, propext what this means
Statement uses: Finset, Rat
Proof uses: Insert.insert, OfNat.ofNat, Neg.neg, Singleton.singleton
5 instances, coercions and auxiliary constants left out.
```
def cmJInvariants : Finset ℚ :=
…
```
def SatoTateConjecture.HasCM An elliptic curve $E$ over $\mathbb{Q}$ has complex multiplication over $\overline{\mathbb{Q}}$ if its $j$-invariant belongs to the set of thirteen rational CM $j$-invariants line 83 source
Source documentation
An elliptic curve $E$ over $\mathbb{Q}$ has complex multiplication over $\overline{\mathbb{Q}}$ if its $j$-invariant belongs to the set of thirteen rational CM $j$-invariants.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: WeierstrassCurve, Rat, WeierstrassCurve.IsElliptic
Proof uses: Membership.mem, Finset, SatoTateConjecture.cmJInvariants, WeierstrassCurve.j
4 instances, coercions and auxiliary constants left out.
```
def HasCM (E : WeierstrassCurve ℚ) [E.IsElliptic] : Prop :=
…
```
def SatoTateConjecture.normalisedAp The normalized coefficient $a_p(E)/(2\sqrt{p})$, using the point-counting definition from ModularityConjecture line 91 source
Source documentation
The normalized coefficient $a_p(E)/(2\sqrt{p})$, using the point-counting definition from ModularityConjecture.
At primes where the supplied equation has integral coefficients and nonsingular reduction, this is the normalized Frobenius trace and lies in $[-1,1]$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: WeierstrassCurve, Rat, WeierstrassCurve.IsElliptic, Nat, Real
Proof uses: HDiv.hDiv, ModularityConjecture.WeierstrassCurve.ap, HMul.hMul, OfNat.ofNat, Real.sqrt
13 instances, coercions and auxiliary constants left out.
```
noncomputable def normalisedAp
    (E : WeierstrassCurve ℚ) [E.IsElliptic] (p : ℕ) : ℝ :=
…
```
def SatoTateConjecture.satoTateCDF The cumulative distribution function of the Sato–Tate measure line 103 source
Source documentation
The cumulative distribution function of the Sato–Tate measure. For $t \in [-1,1]$, it is given by $$ F(t) = \frac{t\sqrt{1-t^2}+\arcsin t}{\pi}+\frac{1}{2}. $$ Mathlib's definitions of Real.sqrt and Real.arcsin make this expression equal to $0$ for $t \le -1$ and $1$ for $t \ge 1$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: HAdd.hAdd, HDiv.hDiv, HMul.hMul, Real.sqrt, HSub.hSub, OfNat.ofNat, HPow.hPow, Nat, Real.arcsin, Real.pi
19 instances, coercions and auxiliary constants left out.
```
noncomputable def satoTateCDF (t : ℝ) : ℝ :=
…
```
def SatoTateConjecture.satoTateMeasure For $a \le b$, the mass assigned to $[a,b]$ by the Sato–Tate distribution line 108 source
Source documentation
For $a \le b$, the mass assigned to $[a,b]$ by the Sato–Tate distribution. This is a real-valued interval mass, not a MeasureTheory.Measure object.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: HSub.hSub, SatoTateConjecture.satoTateCDF
2 instances, coercions and auxiliary constants left out.
```
noncomputable def satoTateMeasure (a b : ℝ) : ℝ :=
…
```
def SatoTateConjecture.satoTateIntegral For $a \le b$, the mass assigned to $[a,b]$ by the Sato–Tate distribution, written in its usual integral form $$ \frac{2}{\pi}\int_a^b \sqrt{1-x^2}\,dx. $$ line 116 source
Source documentation
For $a \le b$, the mass assigned to $[a,b]$ by the Sato–Tate distribution, written in its usual integral form $$ \frac{2}{\pi}\int_a^b \sqrt{1-x^2}\,dx. $$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: HMul.hMul, HDiv.hDiv, OfNat.ofNat, Real.pi, intervalIntegral, Real.sqrt, HSub.hSub, HPow.hPow, Nat, MeasureTheory.MeasureSpace.volume
23 instances, coercions and auxiliary constants left out.
```
noncomputable def satoTateIntegral (a b : ℝ) : ℝ :=
…
```
theorem SatoTateConjecture.satoTateMeasure_eq_satoTateIntegral Sanity check: for $-1 \le a \le b \le 1$, the closed-form interval mass satoTateMeasure agrees with the integral form satoTateIntegral line 122 source
Source documentation
Sanity check: for $-1 \le a \le b \le 1$, the closed-form interval mass satoTateMeasure agrees with the integral form satoTateIntegral.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LE.le, Neg.neg, OfNat.ofNat, Eq, SatoTateConjecture.satoTateMeasure, SatoTateConjecture.satoTateIntegral
Proof uses: Membership.mem, Set, Set.Ioo, HasDerivAt, SatoTateConjecture.satoTateCDF, HMul.hMul, HDiv.hDiv, Nat, Real.pi, Real.sqrt, HSub.hSub, HPow.hPow, LT.lt, LE.le.trans_lt, And.left, LT.lt.trans_le, And.right, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp and 114 more
183 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
theorem satoTateMeasure_eq_satoTateIntegral
    (a b : ℝ) (ha : -1 ≤ a) (hab : a ≤ b) (hb : b ≤ 1) :
    satoTateMeasure a b = satoTateIntegral a b := by
…
```
Mentions: SatoTateConjecture.satoTateMeasure, SatoTateConjecture.satoTateIntegral
def SatoTateConjecture.primeCountInInterval The number of primes $p < N$ for which the normalized coefficient belongs to $[a,b]$ line 149 source
Source documentation
The number of primes $p < N$ for which the normalized coefficient belongs to $[a,b]$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: WeierstrassCurve, Rat, WeierstrassCurve.IsElliptic, Real, Nat
Proof uses: Finset.card, Finset.filter, And, LE.le, SatoTateConjecture.normalisedAp, Nat.primesBelow
5 instances, coercions and auxiliary constants left out.
```
noncomputable def primeCountInInterval
    (E : WeierstrassCurve ℚ) [E.IsElliptic] (a b : ℝ) (N : ℕ) : ℕ :=
…
```
theorem SatoTateConjecture.satoTate_conjecture The Sato–Tate conjecture: for a non-CM elliptic curve sorry line 169 source
Source documentation
The Sato–Tate conjecture: for a non-CM elliptic curve $E$ over $\mathbb{Q}$ and $-1 \le a \le b \le 1$, the proportion of primes $p < N$ whose normalized coefficient belongs to $[a,b]$ tends to $$ \frac{2}{\pi}\int_a^b \sqrt{1-x^2}\,dx $$ as $N \to \infty$.
The finitely many primes where the supplied equation fails to have integral coefficients and nonsingular reduction do not affect this limit.
Established through the work of Clozel–Harris–Taylor [CHT08], Taylor [Tay08], Harris–Shepherd-Barron–Taylor [HST10], and Barnet-Lamb–Geraghty–Harris–Taylor [BGHT11].

depends on sorry what this means
Statement uses: WeierstrassCurve, Rat, WeierstrassCurve.IsElliptic, Not, SatoTateConjecture.HasCM, Real, LE.le, Neg.neg, OfNat.ofNat, Filter.Tendsto, Nat, HDiv.hDiv, SatoTateConjecture.primeCountInInterval, Finset.card, Nat.primesBelow, Filter.atTop, nhds, SatoTateConjecture.satoTateMeasure
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
29 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem satoTate_conjecture
    (E : WeierstrassCurve ℚ) [E.IsElliptic] (hCM : ¬ HasCM E)
    (a b : ℝ) (ha : -1 ≤ a) (hab : a ≤ b) (hb : b ≤ 1) :
    Filter.Tendsto
      (fun N : ℕ ↦
        (primeCountInInterval E a b N : ℝ) /
          ((Nat.primesBelow N).card : ℝ))
      Filter.atTop
      (nhds (satoTateMeasure a b)) := by
…
```
Mentions: SatoTateConjecture.HasCM, SatoTateConjecture.primeCountInInterval, SatoTateConjecture.satoTateMeasure