axisFlipCount
plain-language theorem explainer
Counts how many steps of the 8-tick Gray cycle flip a chosen cube axis k, relative to a vertex v of Q₃. Foundation work on generation–axis coupling and the cycle operator cites it as the discrete strength of that coupling. Defined by filtering the flipped-bit schedule with a predicate on the vertex’s k-th bit.
Claim. For a cube vertex $v \in \{0,\ldots,7\}$ and axis $k \in \{0,1,2\}$, the axis flip count is the number of ticks $t$ in the length-8 Gray schedule at which the flipped bit equals $k$, with the selection predicate written in terms of whether the $k$-th bit of $v$ is set.
background
The module builds the cycle operator $\hat R$ on $\mathbb{C}^8$: the unitary permutation induced by the directed 8-tick Gray code on the vertices of the 3-cube $Q_3$. Vertices form the standard basis; each tick flips exactly one coordinate bit, so the dynamics are a Hamiltonian path that closes after eight steps (the eight-tick octave of the forcing chain).
flippedBit assigns to each tick $t \in \mathrm{Fin},8$ the axis in $\mathrm{Fin},3$ that changes on that step. vertexBit v k reads the $k$-th binary digit of the vertex index $v$. The sibling bitFlipCount k simply counts occurrences of axis $k$ in the flipped-bit list (bit 0 flips four times, etc.).
Axis flip count is the vertex-indexed variant of that tally: same Gray schedule, with the predicate phrased through the bit value of $v$ on axis $k$. In the module narrative this is the discrete coupling of a generation axis to the cycle.
proof idea
Pure definition, no proof obligations. Materialize the eight-step schedule as List.ofFn flippedBit, then countP with the Boolean predicate that holds when the schedule bit equals $k$ and is written as a disjunction on vertexBit v k = true versus false. Both arms require the flipped bit to be $k$, so the count equals the ordinary bit-flip multiplicity of axis $k$.
why it matters
Sits in the Foundation cycle-operator stack that turns the Gray path on $Q_3$ into a unitary on $\mathbb{C}^8$ whose period-8 spectrum and DFT-8 eigenmodes feed generation structure and, downstream, CKM mixing. The inline remark states that generation–axis coupling strength is proportional to this flip count: generation $g$ (axis $g$) sees bitFlipCount g transitions per cycle.
Framework landmarks: T7 (eight-tick octave, period $2^3$) supplies the length-8 schedule; T8 ($D=3$) supplies the three axes. No used_by edges are recorded yet, so the declaration is presently a local measuring stick inside CycleOperator rather than a cited lemma in a closed theorem. It prepares quantitative generation–axis weights once the permutation matrix and its eigenphases are assembled.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.