flipWeight_sum
plain-language theorem explainer
The three axis flip-weights on the Q₃ Gray-code cycle sum to unity. Anyone building CKM mixing angles from cube geometry needs this normalization before weighting generation overlaps. The proof unfolds the weight definition, inserts the Gray-code flip counts 4, 2 and 2, and finishes by arithmetic.
Claim. Let $w_b$ be the flip weight of coordinate axis $b\in\{0,1,2\}$ on the eight-tick Gray-code cycle (the fraction of ticks at which bit $b$ flips). Then $w_0+w_1+w_2=1$.
background
This module derives the CKM quark-mixing matrix from Q₃ cube geometry, generation torsion ${0,11,17}$, and Gray-code chirality. Mixing angles take the schematic form $\sin^2\theta_{ij}\propto(\text{flip-count ratio})\times\varphi^{-|\Delta\tau_{ij}|}$, so the three axis weights must be a probability distribution on the cube axes.
The eight-tick Gray-code walk on the 3-cube flips one bit per tick. The count bitFlipCount records how often each bit flips: bit 0 flips four times, bits 1 and 2 flip twice each (the chirality pattern $[4,2,2]$). Flip weight is that count normalized by the cycle length 8, so the preferred axis carries weight $1/2$ and the other two carry $1/4$ each.
Upstream lemmas bit0_flips_four, bit1_flips_two, and bit2_flips_two fix those raw counts by direct evaluation on the cycle list. The present statement only asserts that the three normalized weights sum to one.
proof idea
Term-mode proof by unfolding. Expand the three flip weights to their definitions in terms of bitFlipCount. Replace the three counts by the upstream equalities bit0_flips_four ($=4$), bit1_flips_two ($=2$), and bit2_flips_two ($=2$). The resulting rational identity $4/8+2/8+2/8=1$ is discharged by norm_num.
why it matters
In the CKM-from-cube derivation the weak eigenstates are labeled by even-sign-flip generators complementary to the three cube axes. Flip weights supply the combinatorial prefactor in $\sin^2\theta_{ij}$, so they must form a partition of unity; otherwise the overlap amplitudes would not be consistently normalized across generations.
The identity locks in the Gray-code chirality $[4,2,2]$ forced by the eight-tick octave (forcing-chain T7). Axis 0 is preferred (weight $1/2$), matching the module's later claim that the preferred axis carries half the flip mass. No downstream theorem currently cites this lemma in the graph, but sibling results (flipWeight_values, the suppression exponents, and the torsion-gap hierarchy) sit on the same normalization step.
It is a small arithmetic gate, not a deep structural theorem, yet without it the CKM angle formulae would float by an overall scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.