Encyclopedia Foundation Foundation Spatial Topology Forcing Self Similarity Forces Flat
ARTICLE 3 claims 3 theorems
Foundation Spatial Topology Forcing Self Similarity Forces Flat
A machine-checked theorem shows that if the universe's basic recognition process is self-similar, space cannot be curved.
Why space must be flat
In geometry, a space is flat when the usual rules of Euclidean geometry hold: parallel lines stay parallel, and triangles have angles that sum to 180 degrees. A sphere is curved, as is a saddle-shaped surface. The distinction matters because the large-scale shape of the universe is a question physics has pursued for a century, and it is not settled by observation alone.
Recognition Science is a framework that starts from the idea that reality keeps a ledger, a discrete record of recognition events, and that the cost of each recognition is forced by a small set of logical conditions. From that starting point, the framework's machine-checked library of formal theorems derives a chain of results. One link in that chain is the declaration self_similarity_forces_flat. It proves that a substrate with a particular kind of self-similarity cannot be curved.
The key property is φ-self-similarity: the recognition process is invariant under a scaling by the golden ratio φ, about 1.618. On a curved manifold, the curvature radius provides a preferred scale. A sphere has an equator, a hyperbolic surface has a curvature radius, and that preferred length breaks the scale-invariance. A self-similar map that rescales lengths would change the ratio of any length to the curvature radius, so the comparison law could not stay invariant. Only a flat geometry, where the curvature radius is infinite, is compatible with self-similarity at all scales.
The theorem itself is a formal statement in the framework's library: if a spatial geometry is flat, spherical, or hyperbolic, and if self-similarity rules out the spherical and hyperbolic cases, then the geometry must be flat. The proof is a short case analysis, and it is checked by the machine with no unproved assumptions. This is a structural result within the framework, not an empirical measurement of the universe's curvature.
What the declaration does not claim is just as important. It does not say that the universe is flat. It says that a substrate with φ-self-similarity must be flat. Whether the real universe has that property is a separate question, and one the framework does not settle here. The theorem also does not say anything about the number of spatial dimensions; that is a further step in the forcing chain, using the classification of flat manifolds. And it does not claim that curved spaces are impossible in general, only that they are incompatible with this specific self-similarity condition.
THEOREM self_similarity_forces_flat · IndisputableMonolith/Foundation/SpatialTopologyForcing.lean
/-- φ-self-similarity excludes non-flat geometries.
On a curved manifold, the curvature radius R provides a preferred scale.
The self-similar map x ↦ x^φ changes the ratio L/R at different scales,
breaking the comparison law's scale-invariance. Only flat geometry
(R = ∞) is compatible. -/
theorem self_similarity_forces_flat
(geom : SpatialGeometry)
(h_compatible : geom = SpatialGeometry.flat ∨
geom = SpatialGeometry.spherical ∨
geom = SpatialGeometry.hyperbolic)
(h_self_similar : geom = SpatialGeometry.spherical → False)
(h_self_similar' : geom = SpatialGeometry.hyperbolic → False) :
geom = SpatialGeometry.flat := by
rcases h_compatible with h | h | h
· exact h
· exact absurd h h_self_similar
· exact absurd h h_self_similar'
THEOREM self_similarity_forces_flat · IndisputableMonolith/Foundation/SpatialTopologyForcing.lean
/-- φ-self-similarity excludes non-flat geometries.
On a curved manifold, the curvature radius R provides a preferred scale.
The self-similar map x ↦ x^φ changes the ratio L/R at different scales,
breaking the comparison law's scale-invariance. Only flat geometry
(R = ∞) is compatible. -/
theorem self_similarity_forces_flat
(geom : SpatialGeometry)
(h_compatible : geom = SpatialGeometry.flat ∨
geom = SpatialGeometry.spherical ∨
geom = SpatialGeometry.hyperbolic)
(h_self_similar : geom = SpatialGeometry.spherical → False)
(h_self_similar' : geom = SpatialGeometry.hyperbolic → False) :
geom = SpatialGeometry.flat := by
rcases h_compatible with h | h | h
· exact h
· exact absurd h h_self_similar
· exact absurd h h_self_similar'
THEOREM self_similarity_forces_flat · IndisputableMonolith/Foundation/SpatialTopologyForcing.lean
/-- φ-self-similarity excludes non-flat geometries.
On a curved manifold, the curvature radius R provides a preferred scale.
The self-similar map x ↦ x^φ changes the ratio L/R at different scales,
breaking the comparison law's scale-invariance. Only flat geometry
(R = ∞) is compatible. -/
theorem self_similarity_forces_flat
(geom : SpatialGeometry)
(h_compatible : geom = SpatialGeometry.flat ∨
geom = SpatialGeometry.spherical ∨
geom = SpatialGeometry.hyperbolic)
(h_self_similar : geom = SpatialGeometry.spherical → False)
(h_self_similar' : geom = SpatialGeometry.hyperbolic → False) :
geom = SpatialGeometry.flat := by
rcases h_compatible with h | h | h
· exact h
· exact absurd h h_self_similar
· exact absurd h h_self_similar'
What this page does not claim
The theorem does not claim the universe is flat. It does not claim curved spaces are impossible in general. It does not claim anything about the number of spatial dimensions.
Verify this page
Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:
$ lake env lean IndisputableMonolith/Foundation/SpatialTopologyForcing.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)
A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.
Derived articles
This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:
- What empirical evidence bears on whether the universe's recognition substrate is φ-self-similar?
- How does the flatness theorem combine with the Bieberbach classification to force the number of spatial dimensions?
- What would it mean for the framework if the universe were observed to be curved on large scales?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM self_similarity_forces_flat · IndisputableMonolith/Foundation/SpatialTopologyForcing.lean
/-- φ-self-similarity excludes non-flat geometries. On a curved manifold, the curvature radius R provides a preferred scale. The self-similar map x ↦ x^φ changes the ratio L/R at different scales, breaking the comparison law's scale-invariance. Only flat geometry (R = ∞) is compatible. -/ theorem self_similarity_forces_flat (geom : SpatialGeometry) (h_compatible : geom = SpatialGeometry.flat ∨ geom = SpatialGeometry.spherical ∨ geom = SpatialGeometry.hyperbolic) (h_self_similar : geom = SpatialGeometry.spherical → False) (h_self_similar' : geom = SpatialGeometry.hyperbolic → False) : geom = SpatialGeometry.flat := by rcases h_compatible with h | h | h · exact h · exact absurd h h_self_similar · exact absurd h h_self_similar'It proves that a substrate with a particular kind of self-similarity cannot be curved. self_similarity_forces_flat · IndisputableMonolith/Foundation/SpatialTopologyForcing.leanTHEOREM self_similarity_forces_flat · IndisputableMonolith/Foundation/SpatialTopologyForcing.lean
/-- φ-self-similarity excludes non-flat geometries. On a curved manifold, the curvature radius R provides a preferred scale. The self-similar map x ↦ x^φ changes the ratio L/R at different scales, breaking the comparison law's scale-invariance. Only flat geometry (R = ∞) is compatible. -/ theorem self_similarity_forces_flat (geom : SpatialGeometry) (h_compatible : geom = SpatialGeometry.flat ∨ geom = SpatialGeometry.spherical ∨ geom = SpatialGeometry.hyperbolic) (h_self_similar : geom = SpatialGeometry.spherical → False) (h_self_similar' : geom = SpatialGeometry.hyperbolic → False) : geom = SpatialGeometry.flat := by rcases h_compatible with h | h | h · exact h · exact absurd h h_self_similar · exact absurd h h_self_similar'On a curved manifold, the curvature radius provides a preferred scale. self_similarity_forces_flat · IndisputableMonolith/Foundation/SpatialTopologyForcing.leanTHEOREM self_similarity_forces_flat · IndisputableMonolith/Foundation/SpatialTopologyForcing.lean
/-- φ-self-similarity excludes non-flat geometries. On a curved manifold, the curvature radius R provides a preferred scale. The self-similar map x ↦ x^φ changes the ratio L/R at different scales, breaking the comparison law's scale-invariance. Only flat geometry (R = ∞) is compatible. -/ theorem self_similarity_forces_flat (geom : SpatialGeometry) (h_compatible : geom = SpatialGeometry.flat ∨ geom = SpatialGeometry.spherical ∨ geom = SpatialGeometry.hyperbolic) (h_self_similar : geom = SpatialGeometry.spherical → False) (h_self_similar' : geom = SpatialGeometry.hyperbolic → False) : geom = SpatialGeometry.flat := by rcases h_compatible with h | h | h · exact h · exact absurd h h_self_similar · exact absurd h h_self_similar'Only a flat geometry, where the curvature radius is infinite, is compatible with self-similarity at all scales. self_similarity_forces_flat · IndisputableMonolith/Foundation/SpatialTopologyForcing.lean