t7_cycle_realizes_circle
plain-language theorem explainer
In any cellular completion of the D-cube (D ≥ 2), a Hamiltonian closed walk realizes as the circle defect S¹. Dimension and forcing-chain authors cite this as the graph-shaped T7 realization step. The proof is definitional reflexivity: RealizedDefect is currently the constant Circle map.
Claim. For every dimension $D \ge 2$, every cellular completion of the $D$-cube, and every Hamiltonian closed walk $W$ on that cube (a bijective phase-indexed path through all $2^D$ vertices), the realized defect of $W$ equals the circle defect.
background
The module supplies a theorem surface for the strengthened T7/T8 dimension route: the T7 closed cycle is graph-shaped, so its realized defect is a circle $S^1$, and no closed cube walk realizes a higher sphere $S^p$ for $p \ge 2$. Smooth-topology content stays predicate-level; the file proves elementary finite-dimensional arithmetic and exposes the names the forcing chain needs.
A closed walk on the $D$-cube is a map from $\mathrm{Fin}(2^D)$ into the $D$-bit pattern space. Hamiltonian means that map is bijective: every vertex is visited exactly once. Cellular completion (T7.5a) packages three structural clauses used in the dimension paper: a closed orientable smooth $D$-manifold substrate, a tame cube-graph embedding, and a retraction back to the cube graph (presently proof placeholders).
Recognized defects include the circle constructor. RealizedDefect is defined, at this stage, to return that circle constantly, recording the paper's conclusion that a T7 graph-shaped cycle realizes as $S^1$.
proof idea
One-line reflexivity. RealizedDefect is definitionally the constant function returning Circle, independent of the cellular completion and the walk. After the type-class and hypothesis context is assembled, rfl closes the goal. The hypotheses $D \ge 2$ and Hamiltonian are part of the intended API surface but are not consulted by the current definitional body.
why it matters
This is the main T7 cycle-realization theorem named in the module doc: Hamiltonian T7 closed walks realize as circles inside a cellular completion. It feeds the specialization grayCycle3_realizes_circle, which instantiates the result at the canonical 3-bit Gray cycle on $Q_3$ (the eight-tick octave of forcing step T7, period $2^3$).
In the Recognition forcing chain, T7 forces the eight-tick octave and T8 forces spatial dimension $D = 3$. The present lemma is the graph-to-defect bridge on that route: the cube cycle is not an arbitrary loop but a Hamiltonian walk whose realized defect is $S^1$, blocking higher-sphere realizations from closed cube walks. The module deliberately matches the AlexanderDuality discipline, keeping CW and covering-dimension formalization for a later Mathlib-backed pass while locking the exact theorem names the chain consumes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.