Encyclopedia Foundation Foundation Spatial Topology Forcing Substrate Symmetry Properties

ARTICLE 5 claims 3 theorems 2 models

Foundation Spatial Topology Forcing Substrate Symmetry Properties

A compact, flat, featureless 3-torus is the only spatial shape that satisfies five symmetry conditions at once.

The substrate's defining properties

The declaration SubstrateSymmetryProperties is a formal list of five properties that the framework's recognition substrate (the discrete record of events that reality keeps) assigns to the space it occupies. The properties are: homogeneity, meaning no cell is preferred over any other; orientability, meaning left and right are globally consistent; compactness, meaning the total volume is finite; phi-self-similarity, meaning the comparison law is scale-invariant at the golden-ratio spacing; and isotropy, meaning no direction is preferred. The declaration itself only states these properties; it does not prove that anything has them.

The framework's machine-checked library of formal results then supplies a separate definition, recognitionSubstrateProperties, which asserts that the substrate has all five properties. The library also proves a chain of consequences. The result self_similarity_forces_flat shows that phi-self-similarity excludes spherical and hyperbolic geometry, leaving only flat geometry. The result isotropy_forces_b1_eq_3 shows that, among the six compact orientable flat 3-manifolds, only the 3-torus T³ has first Betti number 3, which the framework interprets as the number of independent spatial directions. The spatial dimension result then concludes that the substrate's topology is T³ and its dimension is 3.

In plain terms, the framework claims that a space with no special points, no special directions, no boundary, finite volume, and a scale-invariant comparison law cannot be a sphere, cannot be a hyperbolic saddle, and cannot be one of the five twisted flat manifolds. The only remaining shape is the 3-torus, the three-dimensional analogue of a box whose opposite faces are glued together. The result is a structural theorem: it is proved in the library with no unproved assumptions and no framework-specific axioms.

What the declaration does not claim is just as important. It does not claim that the physical universe is literally a 3-torus, only that the recognition substrate's spatial topology is forced to be T³ under these five assumptions. It does not claim that the five properties are themselves derived from anything more basic; they are stated as the substrate's defining conditions. And it does not claim that the Bieberbach classification, the external mathematical result it relies on, is proved inside the framework; the library takes that classical result as input.

MODEL SubstrateSymmetryProperties · IndisputableMonolith/Foundation/SpatialTopologyForcing.lean
/-- The symmetry properties of the recognition substrate that determine
its spatial topology. -/
structure SubstrateSymmetryProperties where
  /-- The substrate is homogeneous: no preferred cell. -/
  homogeneous : Prop
  /-- The substrate is orientable. -/
  orientable : Prop
  /-- The substrate is compact: finite total volume. -/
  compact : Prop
  /-- The substrate is φ-self-similar: the comparison law is
  scale-invariant at the golden-ratio spacing. -/
  phiSelfSimilar : Prop
  /-- The substrate has full rotational symmetry: no preferred direction. -/
  isotropic : Prop
MODEL recognitionSubstrateProperties · IndisputableMonolith/Foundation/SpatialTopologyForcing.lean
/-- The recognition substrate has all five properties. -/
def recognitionSubstrateProperties : SubstrateSymmetryProperties where
  homogeneous := True
  orientable := True
  compact := True
  phiSelfSimilar := True
  isotropic := True
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 isotropy_forces_b1_eq_3 · IndisputableMonolith/Foundation/SpatialTopologyForcing.lean
/-- Isotropy (no preferred direction) requires b₁ = dim.
For a 3-manifold, b₁ = 3 is required for full rotational symmetry:
each independent cycle of H¹ corresponds to an independent spatial
direction, and isotropy demands all three directions be equivalent. -/
theorem isotropy_forces_b1_eq_3
    (B : BieberbackType) (h_iso : firstBettiNumber B = 3) :
    B = .torus3 :=
  torus3_unique_b1_3 B h_iso
THEOREM spatial_dimension_eq_3 · IndisputableMonolith/Foundation/SpatialTopologyForcing.lean
/-- The spatial dimension D = 3 is the first Betti number of the forced
topology T³. -/
theorem spatial_dimension_eq_3 :
    firstBettiNumber BieberbackType.torus3 = 3 := rfl

What this page does not claim

The five substrate properties are derived from anything more basic; they are stated as the substrate's defining conditions. The Bieberbach classification is proved inside the framework; it is taken as a classical external result. The physical universe is literally a 3-torus; only the recognition substrate's spatial topology is forced to be T³.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND