SpatialTopologyForcingCert
plain-language theorem explainer
Master certificate packaging three claims that force spatial topology to the 3-torus and identify D = 3 with its first Betti number. Anyone citing the spatial-topology forcing chain (flatness, uniqueness of b₁ = 3, dimension) uses this bundle. It is a pure structure definition whose fields are discharged by trivial, the uniqueness lemma, and rfl.
Claim. A certificate asserting: (i) flat geometry is forced; (ii) among the six compact orientable flat 3-manifolds (Bieberbach types), if the first Betti number equals 3 then the manifold is the 3-torus $T^3$; (iii) the first Betti number of $T^3$ is exactly 3.
background
The module derives spatial topology from recognition-substrate constraints. The substrate is a compact orientable 3-manifold. Homogeneity follows because the comparison cost $J(x) = \cosh(\log x) - 1$ depends only on ratios, so no preferred cell or boundary exists. Self-similarity under $x \mapsto x^\varphi$ then forces flatness: curvature radii would introduce preferred scales incompatible with scale-free $\varphi$-rescaling.
Among compact orientable flat 3-manifolds the Bieberbach classification yields six types (quotients of $\mathbb{R}^3$ by crystallographic groups). Their first Betti numbers $b_1 = \mathrm{rank}, H^1(M;\mathbb{Z})$ are tabulated: only $T^3$ has $b_1 = 3$; the four screw-turn flats have $b_1 = 1$; Hantzsche–Wendt has $b_1 = 0$. The inductive type enumerates those six manifolds; firstBettiNumber assigns the table values.
proof idea
No proof body: this is a structure whose three fields are propositions. Downstream, the canonical inhabitant fills flat_forced by trivial (the flatness claim is already established as a pure True placeholder at this layer), torus_forced by the uniqueness lemma that only the 3-torus has $b_1 = 3$, and dimension_eq_3 by rfl against the definitional table for the first Betti number.
why it matters
This is the §5 master cert of Spatial Topology Forcing. It packages the chain that lands on framework landmark T8: spatial dimension $D = 3$. Downstream, spatialTopologyForcingCert builds the canonical inhabitant and spatialTopologyForcingCert_inhabited records non-emptiness, so later modules can demand a single certificate rather than three separate lemmas.
The dimension field is exactly the statement that $D = 3$ is $b_1(T^3)$, matching the module claim that the forced topology is the 3-torus. Together with substrate homogeneity and $\varphi$-self-similarity forcing flatness, the cert closes the structural argument that recognition geometry must be $T^3$ with three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.