generation_axis_coupling
plain-language theorem explainer
On the 8-tick Gray cycle of the 3-cube, coordinate axis 0 flips four times per period while axes 1 and 2 each flip twice. Anyone tying generation labels to cube axes, or arguing for a kinematic 2:1 Cabibbo bias from the cycle operator, cites this count. The proof is a one-line projection of the flip-count triple already stored in the chirality certificate.
Claim. During one full 8-tick Gray-code cycle on the 3-cube $Q_3$, bit $0$ is flipped exactly $4$ times, and bits $1$ and $2$ are each flipped exactly $2$ times.
background
The CycleOperator module builds the unitary cycle operator on $\mathbb{C}^8$ induced by the 8-tick Gray path on the 3-cube $Q_3$. The eight vertices are the computational basis; each tick flips exactly one coordinate, and the resulting permutation matrix has period 8 with DFT-8 eigenmodes. Module doc: this algebraic object is "from which the CKM matrix emerges," with per-tick phases encoding generation structure and mixing angles.
The flip-count function records, for each bit $b \in {0,1,2}$, how many of the eight steps flip that bit. In the local convention, generation $g$ is identified with axis $g$, so the generation-axis coupling strength is taken proportional to that count: generation $g$ sees that many transitions per cycle.
Upstream, GrayCodeChirality packages a chirality certificate whose flip-count field is already the certified triple $(4,2,2)$, together with chirality of the cycle, CPT preservation, and bijectivity of the Gray path.
proof idea
One-line term proof: extract the flip-count field of the chirality certificate. That field is the packaged triple of lemmas establishing bit 0 flips four times and bits 1 and 2 each flip twice. No new enumeration of the Gray path is performed here.
why it matters
This names the generation-axis coupling that the cycle-operator story needs for CKM kinematics. The inline note states the qualitative prediction: the 2:1 ratio (axis 0 driven twice as often as axes 1 and 2) is the kinematic origin of a large 1-2 mixing (Cabibbo) and a smaller 2-3 mixing. That sits on the T7 eight-tick octave landmark and on the module claim that eigenstate phases of the period-8 cycle operator determine mixing angles.
No Lean dependents are recorded yet; the declaration is a clean export of certified flip counts for later generation-coupling and CKM arguments rather than a step inside a larger proved chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.