edgeFaceSign
plain-language theorem explainer
Signed contribution of one Gray-code cycle edge to the winding of a chosen face of the 3-cube. Returns +1 or -1 when the directed edge lies on that face boundary (oriented by free-axis order and face side), and 0 otherwise. Cited by anyone assembling face windings or total chiral charge. Pure definitional case analysis on incidence, move direction, and side.
Claim. For each step $s \in \{0,\ldots,7\}$ of the canonical Gray-code Hamiltonian cycle on the 3-cube $Q_3$ and each face $f$ (fixed axis and side bit), the signed edge contribution is an integer: $0$ if the directed edge at step $s$ is not incident to $f$; otherwise $\pm 1$ according to whether the flipped bit is the first free axis of $f$, whether the edge moves that bit from $0$ to $1$, and whether $f$ is the outer ($1$) or inner ($0$) side.
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 foundation for CP violation: each face pairs with a generation pair, and a nonzero winding means the eight-tick cycle distinguishes forward from backward on that face boundary.
A face is a pair (fixed axis in ${0,1,2}$, side bit). The cycle is the standard Gray-code loop on eight vertices, with directed edges cycleEdges and flipped coordinate flippedBit at each step. An edge is incident to a face precisely when it does not flip the face axis and both endpoints carry the face side bit (edgeOnFace). The two free axes of a face order the boundary; the first free axis sets the orientation convention.
The eight-tick period and $D=3$ are the T7/T8 landmarks of the forcing chain; here they appear as the Gray cycle on $Q_3$ and the six faces of that cube.
proof idea
Definitional, not a proved theorem. First gate: if the step edge is not on the face, return $0$. Otherwise read the directed edge, the flipped bit (move axis), whether the move is upward on that bit, whether that axis is the first free axis of the face, and the face side bit. An eight-way match on (isFirstFreeAxis, movesUp, side) assigns $\pm 1$ so that first-axis upward on the outer side is $+1$, with the three other first-axis cases and the four second-axis cases completing the orientation table (inner side and second free axis flip relative to the outer first-axis convention).
why it matters
This is the atomic signed weight inside face winding: faceWinding is exactly the sum of these contributions over the eight cycle steps. The same weights feed totalChiralCharge (sum of absolute contributions over steps and all faces), which measures net chirality of the cycle against face boundaries and is the module's stated nonzero chiral invariant.
In the RS story, nonzero face winding is the geometric origin of CP violation: the eight-tick Gray cycle on $Q_3$ (T7 octave, T8 spatial dimension three) wraps faces asymmetrically, so forward and backward boundary traversals are distinguished. Without a coherent edge-to-face sign, the winding sum and the chiral-charge totals cannot be stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.