cycleEdges
plain-language theorem explainer
The canonical Gray-code Hamiltonian cycle on the 3-cube is recorded as eight directed edges in fixed order: 0→1→3→2→6→7→5→4→0. Anyone computing face windings or edge orientations on Q₃ cites this table. It is a pure case-split definition, not a proved uniqueness claim.
Claim. Define a map from step index $k \in \{0,\ldots,7\}$ to a directed edge of the 3-cube by the Gray-code cycle $0\to 1\to 3\to 2\to 6\to 7\to 5\to 4\to 0$, so each step is the ordered pair of successive vertices in that sequence.
background
The module builds signed winding numbers of a Hamiltonian cycle on the 3-cube $Q_3$ around each of its six faces. Those windings are the geometric seed of CP violation in Recognition Science: each face pairs with a generation, and a nonzero winding distinguishes forward from backward boundary travel.
A directed edge is a pair of 3-bit vertex labels joined by a single bit flip. The eight-tick octave (forcing chain T7) supplies the unique period-8 Gray cycle on $Q_3$ once $D=3$ is forced (T8). The present definition simply lists that cycle's successive edges in order.
Downstream predicates ask whether a cycle edge lies on a given face and with what sign; both read the source and target of the edge at each step index from this table.
proof idea
Pure definition by exhaustive pattern match on Fin 8. Each constructor returns a DirectedEdge record with the Gray-code source and destination for that step. No lemmas are invoked; the body is the enumeration itself.
why it matters
Face-winding arithmetic begins here. edgeOnFace tests incidence by reading the cycle edge at a step and checking the fixed face axis; edgeFaceSign then assigns $+1$, $-1$, or $0$ according to traversal direction on that face. The reversal lemma reversed_swaps_endpoints compares this table to the reversed cycle and proves endpoints swap.
Those pieces assemble into faceWinding and ultimately totalChiralCharge, the nonzero total that the module advertises as the geometric origin of CP violation. The construction sits on the eight-tick octave forced at $D=3$ (T7–T8) and on the Gray cycle imported from the patterns layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.