faceWinding
plain-language theorem explainer
The signed winding of the eight-tick Gray cycle around one face of the 3-cube equals the sum of that edge's signed boundary contributions over all eight cycle steps. Anyone computing face-level chirality or total chiral charge on Q₃ cites this. The body is a direct finite sum of the per-step edge-face signs.
Claim. For a face $f$ of the $3$-cube (fixed axis in $\{0,1,2\}$ and side $0$ or $1$), the face winding is $W(f) := \sum_{i=0}^{7} \sigma(i,f) \in \mathbb{Z}$, where $\sigma(i,f)\in\{+1,-1,0\}$ is the signed contribution of cycle edge $i$ to the oriented boundary of $f$ ($0$ if the edge does not lie on $f$).
background
The module treats Hamiltonian cycles on the $3$-cube $Q_3$ as the geometric carrier of the eight-tick octave. Each face is a pair (fixed coordinate axis, fixed side $0$ or $1$), so there are six faces. The cycle is the standard Gray-code walk on the eight vertices; each step flips one bit and therefore traverses one directed edge.
The local signed contribution of step $i$ to face $f$ is zero unless that edge lies on $f$. When it does, the sign is $+1$ or $-1$ according to whether the flipped bit moves the free coordinate "up" relative to the face orientation. Summing those eight integers yields the net how many times the cycle wraps the face boundary clockwise versus counterclockwise.
Physically, each face pairs with a generation structure; nonzero winding means the cycle distinguishes forward from backward on that face, which the module identifies as the geometric seed of CP violation in Recognition Science.
proof idea
Pure definition: no proof obligations. The value is the finite sum $\sum_{i:\mathrm{Fin},8}\mathrm{edgeFaceSign}(i,f)$, where the summand already returns $0$ off-face and $\pm 1$ on-face. Evaluation is therefore a direct eight-term integer sum once the edge-on-face and orientation predicates are fixed.
why it matters
This is the atomic face-level chirality measure in the Face Winding module. Downstream, allWindings maps it over the six faces, and netChiralCharge folds the signed sum; the module's main theorem line then targets a nonzero total chiral charge. That nonzero total is the geometric origin of CP violation claimed in the module doc: the eight-tick cycle does not treat every face boundary symmetrically.
In the broader forcing chain this sits under the T7 eight-tick octave and the $D=3$ cube geometry (T8). Without a well-defined integer winding per face, the later chiral-charge and generation-pair arguments have nothing to sum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.