edge_dressed_prefers_axis0
plain-language theorem explainer
Over the eight-tick Gray-code cycle on the cube, bit 0 flips strictly more often than bits 1 and 2. That asymmetry marks axis 0 as the preferred mass-basis axis for the edge-dressed generation (generation 2), via maximal passive edge interaction per cycle. Anyone assigning mass eigenstate axes on Q₃ cites this comparison. The proof is a one-line term alias of the Gray-code flip-count theorem.
Claim. Writing $\mathrm{flip}(i)$ for the number of times coordinate $i\in\{0,1,2\}$ changes along the 8-tick Gray-code cycle on $Q_3$, one has $\mathrm{flip}(0)>\mathrm{flip}(1)$ and $\mathrm{flip}(0)>\mathrm{flip}(2)$. Hence axis 0 is the preferred axis for the edge-dressed generation.
background
The module builds the two orthonormal bases on generation space whose overlap is the CKM matrix: mass eigenstates from the CW filtration and torsion ladder, and weak eigenstates from the SU(2) even-sign-flip action on $Q_3$. Mass axes are read off which passive subcells each generation couples to.
bitFlipCount tallies, for each of the three cube axes, how many times that bit flips across the eight-tick Gray-code schedule (the T7 octave). Upstream, bit0_most_flipped records the concrete asymmetry: bit 0 flips most often, while bits 1 and 2 flip equally, breaking $S_3$ down to $S_2\times 1$.
The edge-dressed generation (generation 2) is the one whose CW coupling is dominated by passive edge interaction. More flips on an axis means more such edge contacts per cycle, so the preferred mass axis is the most-flipped bit.
proof idea
One-line term proof: the claim is definitionally the same conjunction as GrayCodeChirality.bit0_most_flipped, so the proof is just that theorem name. The upstream result itself is discharged by native_decide on the finite flip-count table for the 8-tick Gray path. No extra algebra is done here.
why it matters
This pins the mass-basis axis for the edge-dressed generation inside the RS account of CKM mixing. Module doc: mass axes come from CW-level coupling (passive subcells), weak axes from even sign flips; their mismatch forces mixing angles. Naming axis 0 as preferred for gen 2 is the first concrete mass-axis assignment step among the siblings (massBasisAxis, both_bases_label_axes, MixingAngleData).
Framework landmarks: the count runs over the T7 eight-tick octave on $Q_3$ (T8 forces $D=3$, so three bits). The Gray-code chirality asymmetry is what breaks full permutation symmetry of the three axes and gives a distinguished mass direction. No downstream theorems yet list this name, but the module's stated main results on axis mismatch and mixing data are the intended landing zone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.