Real cyclotomic integer with house at most 2

← All problems

cyclotomic_integer_house_le_two

Submitter: Kim Morrison.

Notes: The <= 2 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 is at most 2, then it equals 2 cos(pi / m) for some positive integer m.

theorem declaration uses `sorry`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) := K:Type u_1inst✝⁴:Field Kinst✝³:NumberField Kinst✝²:Algebra ℚ Kn:ℕinst✝¹:NeZero ninst✝:IsCyclotomicExtension {n} ℚ Kβ:Khβ_int:IsIntegral ℤ βhβ_real:β ∈ maximalRealSubfield K⊢ house β ≤ 2 → house β = 2 ∨ ∃ m, 0 < m ∧ house β = 2 * Real.cos (Real.pi / ↑m) All goals completed! 🐙

Solved by

• @mayorov-m-a with Aleph Prover(logicalintelligence.com) on May 8, 2026

• @LorenzoLuccioli with Aristotle (Harmonic) on May 9, 2026 (proof)

• @rishistyping with [submission] aegis-of-the-unit-circle-logos on May 12, 2026

• @rishistyping with Stealth Model on May 12, 2026

• @GanjinZero with Seed Prover (ByteDance) on May 20, 2026

• @daouid with Antigravity (Multi-Model Ensemble: Gemini 3.1 Pro, Gemini 3 Flash, Claude 4.6 Sonnet/Opus) on May 22, 2026 (proof)