torus3_unique_b1_3
plain-language theorem explainer
Among the six compact orientable flat 3-manifolds, only the 3-torus has first Betti number 3. Anyone citing spatial topology forcing, isotropy selection of T³, or the T8 dimension step would invoke this uniqueness. The proof is exhaustive case analysis on the Bieberbach inductive type, simplifying the fixed Betti table.
Claim. Let $B$ be any of the six compact orientable flat 3-manifolds in the Bieberbach classification. If the first Betti number satisfies $b_1(B)=3$, then $B$ is the 3-torus $T^3$.
background
The module forces the recognition substrate's spatial topology from three constraints: homogeneity (the comparison cost $J(x)=\cosh(\log x)-1$ is position-independent), flatness (φ-self-similarity forbids a preferred curvature scale), and the Bieberbach list of compact orientable flat 3-manifolds.
BieberbackType is that finite list: $T^3$ ($b_1=3$), four screw-motion quotients (half-, quarter-, third-, sixth-turn, each $b_1=1$), and Hantzsche–Wendt ($b_1=0$). The first Betti number $b_1=\mathrm{rank},H^1(M;\mathbb{Z})$ is tabulated by a simple function on this inductive type.
Only $T^3$ carries three independent $H^1$ cycles. Downstream, isotropy equates those cycles with spatial directions and demands $b_1=\dim=3$, so uniqueness of the $b_1=3$ entry is the algebraic gate to $T^3$.
proof idea
Introduce the hypothesis $b_1(B)=3$. Case-split on the six constructors of BieberbackType. On each branch, simplify with the definition of firstBettiNumber: the four screw types give $1=3$, Hantzsche–Wendt gives $0=3$, both absurd; only torus3 survives with $3=3$, yielding $B=.\mathrm{torus3}$. No external lemmas beyond the inductive type and its Betti table.
why it matters
This is the uniqueness half of the spatial topology forcing theorem. Downstream, isotropy_forces_b1_eq_3 is a one-line rephrasing under an isotropy hypothesis; spatial_topology_forcing packages $\langle b_1(T^3)=3,,\forall B.,b_1(B)=3\to B=T^3\rangle$; and spatialTopologyForcingCert records torus_forced for the certificate bundle.
In the forcing chain this underwrites T8: spatial dimension $D=3$ is identified with $b_1(T^3)$. Combined with flatness from φ-self-similarity and compactness/orientability of the substrate, it closes the route from substrate symmetries to $T^3$ topology. Status is structural (0 sorry).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.