module module

`IndisputableMonolith.Foundation.T7CycleRealization`

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.UnifiedForcingChain module_import
IndisputableMonolith.Verification.T6T8SpineAudit module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.SubstrateAxioms module_import
IndisputableMonolith.Patterns.GrayCycle module_import

declarations in this module (16)

structure ClosedWalkOnCube L27
def Hamiltonian L31
def EdgeDistinct L36
def ImageIsCircle L39
def ImageIsSpherePofDim L44
inductive RecognizedDefect L48
def Circle L55
def RealizedDefect L60
theorem edge_distinct_of_dim_ge_two L68
theorem closed_walk_image_is_circle L75
theorem no_higher_sphere_from_closed_walk L82
theorem t7_cycle_realizes_circle L92
def grayCycle3ClosedWalk L100
theorem grayCycle3ClosedWalk_hamiltonian L104
theorem grayCycle3_realizes_circle L109
theorem grayCycle3_no_higher_sphere L116