totalChiralCharge
plain-language theorem explainer
Integer measuring total chirality of the eight-tick Hamiltonian cycle on the 3-cube: double sum of absolute edge-to-face signs over all eight steps and six faces. Geometric CP-violation work cites it as the scalar asymmetry of the cycle against face boundaries. Defined by direct summation of absolute signed contributions; nonzero means the cycle is chiral.
Claim. The total chiral charge is the integer $\sum_{i \in \mathrm{Fin}\,8}\sum_{f \in F} |\sigma(i,f)|$, where $F$ is the list of six faces of $Q_3$ and $\sigma(i,f)\in\{-1,0,+1\}$ is the signed contribution of cycle edge $i$ to face $f$ (zero off the face).
background
The module FaceWinding equips the 3-cube $Q_3$ with signed winding numbers of a fixed Hamiltonian 8-cycle around each face. That geometry is the RS origin of CP violation: each face of $Q_3$ is tied to a generation pair, and a nonzero winding means the cycle distinguishes clockwise from counterclockwise boundary travel.
allFaces enumerates the six faces as pairs (fixed axis, fixed bit). For each cycle step and face, edgeFaceSign returns $+1$ or $-1$ when the directed cycle edge lies on the face and traverses its boundary positively or negatively, and $0$ otherwise. The eight-tick structure is the T7 octave; spatial $D=3$ is the T8 forcing step that makes $Q_3$ the right complex.
Upstream face maps from CircleWindingChain and SingularPrism supply the simplicial language; here only the combinatorial cube faces and the cycle edge list are used.
proof idea
Pure definition: expand as a double sum over Fin 8 (cycle steps) and the finset of allFaces, taking the natural absolute value of each edgeFaceSign and coercing to $\mathbb{Z}$. No lemmas, no tactics.
why it matters
Supplies the scalar that MODULE_DOC lists among the main FaceWinding results: a single integer that is nonzero precisely when the eight-tick cycle is chiral relative to the cube faces. That chirality is the geometric seed of CP violation in Recognition Science, sitting on the T7 eight-tick octave and the T8 $D=3$ cube.
No downstream consumers are wired yet in the dependency graph. The module narrative claims the quantity is proved nonzero; the present declaration only defines the sum. A later nonvanishing theorem would close that claim and feed particle-generation and gauge-from-cube arguments that already import this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.