spatial_dimension_eq_3
plain-language theorem explainer
Spatial dimension equals three because the first Betti number of the forced 3-torus is three. Anyone citing Recognition Science T8 (D = 3) or the spatial-topology forcing chain would quote this identification. The proof is pure definitional reflexivity against the Bieberbach-type table.
Claim. The first Betti number of the 3-torus $T^3$ (the unique compact orientable flat 3-manifold selected by substrate constraints among the six Bieberbach types) equals $3$, and this value is the spatial dimension $D$.
background
The module derives spatial topology from three substrate constraints: homogeneity (the comparison cost $J(x)=\cosh(\log x)-1$ is ratio-only, so no preferred cell or boundary), flatness (φ-self-similarity forbids a curvature radius, ruling out spherical and hyperbolic geometry), and the Bieberbach classification of compact orientable flat 3-manifolds.
That classification yields six types. Only the 3-torus $T^3=\mathbb{R}^3/\mathbb{Z}^3$ has first Betti number $b_1=3$; the four screw-motion quotients have $b_1=1$, and the Hantzsche–Wendt manifold has $b_1=0$. The inductive type enumerates those six manifolds; the first-Betti map sends each constructor to the integer in the table above.
proof idea
One-line term proof by definitional reflexivity. The first-Betti function is defined by pattern-match with the clause for the 3-torus constructor equal to $3$, so the equality holds by rfl with no further lemmas.
why it matters
This is the explicit D = 3 identification in the Recognition forcing chain (primer landmark T8). Upstream, isotropy and self-similarity already force the topology to be the 3-torus among the six Bieberbach types; the present line simply reads off $b_1(T^3)=3$ as the spatial dimension. The module is marked structural (zero sorry, zero RS-internal axiom). No downstream dependents are recorded yet; the declaration stands as the terminal dimension readout of the spatial-topology forcing certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.