cycle_visits_all_vertices
plain-language theorem explainer
The canonical 3-bit Gray-code path on Q₃ hits every cube vertex exactly once. Anyone arguing that total 8-tick interaction is balanced while per-axis flip counts are not needs this bijectivity. The proof is a one-line alias of the existing Gray-cycle bijectivity theorem in Patterns.GrayCycle.
Claim. The period-$8$ Gray-code path $\gamma:\mathrm{Fin}\,8\to\{\text{$3$-bit patterns}\}$ is bijective: every vertex of the $3$-cube is visited exactly once.
background
This module studies the directed 3-bit Gray walk on the cube graph $Q_3$ as the geometric source of CP violation in Recognition Science. The walk $[0,1,3,2,6,7,5,4]$ is the standard reflected Gray cycle of period $8$ (the eight-tick octave). Vertices are $3$-bit patterns; successive steps flip exactly one bit.
The J-cost is symmetric, $J(x)=J(1/x)$, which the module identifies with CPT. Chirality arises instead from the directed path: bit $0$ flips four times while bits $1$ and $2$ flip twice each, breaking $S_3$ axis symmetry. Face-pairs are tied to particle generations, so unequal flip counts become generation-dependent coupling.
Upstream, grayCycle3Path is the concrete map $\mathrm{Fin},8\to\mathrm{Pattern},3$, and grayCycle3_bijective already proves it is bijective by finite cardinality ($|\mathrm{Fin},8|=8=2^3$).
proof idea
One-line term wrapper: the claim is definitionally the existing theorem that the Gray-cycle path is bijective. No new argument; it re-exports that result under the chirality module's naming so later certificates can cite a local name.
why it matters
Bijectivity is the "balanced total" half of the module's central contrast: the walk covers every vertex once, so the global 8-tick budget is fair, yet the flip vector $(4,2,2)$ is axis-asymmetric. That split feeds flipAsymmetryNonzero, cycle_is_chiral, and the master chirality certificate. In the forcing chain this sits at the eight-tick octave (T7) on $D=3$ (T8): the directed Gray path is how the recognition operator traverses $Q_3$. Without surjectivity one could not claim every generation's face-pair is visited; without injectivity double-counting would spoil the $4:2:2$ ledger. No downstream edges are recorded yet; the declaration is infrastructure for the chirality bundle rather than a leaf used elsewhere.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.