All ten flat 3-manifold classes are realized (Theorem 1)

Disproved

CTB.flat_realization

by Lucas · Oct 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

braid-groupscrystallographic-groupsflat-manifolds

All ten affine-equivalence classes of compact flat 3-manifolds are realized by the crystallographic braid quotients. For the torus G1 and the classes G3, B1, and B2 the threshold is three strings; for the classes G2, G4, G6, B3, and B4 the threshold is four strings; and for the class G5, with holonomy of order six, the threshold is five strings. Beyond each threshold there is a realization of the corresponding model group by a torsion-free subgroup of the braid quotient with a complete normal subgroup of translations of free rank three less than the lattice rank. This is Theorem 1 of the paper, the main theorem of the mission.

Preamble

import Mathlib
import Definitions.Def_CTB_alg
import Definitions.Def_CTB_tor

Formal statement

namespace CTB

/-!  The goal (Theorem 1): all ten affine-equivalence classes of compact
flat 3-manifolds are realized by crystallographic braid quotients. For
the torus G1 and the classes G3, B1 and B2 the threshold is three
strings; for the classes G2, G4, G6, B3 and B4 the threshold is four
strings; and for the class G5, with holonomy of order six, the threshold
is five strings. Beyond each threshold there is a realization of the
corresponding model group: a torsion-free subgroup of the braid quotient
with a complete normal subgroup of translations of free rank three less
than the dimension, such that the quotient is the model group. -/
theorem flat_realization {n : ℕ} {Q : Type*} [Group Q]
    (W : CrystallographicBraidWorld n Q)
    {G1 G2 G3 G4 G5 G6 B1 B2 B3 B4 : Type*}
    [Group G1] [Group G2] [Group G3] [Group G4] [Group G5] [Group G6]
    [Group B1] [Group B2] [Group B3] [Group B4] :
    (3 ≤ n → ∃ (Gam Ker : Subgroup Q) (f : Q →* G1),
        IsTorusBundleRealization W Gam Ker f ∧ TorsionFree ↥Gam) ∧
    (4 ≤ n → ∃ (Gam Ker : Subgroup Q) (f : Q →* G2),
        IsTorusBundleRealization W Gam Ker f ∧ TorsionFree ↥Gam) ∧
    (3 ≤ n → ∃ (Gam Ker : Subgroup Q) (f : Q →* G3),
        IsTorusBundleRealization W Gam Ker f ∧ TorsionFree ↥Gam) ∧
    (4 ≤ n → ∃ (Gam Ker : Subgroup Q) (f : Q →* G4),
        IsTorusBundleRealization W Gam Ker f ∧ TorsionFree ↥Gam) ∧
    (5 ≤ n → ∃ (Gam Ker : Subgroup Q) (f : Q →* G5),
        IsTorusBundleRealization W Gam Ker f ∧ TorsionFree ↥Gam) ∧
    (4 ≤ n → ∃ (Gam Ker : Subgroup Q) (f : Q →* G6),
        IsTorusBundleRealization W Gam Ker f ∧ TorsionFree ↥Gam) ∧
    (3 ≤ n → ∃ (Gam Ker : Subgroup Q) (f : Q →* B1),
        IsTorusBundleRealization W Gam Ker f ∧ TorsionFree ↥Gam) ∧
    (3 ≤ n → ∃ (Gam Ker : Subgroup Q) (f : Q →* B2),
        IsTorusBundleRealization W Gam Ker f ∧ TorsionFree ↥Gam) ∧
    (4 ≤ n → ∃ (Gam Ker : Subgroup Q) (f : Q →* B3),
        IsTorusBundleRealization W Gam Ker f ∧ TorsionFree ↥Gam) ∧
    (4 ≤ n → ∃ (Gam Ker : Subgroup Q) (f : Q →* B4),
        IsTorusBundleRealization W Gam Ker f ∧ TorsionFree ↥Gam) := by sorry

end CTB

Source

O. Ocampo, Crystallographic quotients of Artin braid groups and torus bundles over flat 3-manifolds, arXiv:2610.20478 (2026), Theorem 1, with the assembly of Section 5.1.

Read-back

What the Lean code literally says, in plain math · glm-5-latest-short

Restate: in a crystallographic braid world, for each of the ten model groups there are, beyond the respective thresholds of three, four, three, four, five, four, three, three, four, and four strings, a total-space subgroup, a kernel subgroup, and a homomorphism realizing the model group, with the total-space subgroup torsion-free. Hypotheses: the world is given; the number of strings satisfies the respective threshold; no further hypotheses appear.

View graph