reversedCycleEdges
plain-language theorem explainer
Explicit table of the eight directed edges obtained by walking the canonical Gray-code Hamiltonian cycle on the 3-cube backwards. Anyone proving orientation-reversal identities for face windings cites this pairing. The body is a pure case split on Fin 8, listing each reversed source–target pair.
Claim. Define a map $r:\{0,\ldots,7\}\to E(Q_3)$ sending each step index to a directed edge of the 3-cube by traversing the canonical 8-tick Gray-code cycle in reverse order: $0\mapsto(0,4)$, $1\mapsto(4,5)$, $2\mapsto(5,7)$, $3\mapsto(7,6)$, $4\mapsto(6,2)$, $5\mapsto(2,3)$, $6\mapsto(3,1)$, $7\mapsto(1,0)$.
background
The module FaceWinding equips the 3-cube $Q_3$ with signed winding numbers of a Hamiltonian cycle around each of its six faces. Those windings are the geometric seed of CP violation in Recognition Science: each face pairs particle generations, and a nonzero winding distinguishes forward from backward boundary travel.
A directed edge is a pair of 3-bit vertices joined by a single bit flip. The forward cycle (documented alongside the directed-edge structure) walks the Gray-code order $0\to1\to3\to2\to6\to7\to5\to4\to0$. The present definition supplies the opposite walk, so orientation comparisons become pure table lookups.
This sits inside the eight-tick octave forced at T7 of the unified forcing chain: period $2^3$ on the cube whose spatial dimension $D=3$ is forced at T8.
proof idea
Pure definition by exhaustive pattern match on Fin 8. Each constructor returns a concrete DirectedEdge record (source, destination). No lemmas are invoked; the values are the reverse of the forward Gray-code edge list.
why it matters
Feeds the theorem that reversing the cycle swaps every edge's endpoints: for each step, the forward edge's source equals the reversed edge's destination and vice versa. That identity is the algebraic hinge for showing face windings change sign under cycle reversal, which is how the module separates chiral charge from orientation conventions.
In the broader RS picture this supports the claim that total chiral charge (sum of the six face windings) is nonzero, the geometric origin of CP violation. It does not itself compute windings; it only supplies the reversed edge table those later arguments need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.