The orientable classes with cyclic holonomy are realized (Theorems 3.1, 3.2, 3.3, and 3.7)

Disproved

CTB.realization_cyclic

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

crystallographic-groupscyclic-holonomyflat-manifolds

The orientable classes with cyclic holonomy are realized. For every n of at least four strings there is a realization of the class G2 with holonomy of order two; for every n of at least three strings a realization of the class G3 with holonomy of order three; for every n of at least four strings a realization of the class G4 with holonomy of order four; and for every n of at least five strings a realization of the class G5 with holonomy of order six. Each realization is by a torsion-free subgroup of the crystallographic braid quotient. These are Theorems 3.1, 3.2, 3.3, and 3.7 of the paper.

Preamble

import Mathlib
import Definitions.Def_CTB_alg
import Definitions.Def_CTB_tor

Formal statement

namespace CTB

/-!  Milestone 3 (Theorems 3.1, 3.2, 3.3 and 3.7): the orientable
classes with cyclic holonomy are realized. For every n of at least four
strings there is a realization of the class G2 with holonomy of order
two; for every n of at least three strings there is a realization of the
class G3 with holonomy of order three; for every n of at least four
strings there is a realization of the class G4 with holonomy of order
four; and for every n of at least five strings there is a realization of
the class G5 with holonomy of order six. Each realization is by a
torsion-free subgroup of the crystallographic braid quotient. -/
theorem realization_cyclic {n : ℕ} {Q : Type*} [Group Q]
    (W : CrystallographicBraidWorld n Q)
    {G2 G3 G4 G5 : Type*} [Group G2] [Group G3] [Group G4] [Group G5] :
    (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) := by sorry

end CTB

Source

O. Ocampo, Crystallographic quotients of Artin braid groups and torus bundles over flat 3-manifolds, arXiv:2610.20478 (2026), Section 3 (Theorems 3.1, 3.2, 3.3, and 3.7).

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 four orientable cyclic-holonomy classes there are, beyond the respective thresholds of four, three, four, and five 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