spatial_topology_forcing
plain-language theorem explainer
Among the six compact orientable flat 3-manifolds (Bieberbach types), the 3-torus is the unique one with first Betti number 3, and that number equals 3. Anyone citing the RS spatial-topology forcing step (flat + compact + orientable + isotropic substrate ⇒ T³, hence D = 3) uses this. The proof is a two-component term: reflexivity for b₁(T³)=3 plus the uniqueness lemma.
Claim. Let $\mathcal{B}$ be the six Bieberbach types of compact orientable flat 3-manifolds. Writing $b_1$ for the first Betti number of each type, one has $b_1(T^3)=3$, and if $B\in\mathcal{B}$ satisfies $b_1(B)=3$ then $B=T^3$.
background
The module derives spatial topology from recognition-substrate constraints. Homogeneity of the comparison law $J(x)=\cosh(\log x)-1$ (ratio-only, no preferred cell) forces a homogeneous manifold. Self-similarity under $x\mapsto x^\varphi$ forbids a curvature radius, so the metric must be flat. Compactness, orientability, and flatness then put the substrate in the Bieberbach list of six compact orientable flat 3-manifolds.
Those types are encoded as an inductive enumeration: $T^3$ (b₁=3), four screw-motion quotients (half-, quarter-, third-, sixth-turn, each b₁=1), and Hantzsche–Wendt (b₁=0). The first Betti number is the rank of $H^1(M;\mathbb{Z})$, assigned by a simple case table on that enumeration.
Isotropy of the substrate selects the unique type with three independent closed 1-cycles, i.e. b₁=3. The external geometric input is standard differential geometry (Bieberbach classification plus isotropy), not an RS-internal axiom.
proof idea
Term-mode pair constructor. The left conjunct is rfl against the definitional clause firstBettiNumber .torus3 = 3. The right conjunct is exactly the sibling uniqueness lemma torus3_unique_b1_3, which case-splits the six Bieberbach constructors and discharges every non-torus branch by the numeric mismatch of their tabulated b₁ values with 3. No further rewriting or arithmetic is required.
why it matters
This is the topology half of the spatial forcing package advertised in the module: flatness from φ-self-similarity, then T³ from flatness + compactness + orientability + isotropy, with D identified as b₁(T³). The forcing-chain landmark T8 (D = 3 spatial dimensions) takes its external topological input from precisely this statement rather than from “S¹ is the unique compact connected 1-manifold.”
Sibling material in the same file (isotropy_forces_b1_eq_3, spatial_dimension_eq_3, and the certificate wrappers) packages the same fact for downstream constants modules that hard-code D := 3 (GapDerivation, AlphaDerivation). Status is structural: zero sorry, zero RS-internal axiom. No used_by edges are recorded yet; the natural consumers are the dimension certificates and any proof that needs uniqueness of the b₁=3 flat type.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.