CubeFace
plain-language theorem explainer
A face of the 3-cube Q₃ is labeled by which coordinate is held fixed (an axis in {0,1,2}) and which value that coordinate takes (0 or 1). This is the basic geometric type for face-winding calculations that underwrite CP violation in RS. Anyone citing face windings, edge incidence, or total chiral charge uses this carrier. It is a plain structure with decidable equality; no proof content.
Claim. A face of the unit 3-cube $Q_3$ is a pair $(a,s)$ where $a\in\{0,1,2\}$ is the fixed coordinate axis and $s\in\{0,1\}$ is the constant value of that coordinate on the face. The six faces are exactly the sets $\{x\in\{0,1\}^3:x_a=s\}$.
background
The module FaceWinding equips the 3-cube $Q_3$ with signed winding numbers of a Hamiltonian cycle (the eight-tick Gray code) around each face. Physically, each face corresponds to a generation pair; nonzero winding is the geometric origin of CP violation in Recognition Science.
A face is the 2-dimensional subcube obtained by fixing one bit. The axis field is that fixed coordinate in $\mathrm{Fin},3$; the side field is the Boolean value of the fixed bit. The complementary two axes are the free directions along which the face boundary is traversed.
Downstream definitions build on this carrier: the explicit list of six faces, incidence of cycle edges on a face, free-axis projections, signed edge contributions, and the net face winding as a sum over the eight cycle steps.
proof idea
No proof: this is a structure declaration. It packages two fields (axis : Fin 3, side : Bool) and derives DecidableEq and Repr so faces can be compared and printed in later combinatorial arguments. All mathematical content lives in the consumers (allFaces, edgeOnFace, faceWinding, etc.).
why it matters
CubeFace is the first main result listed in the module: the explicit enumeration type for the six faces of $Q_3$. Every subsequent object in the face-winding pipeline takes a CubeFace argument: allFaces lists the six instances; edgeOnFace and edgeFaceSign decide incidence and signed boundary contribution; freeAxes returns the two unfixed axes; faceWinding sums signed contributions over the eight-tick cycle.
That pipeline feeds totalChiralCharge (sum of face windings, proved nonzero), which is the geometric CP-violation signal. The setting sits on the T7 eight-tick octave and T8 forcing of $D=3$ spatial dimensions: only in three dimensions does $Q_3$ have six faces whose windings can encode generation-pair chirality. Without this carrier type the winding calculus has nothing to index.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.