edgeOnFace
plain-language theorem explainer
An 8-tick Gray-cycle edge lies on a face of the 3-cube exactly when it does not flip the face's fixed axis and both endpoints carry that axis bit equal to the face side. Anyone building face windings or edge-face incidence counts cites this Boolean predicate. The body is a three-conjunct Boolean combination of bit tests on the directed cycle edge.
Claim. For a step $k \in \{0,\ldots,7\}$ of the Hamiltonian cycle on $Q_3$ and a face $f$ fixed by axis $a \in \{0,1,2\}$ at side $s \in \{0,1\}$, the edge at step $k$ is incident to $f$ if and only if the bit flipped by that edge is not $a$, and both endpoints have coordinate $a$ equal to $s$.
background
The module FaceWinding equips the 3-cube $Q_3$ with signed winding numbers of a fixed 8-tick Hamiltonian cycle around each face. Faces of $Q_3$ are pairs (axis, side): the coordinate that is held fixed and the Boolean value of that coordinate. The six faces match the generation-pair geometry used elsewhere in the foundation stack.
The cycle is the standard Gray-code Hamiltonian path on the eight vertices of $Q_3$ (period $2^3$, the eight-tick octave of T7). Each step determines a directed edge by flipping exactly one bit. Incidence of that edge to a face is the elementary combinatorial fact needed before one can assign orientation signs or sum boundary contributions.
Spatial dimension is the forced $D=3$ of the Recognition chain, so the ambient graph is exactly the 3-cube rather than a higher hypercube.
proof idea
Definitional, not a proof. Unpack the directed edge at the given cycle step, then return the Boolean conjunction of three tests: the flipped bit differs from the face axis (so the edge is free on the face plane), the source vertex has the face-axis bit equal to the face side, and the destination vertex has the same bit equal to the face side. No lemmas are invoked; the body is pure bit arithmetic on the cycle data.
why it matters
Incidence is the gate for the whole winding calculus. Downstream, each_edge_on_two_faces filters the six faces by this predicate and proves every cycle edge meets exactly two faces, the discrete Stokes bookkeeping identity on $Q_3$. The signed contribution edgeFaceSign returns 0 precisely when incidence fails, and otherwise $\pm 1$ according to boundary orientation.
Those signs feed faceWinding and ultimately totalChiralCharge, the nonzero total that the module presents as the geometric origin of CP violation in Recognition Science: nonzero winding means the eight-tick cycle distinguishes forward from backward on generation-pair faces. Without a crisp edge-on-face test, the signed orientation section cannot start.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.