grayCycle3_realizes_circle
plain-language theorem explainer
The canonical 3-bit Gray cycle, realized inside any 3-dimensional cellular completion, has recognized defect equal to the circle S¹. Forcing-chain authors cite this when wiring T7 (eight-tick octave) into the T7-to-realization bridge. The proof is a one-line specialization of the general Hamiltonian cube-walk realization theorem at dimension 3.
Claim. For any cellular completion of the 3-cube, the realized defect of the canonical 3-bit Gray closed walk equals the circle defect $S^1$.
background
Module T7CycleRealization supplies the strengthened T7/T8 dimension route at predicate level: a T7 closed cycle is graph-shaped, so its realized defect is a circle, and no cube closed walk realizes a higher sphere $S^p$ for $p\ge 2$. Smooth topology is kept propositional; only finite-dimensional arithmetic and the exact names needed by the forcing chain are proved.
RealizedDefect records the paper conclusion that a cube closed walk in a cellular completion realizes as a circle. Circle is the circle constructor of the recognized-defect type. The walk in view is the canonical 3-bit Gray cycle on the 3-cube (period $2^3=8$), matching the T7 eight-tick octave of the forcing chain.
The general sibling t7_cycle_realizes_circle states that any Hamiltonian closed walk on the $D$-cube with $D\ge 2$ realizes as the circle; the present theorem fixes $D=3$ and that walk.
proof idea
One-line term wrapper. Apply the general realization theorem t7_cycle_realizes_circle at dimension $3$, discharge $3\ge 2$ by decide, pass the given cellular completion, the canonical Gray closed walk grayCycle3ClosedWalk, and the Hamiltonian certificate grayCycle3ClosedWalk_hamiltonian. No further case analysis.
why it matters
Feeds the forcing-chain bridge constructor t7_to_realization_bridge_holds, which sets realizes_as_circle to this theorem (and pairs it with the companion no-higher-sphere fact). That bridge is the T7 realization step on the path from T7 (eight-tick octave, period $2^3$) toward T8 ($D=3$ spatial dimensions).
Without a named specialization to the Gray 3-cycle, the chain cannot cite a concrete walk whose defect is $S^1$. The module deliberately stays predicate-level, matching the Alexander-duality discipline and deferring full CW/covering-dimension work to a later Mathlib pass; this theorem is the exact API surface the unified forcing chain imports.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.