spatialTopologyForcingCert_inhabited
plain-language theorem explainer
The master certificate that spatial topology is forced to the 3-torus is inhabited: flatness, uniqueness of b₁=3 among Bieberbach types, and D=3 are jointly realized. Anyone citing the T⁸/D=3 forcing step or the substrate-to-T³ derivation uses this existence fact. The proof is a one-line term witness packaging the concrete certificate value.
Claim. There exists a spatial-topology forcing certificate: a record asserting that flat geometry is forced, that among compact orientable flat 3-manifolds the unique type with first Betti number $b_1=3$ is the 3-torus $T^3$, and that $b_1(T^3)=3$ (hence spatial dimension $D=3$).
background
The module derives spatial topology from recognition-substrate constraints. The substrate is treated 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 $x\mapsto x^\varphi$ then forces flat geometry: curvature would introduce a preferred scale and break scale invariance at all scales.
Among compact orientable flat 3-manifolds, the Bieberbach list has six types. Only the 3-torus has first Betti number $b_1=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 flatness placeholder, the uniqueness implication "$b_1=3\Rightarrow T^3$", and the identity $b_1(T^3)=3$.
The concrete value spatialTopologyForcingCert fills those fields with trivial, the uniqueness lemma for $b_1=3$, and reflexivity.
proof idea
One-line term proof: inhabit Nonempty SpatialTopologyForcingCert by the anonymous constructor applied to the already-built certificate value. That value wires flat_forced to True.intro, torus_forced to the uniqueness lemma that only the 3-torus among Bieberbach types has $b_1=3$, and dimension_eq_3 to rfl on the Betti-number table entry for $T^3$.
why it matters
This is the inhabitance seal on the module's master certificate for spatial topology forcing. It closes the structural claim that substrate homogeneity, $\varphi$-self-similarity, and Bieberbach classification jointly force $T^3$, with spatial dimension identified as $b_1(T^3)=3$. That is the local realization of framework landmark T8 ($D=3$ spatial dimensions) inside the Foundation forcing chain.
No downstream dependents are recorded yet; the declaration stands as the exportable existence fact for the certificate type. Status is fully proved (zero sorry, no RS-internal axiom). It does not itself re-prove flatness or the Bieberbach census; those are upstream structural inputs packaged here for citation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.