allFaces
plain-language theorem explainer
Explicit list of the six faces of the 3-cube Q₃, each tagged by fixed axis and side. Anyone computing face windings, edge-face incidence, or chiral charge on the eight-tick Gray cycle cites this roster. The body is a six-element literal of CubeFace pairs, one per coordinate hyperplane.
Claim. The complete face set of the unit 3-cube $Q_3$ is the six-element list $\{(x=0),\,(x=1),\,(y=0),\,(y=1),\,(z=0),\,(z=1)\}$, where each face is a pair $(\mathrm{axis},\mathrm{side})$ with $\mathrm{axis}\in\{0,1,2\}$ and $\mathrm{side}\in\{0,1\}$.
background
The module FaceWinding equips the 3-cube $Q_3$ with signed winding numbers of a Hamiltonian cycle around each face. That geometry is the RS origin of CP violation: nonzero winding means the eight-tick cycle distinguishes clockwise from counterclockwise on a face boundary.
A face is a CubeFace: an axis in $\mathrm{Fin},3$ (which coordinate is held fixed) together with a Boolean side (the fixed value 0 or 1). The three spatial axes come from the dimension-forcing chain (T8: $D=3$); the cycle itself is the Gray-code octave of period $2^3$ (T7).
This definition simply materializes the six faces so later maps (windings, incidence filters, chiral sums) can range over a concrete list rather than an abstract type.
proof idea
Pure data definition: a six-element list literal pairing each axis $0,1,2$ with both Boolean sides. No lemmas or tactics; decidable equality on CubeFace makes native_decide available downstream.
why it matters
Parent results that consume the list include allFaces_length and face_count_matches (cardinality 6 equals the combinatorial face count of the 3-cube), allWindings and faceWinding (per-face signed boundary traversal), each_edge_on_two_faces (incidence), face_pairs_have_three_axes, and the chiral aggregates netChiralCharge and totalChiralCharge.
Those charges are the module's main physical output: the sum of absolute face windings is proved nonzero, giving a geometric CP-odd invariant on the eight-tick cycle. Faces also line up with generation pairs from ParticleGenerations, so the same roster feeds the three-generation structure. Without an explicit face list, none of the winding or chirality theorems can even be stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.