Cyclotomic integers of small house

TheoremReal cyclotomic integers with house at most 2#●ready to prove

Let \(n \ge 1\), let \(K\) be a number field that is a cyclotomic extension of \(\mathbb{Q}\) generated by the \(n\)-th roots of unity, and let \(\beta \in K\) be an algebraic integer lying in the maximal real subfield of \(K\). Write \(\operatorname{house}(\beta)\) for the largest absolute value of the images of \(\beta\) under the complex embeddings of \(K\). If \(\operatorname{house}(\beta) \le 2\), then \(\operatorname{house}(\beta) = 2\) or \(\operatorname{house}(\beta) = 2\cos(\pi/m)\) for some integer \(m \ge 1\).

public theorem_wanted cyclotomic_integer_house_le_two
    {K : Type*} [Field K] [NumberField K] [Algebra ℚ K]
    (n : ℕ) [NeZero n] [IsCyclotomicExtension {n} ℚ K] {β : K}
    (hβ_int : IsIntegral ℤ β)
    (hβ_real : β ∈ NumberField.maximalRealSubfield K) :
    house β ≤ 2 →
      house β = 2 ∨ ∃ m : ℕ, 0 < m ∧ house β = 2 * Real.cos (Real.pi / m)

Sources

• https://arxiv.org/pdf/1004.0665. Problem cyclotomic_integer_house_le_two of the lean-eval benchmark.

TheoremReal cyclotomic integers with house between 2 and 76/33#●ready to prove

Let \(n \ge 1\), let \(K\) be a number field that is a cyclotomic extension of \(\mathbb{Q}\) generated by the \(n\)-th roots of unity, and let \(\beta \in K\) be an algebraic integer lying in the maximal real subfield of \(K\). Write \(\operatorname{house}(\beta)\) for the largest absolute value of the images of \(\beta\) under the complex embeddings of \(K\). If \(2 < \operatorname{house}(\beta) < 76/33\), then \(\operatorname{house}(\beta)\) is one of \((\sqrt{7} + \sqrt{3})/2\), \(\sqrt{5}\), \(1 + 2\cos(2\pi/7)\), \((1 + \sqrt{5})/\sqrt{2}\) and \((1 + \sqrt{13})/2\).

public theorem_wanted cyclotomic_integer_house_between_two_and_76_33
    {K : Type*} [Field K] [NumberField K] [Algebra ℚ K]
    (n : ℕ) [NeZero n] [IsCyclotomicExtension {n} ℚ K] {β : K}
    (hβ_int : IsIntegral ℤ β)
    (hβ_real : β ∈ NumberField.maximalRealSubfield K) :
    (2 < house β ∧ house β < (76 : ℝ) / 33) →
      house β = (Real.sqrt 7 + Real.sqrt 3) / 2 ∨
      house β = Real.sqrt 5 ∨
      house β = 1 + 2 * Real.cos (2 * Real.pi / 7) ∨
      house β = (1 + Real.sqrt 5) / Real.sqrt 2 ∨
      house β = (1 + Real.sqrt 13) / 2

Sources

• https://arxiv.org/pdf/1004.0665. Problem cyclotomic_integer_house_between_two_and_76_33 of the lean-eval benchmark.

2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.