spatialTopologyForcingCert
plain-language theorem explainer
Canonical witness packing the three spatial-topology forcing claims: flat geometry is recorded as forced, among the six compact orientable flat 3-manifolds only the 3-torus has first Betti number 3, and that Betti number equals 3. Anyone citing the T³ substrate or D = 3 from topology will point here. The construction is a three-field structure instance: trivial, the uniqueness theorem, and rfl.
Claim. There is a certificate asserting: (i) flatness of the spatial substrate is forced; (ii) for every compact orientable flat 3-manifold type $B$ in the Bieberbach list, if the first Betti number satisfies $b_1(B)=3$ then $B$ is the 3-torus $T^3$; (iii) $b_1(T^3)=3$.
background
The module derives spatial topology from recognition-substrate constraints. The substrate is modeled as 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 the golden-ratio scaling forces flat geometry: any nonzero curvature radius would break scale invariance.
Among compact orientable flat 3-manifolds the Bieberbach classification yields six types (all crystallographic quotients of $\mathbb{R}^3$). Their first Betti numbers $b_1=\mathrm{rank},H^1(M;\mathbb{Z})$ are 3 only for $T^3=\mathbb{R}^3/\mathbb{Z}^3$; the half-, quarter-, third-, and sixth-turn flats have $b_1=1$, and Hantzsche–Wendt has $b_1=0$.
The certificate structure packages three fields: a placeholder that flatness is forced, the uniqueness implication $b_1(B)=3\Rightarrow B=T^3$, and the equality $b_1(T^3)=3$. Upstream, torus3_unique_b1_3 proves the uniqueness clause by case analysis on the six types.
proof idea
Three-field structure instance, not a deep proof. The flatness field is filled by trivial (the Prop is True). The torus-uniqueness field is exactly the theorem that only $T^3$ has $b_1=3$, applied as a term. The dimension field is rfl on the definitional equality firstBettiNumber torus3 = 3. No further tactics.
why it matters
This is the master certificate for spatial topology forcing in the Foundation layer. Downstream, spatialTopologyForcingCert_inhabited simply wraps it to obtain Nonempty SpatialTopologyForcingCert, closing the module's inhabitance claim.
In the Recognition forcing chain this lands at T8: spatial dimension $D=3$ is identified with $b_1(T^3)$. The module status line records a structural theorem with zero sorry and no RS-internal axioms. Together with flatness-from-$\varphi$-self-similarity and substrate homogeneity, the certificate pins the recognition substrate to the 3-torus rather than any other Bieberbach quotient, which is the topological side of why space is three-dimensional and periodic under the lattice cover.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.