From de6824d2b4d1092fb832ef32411051f4808841f7 Mon Sep 17 00:00:00 2001 From: Rado Kirov Date: Tue, 5 May 2026 05:37:57 +0000 Subject: [PATCH] fix(NumberTheory): correct first disjunct in CMS house theorem MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The first value in Theorem 1.0.5 of Calegari--Morrison--Snyder (arXiv:1004.0665) is `(√7 + √3)/2 ≈ 2.18890`, not `(7 + √3)/2 ≈ 4.366`. The latter is well above the upper bound `76/33 ≈ 2.303` of the hypothesis, so under the typo the disjunct is unreachable and the theorem is strictly weaker than CMS. Co-authored-by: Claude Opus 4.7 (1M context) --- LeanEval/NumberTheory/SmallHouse.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/LeanEval/NumberTheory/SmallHouse.lean b/LeanEval/NumberTheory/SmallHouse.lean index 9d15dba..cfa32fb 100644 --- a/LeanEval/NumberTheory/SmallHouse.lean +++ b/LeanEval/NumberTheory/SmallHouse.lean @@ -32,7 +32,7 @@ theorem cyclotomic_integer_house_between_two_and_76_33 (hβ_int : IsIntegral ℤ β) (hβ_real : β ∈ NumberField.maximalRealSubfield K) : (2 < house β ∧ house β < (76 : ℝ) / 33) → - house β = (7 + Real.sqrt 3) / 2 ∨ + 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 ∨