BieberbackType
plain-language theorem explainer
Enumerates the six compact orientable flat 3-manifolds from the Bieberbach classification: T³, four screw-motion quotients, and the Hantzsche–Wendt manifold. Anyone citing spatial topology forcing or the D=3 step uses this type as the discrete case space. As an inductive definition it carries no proof burden; downstream maps assign first Betti numbers and uniqueness arguments case-split on the constructors.
Claim. There are exactly six compact orientable flat 3-manifolds up to affine diffeomorphism (Bieberbach): the 3-torus $T^3$; the half-turn, quarter-turn, third-turn, and sixth-turn flat manifolds; and the Hantzsche–Wendt manifold. These are the constructors of the discrete type of Bieberbach geometries used below.
background
The module derives spatial topology from recognition-substrate constraints. Homogeneity of the comparison cost $J(x)=\cosh(\log x)-1$ forces a homogeneous manifold; $\varphi$-self-similarity forces flat geometry, because curvature would introduce a preferred scale. Compactness plus orientability then lands in the classical Bieberbach list of compact flat 3-manifolds.
That list has six orientable types, all quotients of $\mathbb{R}^3$ by crystallographic groups. The 3-torus $T^3=\mathbb{R}^3/\mathbb{Z}^3$ is the lattice quotient; the four “turn” manifolds arise from screw motions (finite cyclic rotations combined with translations); Hantzsche–Wendt is the remaining orientable flat quotient. The first Betti number $b_1=\mathrm{rank},H^1(M;\mathbb{Z})$ distinguishes them: $b_1(T^3)=3$, the turn manifolds have $b_1=1$, and Hantzsche–Wendt has $b_1=0$.
This inductive type is the discrete carrier for that classification inside the forcing argument. No external topology library is imported; the six names are the entire case space.
proof idea
No proof: pure inductive definition with six nullary constructors. Mathematical content is the classical Bieberbach enumeration of compact orientable flat 3-manifolds, recorded as named cases rather than derived. Downstream firstBettiNumber is a pattern-match assigning $3,1,1,1,1,0$; uniqueness theorems case-split on the constructors and discharge by simp.
why it matters
This type is the discrete spine of the spatial topology forcing theorem. Downstream, firstBettiNumber tags each case; torus3_unique_b1_3 proves only $T^3$ has $b_1=3$; isotropy_forces_b1_eq_3 upgrades isotropy (no preferred direction) to $B=T^3$; spatial_topology_forcing packages flatness, $T^3$ uniqueness, and $D=3$; spatial_dimension_eq_3 is the one-line $b_1(T^3)=3$; and SpatialTopologyForcingCert is the master certificate structure.
In the Recognition forcing chain this supplies the topological input behind T8 ($D=3$ spatial dimensions): once substrate homogeneity, $\varphi$-self-similarity (flatness), compactness, orientability, and isotropy are granted, the only remaining Bieberbach type is $T^3$, whose first Betti number is the spatial dimension. Without this finite case list the uniqueness and dimension theorems have nothing to case-split on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.