The Hantzsche-Wendt class is realized (Theorem 3.9)
DisprovedCTB.realization_hwThe Hantzsche-Wendt class is realized. For every n of at least four strings there is a realization of the class G6 - the fundamental group of the Hantzsche-Wendt manifold - by a torsion-free subgroup of the crystallographic braid quotient whose holonomy group is the Klein four group. This is Theorem 3.9 of the paper.
import Mathlib import Definitions.Def_CTB_alg import Definitions.Def_CTB_tor
namespace CTB
/-! Milestone 4 (Theorem 3.9): the Hantzsche-Wendt class is realized.
For every n of at least four strings there is a realization of the class
G6, the fundamental group of the Hantzsche-Wendt manifold, by a
torsion-free subgroup of the crystallographic braid quotient whose
holonomy group is the Klein four group. -/
theorem realization_hw {n : ℕ} {Q : Type*} [Group Q]
(W : CrystallographicBraidWorld n Q)
{G6 : Type*} [Group G6] (hn : 4 ≤ n) :
∃ (Gam Ker : Subgroup Q) (f : Q →* G6),
IsTorusBundleRealization W Gam Ker f ∧ TorsionFree ↥Gam ∧
Nonempty (Subgroup.map W.hol Gam ≃* Multiplicative (Fin 2 → ZMod 2)) := by sorry
end CTB
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: in a crystallographic braid world with at least four strings, there exist a total-space subgroup, a kernel subgroup, and a homomorphism realizing the Hantzsche-Wendt model group, with the total-space subgroup torsion-free and its image under the holonomy projection multiplicatively equivalent to the multiplicative twin of the group of two-bit tuples. Hypotheses: the world is given; the number of strings is at least four; no further hypotheses appear.