freeAxes
plain-language theorem explainer
For each face of the 3-cube, the free axes are the two coordinate directions not fixed by that face, returned as an ordered map Fin 2 → Fin 3. Anyone building edge orientations or face windings on Q₃ needs this lookup. The body is a three-way case split on the fixed axis.
Claim. Given a face $f$ of the 3-cube with fixed axis $a\in\{0,1,2\}$, the free axes of $f$ are the ordered pair of the remaining coordinates: $(1,2)$ if $a=0$, $(0,2)$ if $a=1$, and $(0,1)$ if $a=2$.
background
The module FaceWinding equips the 3-cube $Q_3$ with signed winding numbers of a Hamiltonian 8-tick cycle around each face. Those windings are the geometric source of CP violation in Recognition Science: each face pairs particle generations, and a nonzero winding distinguishes forward from backward boundary traversal.
A face is a CubeFace: an axis in $\mathrm{Fin},3$ (the fixed coordinate) together with a Boolean side (value 0 or 1 on that axis). The two free axes are exactly the coordinates that still vary on the face; they parametrize the 2-dimensional square that bounds the face and therefore the four boundary edges used later for orientation signs.
Upstream, the cube geometry and Gray-code cycle live in DimensionForcing, GaugeFromCube, and Patterns.GrayCycle. This definition is pure bookkeeping on that geometry.
proof idea
Definition by exhaustive match on the face's fixed axis. If the axis is 0, return the constant map sending $0\mapsto 1$ and $1\mapsto 2$; if axis 1, send $0\mapsto 0$ and $1\mapsto 2$; if axis 2, send $0\mapsto 0$ and $1\mapsto 1$. No lemmas are invoked.
why it matters
Parent consumer is edgeFaceSign, which assigns $+1$, $-1$, or $0$ according to whether a cycle edge traverses a face boundary positively, negatively, or not at all. That sign is the atomic summand of faceWinding, and the module's main result totalChiralCharge (sum of face windings) is proved nonzero.
In the RS chain this sits under the eight-tick octave (T7) and $D=3$ (T8): the 3-cube is forced, its six faces pair generations, and chiral imbalance of the Hamiltonian cycle on those faces is the geometric origin of CP violation. Without an explicit free-axis map, the orientation test on each edge cannot be stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.