From 7abf9beb6b38e7d71ef382ae4b86c9da9beebb14 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Sun, 24 May 2026 07:53:07 +0000
Subject: [PATCH 1/3] feat: add Brauer-Suzuki theorem eval problem
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR adds the 1959 Brauer-Suzuki theorem: if a finite group G has
generalized quaternion Sylow 2-subgroups, then the unique involution of
G maps to a central element of G/O(G). Historical precursor of
Glauberman's Z*-theorem and a seed of the local-analysis programme.

Introduces LeanEval/GroupTheory/Defs/OddCore.lean defining O(G) as the
normal closure of the union of normal odd-order subgroups, since Mathlib
has no `oddCore` operation.

🤖 Prepared with Claude Code
---
 LeanEval/GroupTheory/BrauerSuzuki.lean | 44 ++++++++++++++++++++++++++
 LeanEval/GroupTheory/Defs/OddCore.lean | 30 ++++++++++++++++++
 manifests/problems/brauer_suzuki.toml  |  9 ++++++
 3 files changed, 83 insertions(+)
 create mode 100644 LeanEval/GroupTheory/BrauerSuzuki.lean
 create mode 100644 LeanEval/GroupTheory/Defs/OddCore.lean
 create mode 100644 manifests/problems/brauer_suzuki.toml

diff --git a/LeanEval/GroupTheory/BrauerSuzuki.lean b/LeanEval/GroupTheory/BrauerSuzuki.lean
new file mode 100644
index 0000000..ea1a4db
--- /dev/null
+++ b/LeanEval/GroupTheory/BrauerSuzuki.lean
@@ -0,0 +1,44 @@
+import Mathlib
+import EvalTools.Markers
+import LeanEval.GroupTheory.Defs.OddCore
+
+namespace LeanEval
+namespace GroupTheory
+
+open LeanEval.GroupTheory.Defs
+
+/-!
+# Brauer–Suzuki theorem on generalized quaternion Sylow 2-subgroups
+
+Let `G` be a finite group whose Sylow 2-subgroups are generalized
+quaternion (i.e., isomorphic to `QuaternionGroup (2^(n-1))` for some
+`n ≥ 2`). Let `t` be the unique involution of any (equivalently, every)
+Sylow 2-subgroup. Then the image of `t` in `G / O(G)` is central, where
+`O(G)` is the largest normal subgroup of `G` of odd order.
+
+R. Brauer and M. Suzuki, "On finite groups of even order whose 2-Sylow
+group is a quaternion group", Proc. Nat. Acad. Sci. U.S.A. 45 (1959).
+This was the precursor of Glauberman's Z*-theorem (1966) and the
+historical seed of the local-analysis programme in CFSG.
+
+The conclusion is phrased entirely in the quotient `G / O(G)`,
+applied to the image of `t` under `QuotientGroup.mk`; the value of
+`t : G` only enters via that map.
+
+Introduces `Defs/OddCore.lean` since Mathlib has no `oddCore`/`O(G)`
+operation.
+-/
+
+/-- **Brauer–Suzuki theorem (quaternion case).** -/
+@[eval_problem]
+theorem brauer_suzuki {G : Type*} [Group G] [Finite G]
+    (n : ℕ) (hn : 2 ≤ n)
+    (P : Sylow 2 G)
+    (hquat : Nonempty ((P : Subgroup G) ≃* QuaternionGroup (2 ^ (n - 1))))
+    (t : G) (ht_mem : t ∈ (P : Subgroup G)) (ht_ord : orderOf t = 2) :
+    (QuotientGroup.mk t : G ⧸ oddCore G) ∈
+      Subgroup.center (G ⧸ oddCore G) := by
+  sorry
+
+end GroupTheory
+end LeanEval
diff --git a/LeanEval/GroupTheory/Defs/OddCore.lean b/LeanEval/GroupTheory/Defs/OddCore.lean
new file mode 100644
index 0000000..336ec1c
--- /dev/null
+++ b/LeanEval/GroupTheory/Defs/OddCore.lean
@@ -0,0 +1,30 @@
+import Mathlib
+
+namespace LeanEval
+namespace GroupTheory
+namespace Defs
+
+/-- `oddCore G` is the largest normal subgroup of `G` of odd order.
+Classically denoted `O(G)` (in older notation `O_{2'}(G)`).
+
+Defined as the normal closure of the union of all normal odd-order
+subgroups. Since each such subgroup is already normal, the normal closure
+of their union coincides with their supremum; we use `normalClosure` to
+obtain the `Normal` instance for free.
+
+For a finite group this agrees with the textbook definition: the product
+of two normal odd-order subgroups is again a normal odd-order subgroup,
+and finiteness bounds the chain. For an infinite group the definition
+still makes sense as the largest normal subgroup generated by odd-order
+normal subgroups.
+-/
+def oddCore (G : Type*) [Group G] : Subgroup G :=
+  Subgroup.normalClosure
+    (⋃ N ∈ {N : Subgroup G | N.Normal ∧ Odd (Nat.card N)}, (N : Set G))
+
+instance oddCore_normal (G : Type*) [Group G] : (oddCore G).Normal :=
+  Subgroup.normalClosure_normal
+
+end Defs
+end GroupTheory
+end LeanEval
diff --git a/manifests/problems/brauer_suzuki.toml b/manifests/problems/brauer_suzuki.toml
new file mode 100644
index 0000000..fe8a566
--- /dev/null
+++ b/manifests/problems/brauer_suzuki.toml
@@ -0,0 +1,9 @@
+id = "brauer_suzuki"
+title = "Brauer–Suzuki theorem (quaternion Sylow 2-subgroup)"
+test = false
+module = "LeanEval.GroupTheory.BrauerSuzuki"
+holes = ["brauer_suzuki"]
+submitter = "Kim Morrison"
+notes = "If a finite group G has generalized quaternion Sylow 2-subgroups, then the unique involution of G maps to a central element of G/O(G), where O(G) is the largest normal odd-order subgroup. R. Brauer and M. Suzuki, 'On finite groups of even order whose 2-Sylow group is a quaternion group', Proc. Nat. Acad. Sci. U.S.A. 45 (1959), 1757-1759. Historical precursor of Glauberman's Z*-theorem (1966) and the local-analysis programme in CFSG. Introduces Defs/OddCore.lean defining O(G) as the supremum of all normal odd-order subgroups (Mathlib has no `oddCore` operation)."
+source = "R. Brauer and M. Suzuki, On finite groups of even order whose 2-Sylow group is a quaternion group, Proc. Nat. Acad. Sci. U.S.A. 45 (1959), 1757-1759. https://doi.org/10.1073/pnas.45.12.1757"
+informal_solution = "The argument is character-theoretic and proceeds via a careful analysis of the principal 2-block of G. In a generalized quaternion 2-Sylow P, the unique involution z = a^{2^{n-2}} is central in P (where a is the generator of the cyclic maximal subgroup of P). Brauer's principal-block reformulation: z lies in the kernel of every ordinary irreducible character not in the principal 2-block, plus an analysis of how the principal block's characters restrict to ⟨z⟩, forces z·O(G) into the center of G/O(G). Modern simplification: Glauberman's Z*-theorem, of which Brauer-Suzuki is the prototypical case, says any isolated involution is in Z*(G); the unique involution of a generalized-quaternion Sylow 2-subgroup is automatically isolated."

From 6daa00c745ea578bfd9e87ce44395b4cdc855795 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Sun, 24 May 2026 12:02:44 +0000
Subject: [PATCH 2/3] fix: use textbook indexing for quaternion size in
 Brauer-Suzuki
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The original statement used `QuaternionGroup (2^(n-1))` with `n ≥ 2`,
which is mathematically correct but indexes Q_8, Q_16, ... by n = 2, 3,
...  — not matching the textbook convention where n = log₂|P|.

Update to `QuaternionGroup (2^(n-2))` with `n ≥ 3`, so n cleanly equals
log₂|P| and the docstring's Q_{2^n} notation matches the index.
Spotted in second-opinion review by Codex.

🤖 Prepared with Claude Code
---
 LeanEval/GroupTheory/BrauerSuzuki.lean | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/LeanEval/GroupTheory/BrauerSuzuki.lean b/LeanEval/GroupTheory/BrauerSuzuki.lean
index ea1a4db..f58ccd4 100644
--- a/LeanEval/GroupTheory/BrauerSuzuki.lean
+++ b/LeanEval/GroupTheory/BrauerSuzuki.lean
@@ -11,10 +11,12 @@ open LeanEval.GroupTheory.Defs
 # Brauer–Suzuki theorem on generalized quaternion Sylow 2-subgroups
 
 Let `G` be a finite group whose Sylow 2-subgroups are generalized
-quaternion (i.e., isomorphic to `QuaternionGroup (2^(n-1))` for some
-`n ≥ 2`). Let `t` be the unique involution of any (equivalently, every)
-Sylow 2-subgroup. Then the image of `t` in `G / O(G)` is central, where
-`O(G)` is the largest normal subgroup of `G` of odd order.
+quaternion: isomorphic to `Q_{2^n}` for some `n ≥ 3`, i.e., to Mathlib's
+`QuaternionGroup (2^(n-2))` (since `QuaternionGroup m` has order `4m`,
+giving `|Q_{2^n}| = 2^n` and `n = log₂|P|`). Let `t` be the unique
+involution of any (equivalently, every) Sylow 2-subgroup. Then the
+image of `t` in `G / O(G)` is central, where `O(G)` is the largest
+normal subgroup of `G` of odd order.
 
 R. Brauer and M. Suzuki, "On finite groups of even order whose 2-Sylow
 group is a quaternion group", Proc. Nat. Acad. Sci. U.S.A. 45 (1959).
@@ -32,9 +34,9 @@ operation.
 /-- **Brauer–Suzuki theorem (quaternion case).** -/
 @[eval_problem]
 theorem brauer_suzuki {G : Type*} [Group G] [Finite G]
-    (n : ℕ) (hn : 2 ≤ n)
+    (n : ℕ) (hn : 3 ≤ n)
     (P : Sylow 2 G)
-    (hquat : Nonempty ((P : Subgroup G) ≃* QuaternionGroup (2 ^ (n - 1))))
+    (hquat : Nonempty ((P : Subgroup G) ≃* QuaternionGroup (2 ^ (n - 2))))
     (t : G) (ht_mem : t ∈ (P : Subgroup G)) (ht_ord : orderOf t = 2) :
     (QuotientGroup.mk t : G ⧸ oddCore G) ∈
       Subgroup.center (G ⧸ oddCore G) := by

From 8e1406dc7b291125ad4cec6291eab04bee750194 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Sun, 24 May 2026 12:32:59 +0000
Subject: [PATCH 3/3] refactor: define oddCore as sSup rather than
 normalClosure
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Switch to the more direct definition `sSup {N | N.Normal ∧ Odd (Nat.card N)}`,
matching the textbook formulation directly. The Normal instance is now
proved by `iSup_induction`: conjugation by `g` fixes every normal
subgroup in the indexing family, so it fixes their supremum.

🤖 Prepared with Claude Code
---
 LeanEval/GroupTheory/Defs/OddCore.lean | 47 +++++++++++++++++---------
 1 file changed, 31 insertions(+), 16 deletions(-)

diff --git a/LeanEval/GroupTheory/Defs/OddCore.lean b/LeanEval/GroupTheory/Defs/OddCore.lean
index 336ec1c..1e1ae67 100644
--- a/LeanEval/GroupTheory/Defs/OddCore.lean
+++ b/LeanEval/GroupTheory/Defs/OddCore.lean
@@ -4,26 +4,41 @@ namespace LeanEval
 namespace GroupTheory
 namespace Defs
 
-/-- `oddCore G` is the largest normal subgroup of `G` of odd order.
-Classically denoted `O(G)` (in older notation `O_{2'}(G)`).
+/-- `oddCore G` is the largest normal subgroup of `G` of odd order — the
+supremum of all normal subgroups whose cardinality is odd. Classically
+denoted `O(G)` (in older notation `O_{2'}(G)`).
 
-Defined as the normal closure of the union of all normal odd-order
-subgroups. Since each such subgroup is already normal, the normal closure
-of their union coincides with their supremum; we use `normalClosure` to
-obtain the `Normal` instance for free.
-
-For a finite group this agrees with the textbook definition: the product
-of two normal odd-order subgroups is again a normal odd-order subgroup,
-and finiteness bounds the chain. For an infinite group the definition
-still makes sense as the largest normal subgroup generated by odd-order
-normal subgroups.
+For a finite group, the join of two normal odd-order subgroups is again
+a normal odd-order subgroup, and finiteness bounds the chain — so the
+supremum is itself a normal subgroup of odd order, agreeing with the
+textbook definition. For an infinite group the definition still makes
+sense as a subgroup, though it need not be of odd order.
 -/
 def oddCore (G : Type*) [Group G] : Subgroup G :=
-  Subgroup.normalClosure
-    (⋃ N ∈ {N : Subgroup G | N.Normal ∧ Odd (Nat.card N)}, (N : Set G))
+  sSup {N : Subgroup G | N.Normal ∧ Odd (Nat.card N)}
 
-instance oddCore_normal (G : Type*) [Group G] : (oddCore G).Normal :=
-  Subgroup.normalClosure_normal
+/-- The odd core is normal: conjugation by any `g : G` fixes every normal
+subgroup in the family pointwise, hence fixes their supremum setwise. -/
+instance oddCore_normal (G : Type*) [Group G] : (oddCore G).Normal where
+  conj_mem n hn g := by
+    have hn' : n ∈ ⨆ N : {N : Subgroup G // N.Normal ∧ Odd (Nat.card N)},
+        (N : Subgroup G) := by
+      rwa [oddCore, sSup_eq_iSup'] at hn
+    refine Subgroup.iSup_induction (C := fun y => g * y * g⁻¹ ∈ oddCore G)
+      _ hn' (fun N x hxN => ?_) ?_ (fun x y hx hy => ?_)
+    · -- `N.val` is a normal subgroup, so `g * x * g⁻¹ ∈ N.val ≤ oddCore G`
+      have hN_norm : (N : Subgroup G).Normal := N.prop.1
+      exact (le_sSup N.prop : (N : Subgroup G) ≤ oddCore G)
+        (hN_norm.conj_mem x hxN g)
+    · -- `g * 1 * g⁻¹ = 1 ∈ oddCore G`
+      show g * 1 * g⁻¹ ∈ oddCore G
+      simp
+    · -- `g * (x * y) * g⁻¹ = (g * x * g⁻¹) * (g * y * g⁻¹)`
+      show g * (x * y) * g⁻¹ ∈ oddCore G
+      have h_distr : g * (x * y) * g⁻¹ = (g * x * g⁻¹) * (g * y * g⁻¹) := by
+        group
+      rw [h_distr]
+      exact mul_mem hx hy
 
 end Defs
 end GroupTheory