From 6a2aeb200b5fe3ed327d16fc37dece0629c90c3e Mon Sep 17 00:00:00 2001
From: "jinping.z" <cecily73517@gmail.com>
Date: Tue, 21 Jul 2026 19:08:14 +0200
Subject: [PATCH 1/2] Add files via upload

Add Schinzel-Zassenhaus theorem formalization
---
 LeanEval/NumberTheory/SchinzelZassenhaus.lean | 46 +++++++++++++++++++
 1 file changed, 46 insertions(+)
 create mode 100644 LeanEval/NumberTheory/SchinzelZassenhaus.lean

diff --git a/LeanEval/NumberTheory/SchinzelZassenhaus.lean b/LeanEval/NumberTheory/SchinzelZassenhaus.lean
new file mode 100644
index 00000000..53924e48
--- /dev/null
+++ b/LeanEval/NumberTheory/SchinzelZassenhaus.lean
@@ -0,0 +1,46 @@
+import Mathlib.NumberTheory.NumberField.House
+
+/-!
+# The Schinzel–Zassenhaus Conjecture
+
+This file records a Lean statement of Dimitrov's theorem as it appears in
+Chapter 4 of McKee and Smyth, *Around the Unit Circle*.
+
+Let `α₁, ..., αₙ` denote the conjugates of a nonzero algebraic
+integer `α` which is not a root of unity.  The Schinzel–Zassenhaus
+conjecture asserts that there is an absolute constant `c > 0` such that
+
+`max_{1 ≤ j ≤ n} |αⱼ| > 1 + c / d`.
+
+The quantity `maxⱼ |αⱼ|` is called the house of `α`; in Mathlib this
+is `NumberField.house`.
+
+## Reference
+
+The formalization is based on Chapter 4 ("The Schinzel–Zassenhaus Conjecture") of the book:
+* **James McKee, Chris Smyth**, *Around the Unit Circle: Mahler Measure, Integer Matrices and Roots of Unity*, Springer, Universitext, 2021.
+（https://link.springer.com/chapter/10.1007/978-3-030-80031-4_4）
+-/
+
+namespace LeanEval.NumberTheory
+
+/-- **Dimitrov's theorem**, McKee–Smyth Theorem 4.1.
+
+Let `α` be a nonzero algebraic integer, not a root of unity.  Then the
+house of `α` is at least `2 ^ (1 / (4 * d'))`, where `d'` is the number of
+different phases among its conjugates.
+
+The condition "not a root of unity" is expressed as `¬ IsOfFinOrder α`,
+Mathlib's standard predicate for an element having no positive power equal to 1.
+-/
+
+theorem dimitrov {K : Type*} [Field K] [NumberField K]
+    (α : K)
+    (α_int : IsIntegral ℤ α)
+    (α_ne_zero : α ≠ 0)
+    (α_not_rootOfUnity : ¬ IsOfFinOrder α) :
+    (2 : ℝ) ^ (1 / (4 * (Finset.univ.image fun σ : K →+* ℂ ↦ (σ α).arg).card) : ℝ) ≤
+      NumberField.house α := by
+  sorry
+
+end LeanEval.NumberTheory
\ No newline at end of file

From 0f6728e24214f8463d6371eb0240361f349ad622 Mon Sep 17 00:00:00 2001
From: "jinping.z" <cecily73517@gmail.com>
Date: Tue, 21 Jul 2026 19:15:57 +0200
Subject: [PATCH 2/2] Add files via upload

Add manifest for Schinzel-Zassenhaus theorem
---
 manifests/problems/dimitrov_theorem_4_1.toml | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 manifests/problems/dimitrov_theorem_4_1.toml

diff --git a/manifests/problems/dimitrov_theorem_4_1.toml b/manifests/problems/dimitrov_theorem_4_1.toml
new file mode 100644
index 00000000..38308757
--- /dev/null
+++ b/manifests/problems/dimitrov_theorem_4_1.toml
@@ -0,0 +1,9 @@
+id = "dimitrov"
+title = "Dimitrov's lower bound for the house of a nonzero algebraic integer that is not a root of unity"
+test = false
+module = "LeanEval.NumberTheory.SchinzelZassenhaus"
+holes = ["dimitrov"]
+submitter = "Zou Jinping"
+notes = "Statement-only benchmark problem. The theorem uses Mathlib's NumberField.house and IsOfFinOrder."
+source = "James McKee and Chris Smyth, Around the Unit Circle, Chapter 4, Theorem 4.1; Vesselin Dimitrov (2019)."
+informal_solution = "Dimitrov's proof of the Schinzel--Zassenhaus conjecture."
\ No newline at end of file