axis_flip_asymmetry
plain-language theorem explainer
The eight-tick Gray-code cycle on the 3-cube flips coordinate axes unequally: axis 0 is flipped four times and axis 1 only twice. Anyone tracking how the Hamiltonian cycle breaks S₃ axis-permutation symmetry cites this count inequality. The proof is a one-line native decision over the finite list of flipped bits.
Claim. In the standard 8-step Gray-code Hamiltonian cycle on the 3-cube $Q_3$, if $b_i\in\{0,1,2\}$ is the coordinate axis flipped at step $i$, then $\#\{i:b_i=0\}\neq\#\{i:b_i=1\}$.
background
The module Face Winding Numbers on $Q_3$ supplies the geometric origin of CP violation in Recognition Science. The 3-cube carries an 8-tick Hamiltonian cycle (binary-reflected Gray code), matching the eight-tick octave forced at T7. Each step flips exactly one bit of the vertex label in ${0,1}^3$.
The map from step index to flipped axis records which coordinate changes at each of the eight edges. Doc-comment on that map lists the pattern explicitly (e.g. steps 0,2,4 flip bit 0). The six faces of $Q_3$ correspond to generation pairs; face windings measure signed boundary traversal by the cycle. Unequal axis usage is the combinatorial reason the cycle is not $S_3$-symmetric under coordinate permutation.
Module framing: a nonzero winding distinguishes forward from backward at a face, the geometric seed of CP violation.
proof idea
One-line computational proof via native_decide. Materialize the eight-element list of flipped axes from the explicit case table of the step-to-axis map, evaluate the two list-count queries by kernel computation, and check they differ. No algebraic lemmas or induction; the claim is a finite combinatorial fact about the Gray-code edge sequence (doc-comment: 4 flips of bit 0 versus 2 of bit 1).
why it matters
Records the 4:2:2 split of axis flips that breaks $S_3$ axis-permutation symmetry of the cycle. That broken symmetry is part of the geometric foundation for CP violation in this module: face windings on generation-pair faces can be chiral precisely because the cycle treats axes unequally.
Sits under the eight-tick octave (T7) and $D=3$ forcing (T8), since the Gray cycle lives on $Q_3$. The module's headline target is the total chiral charge (sum of face windings, proved nonzero). Even with no direct downstream edges listed yet, the count asymmetry is why the cycle cannot be axis-symmetric, so windings need not cancel under orientation reversal.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.