Real cyclotomic integer with house in (2, 76/33) | Lean AI formalization leaderboard

Problem statement

Notes: The 2 < house < 76/33 branch of Theorem 1.0.5 from Calegari--Morrison--Snyder, stated using Mathlib's NumberField.house.

Source: https://arxiv.org/pdf/1004.0665

Informal solution: If the house lies in (2, 76/33), then it is one of the five explicitly listed values.

theorem declaration uses `sorry`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 := byK:Type u_1inst✝⁴:Field Kinst✝³:NumberField Kinst✝²:Algebra ℚ Kn:ℕinst✝¹:NeZero ninst✝:IsCyclotomicExtension {n} ℚ Kβ:Khβ_int:IsIntegral ℤ βhβ_real:β ∈ maximalRealSubfield K⊢ 2 < house β ∧ house β < 76 / 33 →
  house β = (√7 + √3) / 2 ∨
    house β = √5 ∨ house β = 1 + 2 * Real.cos (2 * Real.pi / 7) ∨ house β = (1 + √5) / √2 ∨ house β = (1 + √13) / 2
  sorryAll goals completed! 🐙