grayCycle3ClosedWalk_hamiltonian
plain-language theorem explainer
The explicit 3-bit Gray cycle on the cube graph Q₃ is Hamiltonian: its path visits every vertex exactly once. Anyone citing the T7 eight-tick realization or the circle-defect specialization needs this fact. The proof is a one-line reduction to the known bijectivity of the Gray-cycle path map.
Claim. The closed walk given by the standard 3-bit Gray cycle on the 3-cube is Hamiltonian: its path map is bijective on the vertex set, so it visits every vertex of $Q_3$ exactly once.
background
Module T7CycleRealization supplies the elementary graph-arithmetic surface for the strengthened T7/T8 dimension route: a T7 closed cycle is graph-shaped, so its realized defect is a circle $S^1$, and no closed walk in a cube graph realizes a higher sphere $S^p$ for $p\ge 2$. Smooth topology stays predicate-level; the module only proves finite-dimensional arithmetic and names the theorems the forcing chain needs.
A closed walk on the $D$-cube is a path that returns to its start. Hamiltonian means that path is bijective on vertices (visits every vertex exactly once). The object under study is the explicit 3-bit Gray cycle packaged as a closed walk on $Q_3$, whose underlying path is the standard Gray-code enumeration of ${0,1}^3$.
T7 in the forcing chain is the eight-tick octave (period $2^3$). The Gray cycle is the concrete combinatorial model of that period-8 loop on the 3-cube.
proof idea
One-line term proof. Unfold the definitions of Hamiltonian (bijectivity of the walk path) and of the explicit 3-bit Gray closed walk, then apply Patterns.grayCycle3_bijective, which already records that the Gray-cycle path on three bits is a bijection. simpa discharges the goal.
why it matters
This is the Hamiltonian hypothesis required by the specialization grayCycle3_realizes_circle: that theorem feeds the walk and this fact into the general realization lemma t7_cycle_realizes_circle, concluding that the realized defect of the canonical 3-bit Gray cycle is the circle. Without bijectivity, the walk would not cover the full vertex set and the defect would not be forced to $S^1$.
In the Recognition forcing chain this pins the T7 eight-tick octave as a genuine Hamiltonian cycle on $Q_3$, the combinatorial substrate for period $2^3$. Downstream the same surface supports the T7/T8 claim that closed cube walks realize circles and never higher spheres, keeping the dimension route elementary until a full CW/covering-dimension pass.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.