vertexBit
plain-language theorem explainer
Extracts the k-th binary coordinate of a vertex of the 3-cube Q₃, labeled by Fin 8. Anyone building face incidence, edge orientation, or winding numbers on the eight-tick cycle cites this bit probe. The body is a one-line arithmetic definition: integer division by 2^k mod 2 equals one.
Claim. For a vertex index $v \in \{0,\ldots,7\}$ and axis $k \in \{0,1,2\}$, return whether the $k$-th binary digit of $v$ is $1$: $\bigl(\lfloor v / 2^k \rfloor \bmod 2\bigr) = 1$.
background
The module Face Winding Numbers on $Q_3$ equips the 3-cube with signed winding numbers of a Hamiltonian cycle around each face. Those windings are the geometric origin of CP violation in Recognition Science: each face pairs with a generation pair, and a nonzero winding distinguishes forward from backward boundary traversal.
Vertices of $Q_3$ are the eight points of ${0,1}^3$, coded as integers $0..7$. The three axes are the bit positions $k=0,1,2$. Faces are fixed by choosing one axis and one side bit (the coordinate held constant). Incidence and orientation tests therefore need a pure bit extractor on vertex labels.
Related bit maps appear elsewhere (e.g. Bool-to-Nat conversion on the periodic Freudenthal torus), but here the probe is specialized to Fin 8 and Fin 3 so that cycle edges, free axes, and face sides share one coordinate language.
proof idea
Pure definition, no proof obligations. The body reads the $k$-th bit of the natural number underlying $v$ by integer division by $2^{k}$ followed by reduction mod 2, then compares the residue to 1, yielding a Bool. No lemmas are applied.
why it matters
This bit probe is the coordinate primitive for the whole face-winding stack. Downstream, edge-on-face incidence checks that both endpoints carry the face's side bit on the face axis and that the edge does not flip that axis. Edge-face sign then uses the same probe to decide whether a boundary step moves "up" along the free axis, returning $+1$, $-1$, or $0$. Those signed contributions assemble into face winding and ultimately the nonzero total chiral charge.
Outside this module, the cycle operator's axis-flip count filters flipped bits against the vertex bit on axis $k$, tying generation-axis coupling strength to the same coordinates. In the broader RS chain this sits under the eight-tick octave (T7) and $D=3$ (T8): the cube $Q_3$ is the discrete geometry whose chiral face windings seed CP violation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.