DirectedEdge
plain-language theorem explainer
A directed edge on the 3-cube is an ordered pair of vertices, each labeled by an index in {0,...,7}. It is the atomic carrier for the Gray-code Hamiltonian cycle and its reverse. Anyone computing face windings or edge orientations for CP-violation geometry cites this type. The declaration is a bare structure with decidable equality; no proof content.
Claim. A directed edge of the 3-cube $Q_3$ is an ordered pair $(s,d)$ with $s,d\in\{0,\ldots,7\}$, intended as the source and target of a one-bit flip between 3-bit vertex patterns.
background
The module builds signed winding numbers of a Hamiltonian cycle on the 3-cube $Q_3$ around each of its six faces. That geometry is the RS account of CP violation: each face pairs particle generations, and a nonzero winding distinguishes forward from backward traversal of the face boundary.
Vertices of $Q_3$ are the eight 3-bit strings, identified with Fin 8. The canonical 8-tick schedule is the Gray-code cycle $0\to 1\to 3\to 2\to 6\to 7\to 5\to 4\to 0$. A directed edge is simply the ordered pair of endpoints of one step of such a cycle (or its reverse). The doc-comment states the intended meaning: a pair of 3-bit patterns joined by a single bit flip.
Downstream lists assemble the eight forward edges and the eight reversed edges from this type; orientation and winding then count how those edges traverse each face boundary.
proof idea
No proof: this is a two-field structure (source and destination in Fin 8) with derived decidable equality and a printable representation. Inhabitants are written as constructors ⟨s, d⟩. All content lives in the consumers that populate and compare these pairs.
why it matters
Face winding is the geometric origin of CP violation in Recognition Science: nonzero net signed traversal of a face boundary means the eight-tick cycle distinguishes chirality at that generation pair. This structure is the edge atom for that count.
It is consumed by the canonical Gray-code edge list, by the reversed-cycle edge list, and by the theorem that reversal swaps endpoints of every edge. Those feed edge-on-face tests, edge-face signs, and finally the net face winding and total chiral charge (proved nonzero in the module). The construction sits on the T7 eight-tick octave and the $D=3$ cube forced upstream; without a directed edge type there is nothing to orient on the faces.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.