edge_distinct_of_dim_ge_two
plain-language theorem explainer
For spatial dimension at least two, every Hamiltonian closed walk on the D-cube satisfies edge-distinct realizability. Anyone wiring the T7 cycle-realization surface (circle image of the eight-tick walk) cites this API lemma. The proof is a one-line discharge: edge-distinctness is presently the unit proposition, with the real edge-level argument deferred until cube edges are factored out of the Gray-cycle layer.
Claim. Let $D\ge 2$ be a natural number and let $W$ be a closed walk on the $D$-dimensional hypercube that visits every vertex exactly once (i.e., whose phase-indexed path $W:\mathrm{Fin}(2^D)\to\{0,1\}^D$ is bijective). Then $W$ is edge-distinct.
background
Module T7CycleRealization supplies the 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 stays predicate-level; only elementary finite-dimensional arithmetic is proved here.
A closed walk on the $D$-cube is a phase-indexed path through the $D$-bit pattern space, i.e. a map $\mathrm{Fin}(2^D)\to\mathrm{Pattern},D$. Hamiltonian means that path is bijective: every vertex is visited exactly once. Edge-distinctness is the intended combinatorial condition that successive steps use distinct cube edges; it is kept as the unit proposition until a generic edge API is factored out of Patterns.GrayCycle.
Upstream, spatial dimension is forced to $D=3$ by T8 (and again by the linking argument labeled T9). The present lemma is dimension-parametric and only needs $D\ge 2$.
proof idea
One-line tactic proof: trivial. Because EdgeDistinct is definitionally True for any closed walk, the goal is immediate once the hypotheses (dimension bound and Hamiltonian) are in context. No combinatorial edge reasoning is performed; the declaration only locks the intended API name and hypothesis shape for later discharge when cube-edge objects exist.
why it matters
This is Part (i) of the T7 cycle-realization package. Together with the sibling claims that a Hamiltonian closed walk has circle image and that no closed cube walk realizes $S^p$ for $p\ge 2$, it underwrites the forcing-chain step T7: the eight-tick octave is a genuine $S^1$ defect, not a higher sphere. That circle image is what later feeds the winding/homology side of the dimension route (T8 forces $D=3$).
The lemma itself has no downstream users yet in the graph; it exists to expose stable names matching the Alexander-duality discipline while the edge API remains unfactored. Closing the deferred edge-level proof will turn the present triviality into a genuine combinatorial statement without renaming the theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.