EdgeDistinct
plain-language theorem explainer
Edge-distinctness is a predicate on closed walks of the D-cube, currently the trivial proposition True. It stands in for a future edge-level statement once cube-edge objects are factored out of the Gray-cycle API. The T7 edge-distinctness theorem for D ≥ 2 and the T6–T8 spine audit both cite it. The body is a one-line definitional placeholder, not a combinatorial argument.
Claim. For any dimension $D$ and any closed walk $W$ on the $D$-cube (a phase-indexed path through the $D$-bit pattern space), the edge-distinctness predicate on $W$ is the trivial proposition $\top$.
background
The module strengthens the T7/T8 dimension route: the T7 closed cycle is graph-shaped, so its realized defect is a circle $S^1$, and no closed walk in the cube graph realizes a higher sphere $S^p$ for $p \ge 2$. Smooth-topology content is kept predicate-level; only elementary finite-dimensional arithmetic is proved, matching the Alexander-duality discipline while deferring full CW/covering-dimension work.
A closed walk on the $D$-cube is a map from $\mathrm{Fin}(2^D)$ into the $D$-bit pattern space. Hamiltonian walks visit every vertex once. Spatial dimension $D$ is forced to 3 by T8 (and appears as the constant 3 in several sibling modules). Edge distinctness is the missing combinatorial layer: successive steps of the walk should use distinct cube edges in the sense needed for a circle realization.
The doc-comment states the intent explicitly: keep the predicate until a generic edge API is factored out of Patterns.GrayCycle.
proof idea
There is no proof content. The declaration is a definition whose right-hand side is the constant proposition True, ignoring the walk argument. Downstream theorems that need the predicate (for example the D ≥ 2 Hamiltonian case) discharge it by trivial or by definitional rewriting to True.
why it matters
In the forcing chain, T7 is the eight-tick octave (period $2^3$). This predicate is the named interface for the edge-level half of the T7 cycle-realization surface: once nontrivial, it underwrites that a Hamiltonian cube walk has edge-distinct realizability, which feeds the claim that the realized defect is a circle and not a higher sphere.
Immediate consumers are edge_distinct_of_dim_ge_two (Part (i) of the intended API, still discharged by trivial) and the T6–T8 spine audit, which records that EdgeDistinct is definitionally True. The audit theorem t7_edge_distinct_is_placeholder makes that status explicit for verification. Closing the placeholder is the remaining combinatorial step before the T7 realization layer is no longer predicate-level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.