module module

`IndisputableMonolith.Foundation.SpatialTopologyForcing`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (13)

structure SubstrateSymmetryProperties L62
def recognitionSubstrateProperties L76
inductive SpatialGeometry L86
theorem self_similarity_forces_flat L96
inductive BieberbackType L112
def firstBettiNumber L121
theorem torus3_unique_b1_3 L130
theorem isotropy_forces_b1_eq_3 L139
theorem spatial_topology_forcing L157
theorem spatial_dimension_eq_3 L164
structure SpatialTopologyForcingCert L169
def spatialTopologyForcingCert L174
theorem spatialTopologyForcingCert_inhabited L179