self_similarity_forces_flat
plain-language theorem explainer
If a spatial geometry is one of the three constant-curvature types and both spherical and hyperbolic geometries are ruled out by φ-self-similarity, the geometry must be flat. Topology-forcing arguments in the Recognition substrate cite this to discard curved backgrounds before the Bieberbach step. The proof is pure case analysis on the three-way disjunction, discharging the curved cases by the supplied absurdities.
Claim. Let $G$ be a spatial geometry of constant-curvature type (flat, spherical, or hyperbolic). If $G$ spherical is impossible and $G$ hyperbolic is impossible, then $G$ is flat.
background
The module derives the spatial topology of the recognition substrate from three substrate constraints: homogeneity from the comparison law, flatness from φ-self-similarity, and the Bieberbach classification of compact orientable flat 3-manifolds. The comparison cost is $J(x) = \cosh(\log x) - 1$, which depends only on ratios and is scale-invariant.
SpatialGeometry is the three-way inductive type of constant-curvature geometries: flat, spherical, hyperbolic. The module doc states the physical content of the flatness step: a self-similar scaling $x \mapsto x^\varphi$ needs a metric invariant under rescaling; a finite curvature radius $R$ supplies a preferred scale and breaks that invariance, so only $R = \infty$ (flat) survives.
This lemma packages that exclusion as a pure logical filter on the geometry type. It does not itself construct the curvature-radius argument; the two self-similarity hypotheses are the interfaces that carry that physics into the case split.
proof idea
Tactic proof by cases on the compatibility hypothesis that $G$ is flat, spherical, or hyperbolic. The flat branch is the goal. The spherical branch is discharged by absurd against the hypothesis that spherical geometry is false under self-similarity; the hyperbolic branch is discharged the same way against the second self-similarity hypothesis. No external lemmas are invoked beyond the inductive structure of SpatialGeometry.
why it matters
This is step 2 of the module's three-part derivation that forces $T^3$ topology on the recognition substrate. Homogeneity first forces a homogeneous 3-manifold; this lemma forces flat geometry once φ-self-similarity is imposed; Bieberbach classification then restricts to six compact orientable flat 3-manifolds, of which only the 3-torus has first Betti number 3 under isotropy.
In the broader forcing chain this supports the $D = 3$ spatial-dimension landmark (T8) by fixing not only dimension but the flat topology compatible with the φ-ladder and the eight-tick octave. The golden ratio $\varphi$ enters as the self-similar fixed point (T6): the map $x \mapsto x^\varphi$ is what makes a finite curvature radius incompatible with the scale-free comparison law (RCL / T5 J-uniqueness).
No downstream consumers are recorded yet in the graph; sibling theorems (isotropy_forces_b1_eq_3, spatial_topology_forcing, spatial_dimension_eq_3) are the natural landing sites once wired.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.