flipWeight_values
plain-language theorem explainer
On the Q₃ cube, the preferred weak axis (axis 0) carries flip weight 1/2 and the other two axes each carry 1/4. Anyone building CKM amplitudes from Gray-code chirality cites this numerical split. The proof unfolds the weight definition and substitutes the bit-flip counts 4, 2, 2.
Claim. The flip weights of the three cube axes satisfy $w(0)=1/2$, $w(1)=1/4$, and $w(2)=1/4$, where each weight is the Gray-code bit-flip count of that axis normalized by the eight edges of $Q_3$.
background
This module derives the CKM matrix from Q₃ geometry, generation torsion {0, 11, 17}, and Gray-code chirality. Weak eigenstates are tied to the three even-sign-flip SU(2) generators (complements of axes 0, 1, 2). The flip weight of an axis is the fraction of the eight cube edges on which that bit flips in the Gray-code Hamiltonian cycle.
Upstream, bitFlipCount records how often each coordinate flips along the cycle. The Gray-code chirality theorems give the fixed pattern [4, 2, 2]: bit 0 flips four times, bits 1 and 2 flip twice each. Those counts are the only numerical input here.
The local CKM amplitude ansatz (stated just below this lemma) is $|V_{ij}|^2 \propto w_i ,\varphi^{-2|\Delta\tau_{ij}|}$, so the three weights must be pinned before any mixing-angle estimate.
proof idea
Term-mode proof by unfolding. Simplify with the definition of flip weight (bit-flip count over 8). Insert the three upstream equalities bit0_flips_four ($=4$), bit1_flips_two ($=2$), and bit2_flips_two ($=2$). Close with norm_num to obtain $4/8=1/2$ and $2/8=1/4$.
why it matters
Fixes the axis weights that enter every structural CKM amplitude in this module: $|V_{ij}|^2 \propto w_i \times \varphi^{-2|\Delta\tau_{ij}|}$. Axis 0 is preferred (weight 1/2), matching the Gray-code chirality [4,2,2] forced by the eight-tick octave (T7) on Q₃. Diagonal elements then sit near unity up to unitarity normalization; off-diagonal entries inherit both the weight ratio and the torsion-gap φ-suppression from the mass ladder.
No downstream theorem yet records a use edge, but the Part-4 amplitude definitions immediately below are written to consume exactly these three values. Without the 1/2 : 1/4 : 1/4 split the Cabibbo-scale hierarchy cannot be read off the cube.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.