module module

`IndisputableMonolith.Foundation.SubstrateAxioms`

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

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Foundation.DimensionForcing module_import
IndisputableMonolith.Foundation.T7CycleRealization module_import
IndisputableMonolith.Foundation.UnifiedForcingChain module_import

declarations in this module (11)

abbrev Dimension L21
structure CellularCompletion L28
theorem cellular_completion_trivial L36
structure OneAcyclicSubstrate L43
theorem one_acyclic_trivial L47
structure LoopEntanglement L54
theorem loop_entanglement_circle_witness L58
structure CompatibilityWithRealizedCycle L64
theorem compatibility_trivial L68
structure T75SubstratePackage L73
theorem substrate_package_trivial L80