firstBettiNumber
plain-language theorem explainer
Assigns the classical first Betti number b₁ to each of the six compact orientable flat 3-manifolds in the Bieberbach list: 3 for T³, 1 for the four screw-motion quotients, and 0 for Hantzsche–Wendt. Anyone proving uniqueness of T³ under isotropy or identifying D with b₁(T³) cites this table. It is a pure pattern-match definition with no proof obligations.
Claim. Define $b_1$ on the six compact orientable flat 3-manifolds by $b_1(T^3)=3$, $b_1=1$ on the half-turn, quarter-turn, third-turn, and sixth-turn flat manifolds, and $b_1=0$ on the Hantzsche–Wendt manifold.
background
The module forces spatial topology of the recognition substrate from three constraints: homogeneity (the cost $J(x)=\cosh(\log x)-1$ is position-independent), flatness (φ-self-similarity forbids a preferred curvature scale), and the Bieberbach classification of compact orientable flat 3-manifolds.
That classification yields exactly six types, encoded by the inductive type with constructors for $T^3$, the four crystallographic screw quotients (half-, quarter-, third-, sixth-turn), and Hantzsche–Wendt. The first Betti number $b_1=\mathrm{rank},H^1(M;\mathbb{Z})$ distinguishes them: only $T^3$ has three independent 1-cycles.
Upstream, the circle-winding chain supplies the injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$ (distinct multiples of the once-around loop are never homologous), which underwrites treating $b_1$ as a well-defined integer invariant of free abelian homology rank.
proof idea
No proof: a definition by exhaustive pattern match on the six constructors of the Bieberbach inductive type. Each clause hard-codes the classical value of $b_1$ for that manifold. Downstream uniqueness lemmas simply case-split on the same constructors and simplify against this table.
why it matters
This table is the numerical spine of the spatial topology forcing argument (framework landmark T8: $D=3$). Downstream, torus3_unique_b1_3 reads off that only $T^3$ has $b_1=3$; isotropy then forces that unique type because "each independent cycle of $H^1$ corresponds to an independent spatial direction." The master theorem packages flatness, $T^3$ uniqueness, and $D=b_1(T^3)=3$ into one certificate, and spatial_dimension_eq_3 is literally rfl against this definition.
Without the assignment, the forcing chain cannot equate spatial dimension with a topological invariant of the forced manifold. The module status is structural (0 sorry, 0 RS-internal axiom); the values themselves are classical Bieberbach data imported as a definition rather than re-derived from singular homology inside Lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.