Prove2Me

The four non-orientable classes are realized (Theorems 4.1 and 4.5)

Disproved
CTB.realization_nonorientable

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

crystallographic-groupsflat-manifoldsnon-orientable-manifolds

The four non-orientable classes are realized. For every n of at least three strings there are realizations of the classes B1 and B2, each with holonomy of order two; and for every n of at least four strings there are realizations of the classes B3 and B4, each with holonomy the Klein four group. Every realization is by a torsion-free subgroup of the crystallographic braid quotient. These are Theorems 4.1 and 4.5 of the paper.

Preamble
import Mathlib
import Definitions.Def_CTB_alg
import Definitions.Def_CTB_tor
Formal statement
namespace CTB

/-!  Milestone 5 (Theorems 4.1 and 4.5): the four non-orientable
classes are realized. For every n of at least three strings there are
realizations of the classes B1 and B2, each with holonomy of order two;
and for every n of at least four strings there are realizations of the
classes B3 and B4, each with holonomy the Klein four group. Every
realization is by a torsion-free subgroup of the crystallographic braid
quotient. -/
theorem realization_nonorientable {n : ℕ} {Q : Type*} [Group Q]
    (W : CrystallographicBraidWorld n Q)
    {B1 B2 B3 B4 : Type*} [Group B1] [Group B2] [Group B3] [Group B4] :
    (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), Section 4 (Theorems 4.1 and 4.5).
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 non-orientable classes there are, beyond the respective thresholds of 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