Schur–Siegel–Smyth trace problem

DefinitionConjugates#✓fully proved

The conjugates of a complex number \(\alpha\) are the roots in \(\mathbb{C}\) of its minimal polynomial over \(\mathbb{Q}\), counted with multiplicity. If \(\alpha\) is transcendental, its minimal polynomial is taken to be \(0\) and it has no conjugates.

noncomputable def conjugates (α : ℂ) : Multiset ℂ :=
  (minpoly ℚ α).aroots ℂ

Used by 6

Used byPositivity of the absolute trace · Totally positive algebraic integers · One is a totally positive algebraic integer · Trace as the sum of conjugates · The trace of a totally positive algebraic integer is real · The trace of a totally positive algebraic integer has positive real part

DefinitionDegree of a complex number#✓fully proved

The degree of a complex number \(\alpha\) is the degree of its minimal polynomial over \(\mathbb{Q}\). If \(\alpha\) is transcendental, its minimal polynomial is taken to be \(0\), so its degree is \(0\).

noncomputable def degree (α : ℂ) : ℕ :=
  (minpoly ℚ α).natDegree

Used by 2

Used byAbsolute trace · Positivity of the absolute trace

DefinitionTrace as the sum of conjugates#✓fully proved

For \(\alpha \in \mathbb{C}\), the trace of \(\alpha\) is the sum of its conjugates, that is, of the roots in \(\mathbb{C}\) of the minimal polynomial of \(\alpha\) over \(\mathbb{Q}\), counted with multiplicity. For transcendental \(\alpha\) there are no conjugates and the trace is \(0\).

noncomputable def trace (α : ℂ) : ℂ :=
  (conjugates α).sum

Uses 1 · Used by 4

Statement usesConjugates

Used byAbsolute trace · Positivity of the absolute trace · The trace of a totally positive algebraic integer is real · The trace of a totally positive algebraic integer has positive real part

DefinitionAbsolute trace#✓fully proved

The absolute trace of a complex number \(\alpha\) is the real number obtained by dividing the real part of the trace of \(\alpha\) by the degree of \(\alpha\). If \(\alpha\) is transcendental, its trace and its degree are both \(0\), and its absolute trace is taken to be \(0\).

For algebraic \(\alpha\) the trace is real, and for a totally positive algebraic integer \(\alpha\) the absolute trace is the mean of the conjugates of \(\alpha\).

noncomputable def absoluteTrace (α : ℂ) : ℝ :=
  (trace α).re / degree α

Uses 2 · Used by 3

Statement usesDegree of a complex number · Trace as the sum of conjugates

Used byAbsolute trace of a totally positive algebraic integer is at least one · Positivity of the absolute trace · Admissible trace bounds

DefinitionTotally positive algebraic integers#✓fully proved

A complex number \(\alpha\) is a totally positive algebraic integer when it is integral over \(\mathbb{Z}\) and every conjugate of \(\alpha\) (every root in \(\mathbb{C}\) of its minimal polynomial over \(\mathbb{Q}\)) is a strictly positive real number.

def IsTotallyPositive (α : ℂ) : Prop :=
  IsIntegral ℤ α ∧ ∀ β ∈ conjugates α, β.im = 0 ∧ 0 < β.re

Uses 1 · Used by 6

Statement usesConjugates

Used byAbsolute trace of a totally positive algebraic integer is at least one · Positivity of the absolute trace · Admissible trace bounds · One is a totally positive algebraic integer · The trace of a totally positive algebraic integer is real · The trace of a totally positive algebraic integer has positive real part

TheoremThe trace of a totally positive algebraic integer has positive real part#✓fully proved

If \(\alpha \in \mathbb{C}\) is a totally positive algebraic integer, then the real part of the trace of \(\alpha\) is strictly positive.

theorem trace_pos_re {α : ℂ} (hα : IsTotallyPositive α) :
    0 < (trace α).re

Uses 3 · Used by 1

Statement usesTotally positive algebraic integers · Trace as the sum of conjugates

Proof usesConjugates

Used byPositivity of the absolute trace

TheoremThe trace of a totally positive algebraic integer is real#✓fully proved

If \(\alpha \in \mathbb{C}\) is a totally positive algebraic integer, then the imaginary part of the trace of \(\alpha\) is \(0\).

theorem trace_im_eq_zero {α : ℂ} (hα : IsTotallyPositive α) :
    (trace α).im = 0

Uses 3

Statement usesTotally positive algebraic integers · Trace as the sum of conjugates

Proof usesConjugates

TheoremPositivity of the absolute trace#✓fully proved

If a complex number \(\alpha\) is a totally positive algebraic integer, then the absolute trace of \(\alpha\) is strictly positive.

theorem absoluteTrace_pos {α : ℂ} (hα : IsTotallyPositive α) :
    0 < absoluteTrace α

Uses 6

Statement usesTotally positive algebraic integers · Absolute trace

Proof usesConjugates · Degree of a complex number · Trace as the sum of conjugates · The trace of a totally positive algebraic integer has positive real part

TheoremMinimal polynomial of one#✓fully proved

The minimal polynomial of \(1 \in \mathbb{C}\) over \(\mathbb{Q}\) is \(X - 1\).

theorem minpoly_rat_one_eq : minpoly ℚ (1 : ℂ) = Polynomial.X - Polynomial.C (1 : ℚ)

Used by 1

Used byOne is a totally positive algebraic integer

TheoremOne is a totally positive algebraic integer#✓fully proved

The complex number \(1\) is a totally positive algebraic integer.

theorem isTotallyPositive_one : IsTotallyPositive (1 : ℂ)

Uses 3

Statement usesTotally positive algebraic integers

Proof usesConjugates · Minimal polynomial of one

DefinitionAdmissible trace bounds#✓fully proved

A real number \(\rho\) is admissible when \(\rho \ge 0\) and only finitely many totally positive algebraic integers \(\alpha \in \mathbb{C}\) have absolute trace less than \(\rho\).

def IsAdmissible (ρ : ℝ) : Prop :=
  0 ≤ ρ ∧ {α : ℂ | IsTotallyPositive α ∧ absoluteTrace α < ρ}.Finite

Uses 2 · Used by 3

Statement usesTotally positive algebraic integers · Absolute trace

Used byAdmissible bounds lie below the Schur–Siegel–Smyth constant · Schur–Siegel–Smyth trace constant · Upper bounds for the Schur–Siegel–Smyth constant

DefinitionSchur–Siegel–Smyth trace constant#✓fully proved

The Schur–Siegel–Smyth trace constant \(C_{86}\) is the supremum, taken in the extended reals, of the admissible real bounds: the real numbers \(\rho \ge 0\) such that only finitely many complex numbers that are totally positive algebraic integers have absolute trace less than \(\rho\).

The extended-real value is \(-\infty\) for an empty admissible set and \(+\infty\) for an unbounded one; finiteness is the content of the known upper bounds.

noncomputable def schurSiegelSmythConstant : EReal :=
  sSup {x : EReal | ∃ ρ : ℝ, IsAdmissible ρ ∧ x = ρ}

Uses 1 · Used by 8

Statement usesAdmissible trace bounds

Used byClassical upper bound for the Schur–Siegel–Smyth constant · Admissible bounds lie below the Schur–Siegel–Smyth constant · Orloski–Sardari–Smith lower bound for the Schur–Siegel–Smyth constant · Sardari–Orloski upper bound for the Schur–Siegel–Smyth constant · Upper bounds for the Schur–Siegel–Smyth constant · Schur's lower bound for the Schur–Siegel–Smyth constant · Smith's upper bound for the Schur–Siegel–Smyth trace constant · Smyth's lower bound for the Schur–Siegel–Smyth constant

TheoremAdmissible bounds lie below the Schur–Siegel–Smyth constant#✓fully proved

Let \(C_{86}\) be the Schur–Siegel–Smyth trace constant, an extended real number. Every admissible real number \(\rho\) satisfies \(\rho \le C_{86}\) in the extended reals.

theorem coe_le_schurSiegelSmythConstant {ρ : ℝ} (hρ : IsAdmissible ρ) :
    (ρ : EReal) ≤ schurSiegelSmythConstant

Uses 2 · Used by 1

Statement usesAdmissible trace bounds · Schur–Siegel–Smyth trace constant

Used byUpper bounds for the Schur–Siegel–Smyth constant

TheoremUpper bounds for the Schur–Siegel–Smyth constant#✓fully proved

For every extended real number \(b\), the Schur–Siegel–Smyth trace constant is at most \(b\) if and only if every admissible real number \(c\) satisfies \(c \le b\).

theorem schurSiegelSmythConstant_le_iff {b : EReal} :
    schurSiegelSmythConstant ≤ b ↔
      ∀ c : ℝ, IsAdmissible c → (c : EReal) ≤ b

Uses 3

Statement usesAdmissible trace bounds · Schur–Siegel–Smyth trace constant

Proof usesAdmissible bounds lie below the Schur–Siegel–Smyth constant

DefinitionSum of the conjugates of a complex number#✓fully proved

For a complex number \(\alpha\), the trace \(\operatorname{tr}(\alpha) \in \mathbb{C}\) is the sum, counted with multiplicity, of the complex roots of the minimal polynomial of \(\alpha\) over \(\mathbb{Q}\). When \(\alpha\) is algebraic these roots are the conjugates \(\alpha_1, \dots, \alpha_n\) of \(\alpha\), so \(\operatorname{tr}(\alpha) = \alpha_1 + \dots + \alpha_n\); when \(\alpha\) is transcendental its minimal polynomial is \(0\) by convention and \(\operatorname{tr}(\alpha) = 0\).

noncomputable def trace (α : ℂ) : ℂ := ((minpoly ℚ α).aroots ℂ).sum

Used by 1

Used byThe Schur–Siegel–Smyth constant \(\lambda_{\mathrm{SSS}}\)

DefinitionDegree of a complex number over the rationals#✓fully proved

For a complex number \(\alpha\), the degree \(\deg(\alpha)\) is the natural number given by the degree of the minimal polynomial of \(\alpha\) over \(\mathbb{Q}\). When \(\alpha\) is transcendental its minimal polynomial is \(0\) by convention, so \(\deg(\alpha) = 0\).

noncomputable def degree (α : ℂ) : ℕ := (minpoly ℚ α).natDegree

Used by 1

Used byThe Schur–Siegel–Smyth constant \(\lambda_{\mathrm{SSS}}\)

DefinitionTotally positive algebraic numbers#✓fully proved

A complex number \(\alpha\) is totally positive if it is algebraic over \(\mathbb{Q}\) and every complex root of its minimal polynomial over \(\mathbb{Q}\), that is, every conjugate of \(\alpha\), is a positive real number.

def IsTotallyPositive (α : ℂ) : Prop :=
  IsAlgebraic ℚ α ∧ ∀ β ∈ (minpoly ℚ α).aroots ℂ, 0 < β

Used by 1

Used byThe Schur–Siegel–Smyth constant \(\lambda_{\mathrm{SSS}}\)

DefinitionThe Schur–Siegel–Smyth constant \(\lambda_{\mathrm{SSS}}\)#✓fully proved

Let \(\lambda_{\mathrm{SSS}}\) be the supremum in \(\mathbb{R}\) of the set of real numbers \(\lambda\) such that, for every \(\varepsilon > 0\), only finitely many complex numbers \(\alpha\) are totally positive algebraic integers with \(\operatorname{tr}(\alpha) < (\lambda - \varepsilon) \deg(\alpha)\), where \(\operatorname{tr}(\alpha)\) and \(\deg(\alpha)\) are the trace and the degree of \(\alpha\) over \(\mathbb{Q}\) (the trace of a totally positive \(\alpha\) is real). By the convention for suprema in \(\mathbb{R}\), \(\lambda_{\mathrm{SSS}} = 0\) if this set is empty or unbounded above.

The set is closed downwards and contains its supremum when it is nonempty and bounded above, so \(\lambda_{\mathrm{SSS}}\) is then the greatest such \(\lambda\). The source says "least real number", but this is a typo, as the set has no lower bound. The greatest real number agrees with Orloski, Sardari and Smith, "New lower bounds for the Schur-Siegel-Smyth trace problem" (arXiv:2401.03252), where \(\lambda_{\mathrm{SSS}}\) is the limit inferior of \(\operatorname{tr}(\alpha)/\deg(\alpha)\) over all totally positive algebraic integers \(\alpha\).

noncomputable def lambda_SSS : ℝ := sSup { lam : ℝ | ∀ ε > (0 : ℝ),
  { α : ℂ | IsIntegral ℤ α ∧ IsTotallyPositive α ∧ trace α < (lam - ε) * degree α }.Finite }

Uses 3 · Used by 1

Statement usesTotally positive algebraic numbers · Degree of a complex number over the rationals · Sum of the conjugates of a complex number

Used bySmith's theorem on the Schur–Siegel–Smyth trace problem

TheoremSmith's theorem on the Schur–Siegel–Smyth trace problem#●ready to prove

The Schur–Siegel–Smyth constant satisfies \(\lambda_{\mathrm{SSS}} < 1.89831\); this is Theorem 1.1 of the source.

public theorem_wanted theorem_1_1 : lambda_SSS < 1.89831

Sources

• A. Smith, Algebraic integers with conjugates in a prescribed distribution, Annals of Math, 200 (1) 2024. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_algebraic_integers of the lean-eval benchmark.

Uses 1

Statement usesThe Schur–Siegel–Smyth constant \(\lambda_{\mathrm{SSS}}\)

TheoremAbsolute trace of a totally positive algebraic integer is at least one#●ready to prove

For every complex number \(\alpha\) that is a totally positive algebraic integer, the absolute trace of \(\alpha\) is at least \(1\).

theorem_wanted absoluteTrace_one_le_wanted (α : ℂ)
    (hα : IsTotallyPositive α) :
    1 ≤ absoluteTrace α

Sources

• catalogue trivial lower row, by AM--GM: the absolute trace is at least the geometric mean of the conjugates, whose product is a nonzero rational integer.

Uses 2

Statement usesTotally positive algebraic integers · Absolute trace

TheoremSchur's lower bound for the Schur–Siegel–Smyth constant#●ready to prove

The Schur–Siegel–Smyth trace constant \(C_{86}\), an extended real number, satisfies \(\sqrt{e} \le C_{86}\).

theorem_wanted schur1918LowerBound_wanted :
    ((Real.sqrt (Real.exp 1) : ℝ) : EReal) ≤ schurSiegelSmythConstant

Sources

• Schur (1918), lower bound √e ≤ C₈₆.

Uses 1

Statement usesSchur–Siegel–Smyth trace constant

TheoremSmyth's lower bound for the Schur–Siegel–Smyth constant#●ready to prove

The Schur–Siegel–Smyth trace constant \(C_{86}\), an extended real number, satisfies \(1.7719 \le C_{86}\).

theorem_wanted smyth1984LowerBound_wanted :
    ((17719 / 10000 : ℝ) : EReal) ≤ schurSiegelSmythConstant

Sources

• Smyth (1984), auxiliary-function lower bound 1.7719 ≤ C₈₆.

Uses 1

Statement usesSchur–Siegel–Smyth trace constant

TheoremOrloski–Sardari–Smith lower bound for the Schur–Siegel–Smyth constant#●ready to prove

The Schur–Siegel–Smyth trace constant \(C_{86}\), an extended real number, satisfies \(1.80203 \le C_{86}\).

theorem_wanted orloskiSardariSmith2025LowerBound_wanted :
    ((180203 / 100000 : ℝ) : EReal) ≤ schurSiegelSmythConstant

Sources

• Orloski--Sardari--Smith (2025), best known lower bound 1.80203 ≤ C₈₆.

Uses 1

Statement usesSchur–Siegel–Smyth trace constant

TheoremClassical upper bound for the Schur–Siegel–Smyth constant#●ready to prove

The Schur–Siegel–Smyth trace constant \(C_{86}\), an extended real number, satisfies \(C_{86} \le 2\).

theorem_wanted classicalUpperBound_wanted :
    schurSiegelSmythConstant ≤ (2 : EReal)

Sources

• classical upper bound C₈₆ ≤ 2, from the totally positive algebraic integers 4 cos^2 (π / n) whose absolute traces tend to 2.

Uses 1

Statement usesSchur–Siegel–Smyth trace constant

TheoremSmith's upper bound for the Schur–Siegel–Smyth trace constant#●ready to prove

The Schur–Siegel–Smyth trace constant \(C_{86}\), an extended real number, satisfies \(C_{86} < 1.89831\).

theorem_wanted smith2024UpperBound_wanted :
    schurSiegelSmythConstant < ((189831 / 100000 : ℝ) : EReal)

Sources

• Smith (2024), strict upper bound C₈₆ < 1.89831 (the form of Smith's theorem recorded in the neighbouring AlgebraicIntegersWanted file as lambda_SSS < 1.89831), disproving the conjectured value 2: infinitely many totally positive algebraic integers have absolute trace below 1.89831.

Uses 1

Statement usesSchur–Siegel–Smyth trace constant

TheoremSardari–Orloski upper bound for the Schur–Siegel–Smyth constant#●ready to prove

The Schur–Siegel–Smyth trace constant \(C_{86}\), an extended real number, satisfies \(C_{86} \le 1.8216\).

theorem_wanted sardariOrloski2024UpperBound_wanted :
    schurSiegelSmythConstant ≤ ((18216 / 10000 : ℝ) : EReal)

Sources

• Sardari--Orloski (2024), best known upper bound C₈₆ ≤ 1.8216 from explicit limiting measures.

Uses 1

Statement usesSchur–Siegel–Smyth trace constant

18 fully proved8 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.