SpatialGeometry
plain-language theorem explainer
Enumerates the three constant-curvature spatial geometries: flat, spherical, and hyperbolic. Downstream topology-forcing arguments quantify over this type when excluding curved options. The declaration is a pure inductive type with no proof content; it supplies the discrete case split used by the φ-self-similarity flatness theorem.
Claim. A spatial geometry is one of three constant-curvature types: flat ($K = 0$), spherical ($K > 0$), or hyperbolic ($K < 0$).
background
The module derives the spatial topology of the recognition substrate from three joint constraints: homogeneity from the comparison law, flatness from φ-self-similarity, and the Bieberbach classification of compact orientable flat 3-manifolds. The end target is the 3-torus $T^3$.
In classical Riemannian geometry, a simply connected complete manifold of constant sectional curvature is isometric to Euclidean space, the sphere, or hyperbolic space. This inductive type packages exactly that trichotomy for the substrate metric.
The comparison cost $J(x) = \cosh(\log x) - 1$ is scale-free: it depends only on ratios. A preferred curvature radius $R$ would break that scale invariance under the self-similar map $x \mapsto x^\varphi$, which is why the geometry type must later be forced to flat.
proof idea
No proof: this is an inductive definition with three nullary constructors (flat, spherical, hyperbolic). Downstream theorems case-split on the type or pass a value of it as a hypothesis.
why it matters
This type is the discrete domain for self_similarity_forces_flat, which states that φ-self-similarity excludes non-flat geometries: a finite curvature radius $R$ supplies a preferred scale, so the map $x \mapsto x^\varphi$ changes $L/R$ across scales and breaks the comparison law's scale invariance. Only flat geometry ($R = \infty$) survives.
That flatness step is the second of three substrate constraints in the module derivation (homogeneity, flatness, Bieberbach). Together they force $T^3$ among compact orientable flat 3-manifolds, aligning with the forcing-chain landmark that spatial dimension is three (T8) and with the eight-tick octave structure living on a homogeneous spatial substrate.
Without this enumeration, the flatness theorem would have no typed case split between curved and flat options.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.