flipWeight
plain-language theorem explainer
Normalized flip-count weights on the three cube axes: each axis weight is its Gray-code flip total divided by eight. CKM-from-cube derivations cite this to turn the chirality pattern (4,2,2) into probability weights (1/2,1/4,1/4). The body is a one-line cast-and-scale of the bit-flip count over the eight-tick cycle.
Claim. For each axis $k \in \{0,1,2\}$, the flip weight is $w_k = f_k/8$, where $f_k$ is the number of times bit $k$ flips during one eight-tick Gray-code cycle on the $Q_3$ cube.
background
The module builds the CKM quark-mixing matrix from $Q_3$ cube geometry, generation torsion ${0,11,17}$, and Gray-code chirality. Mass eigenstates sit on torsion levels; weak eigenstates sit on even-sign-flip $SU(2)$ generators labeled by complement axes. Mixing angles take the schematic form $\sin^2\theta_{ij} \propto$ (flip-count ratio) $\times \varphi^{-|\Delta\tau_{ij}|}$.
Upstream, the Gray-code chirality layer counts how often each coordinate bit flips across the closed eight-tick walk on the cube. That count is the natural integer weight of each axis in the weak-basis structure. The eight-tick period is the Recognition octave (forcing chain T7).
This definition only normalizes those integer counts to real weights that sum to one, so they can enter the CKM overlap formula as dimensionless factors.
proof idea
Definitional, not a proof. Cast the natural-number bit-flip count of axis $k$ to a real, then divide by $8$ (the length of the Gray-code cycle). No lemmas are applied at the definition site; downstream theorems insert the concrete counts $f_0=4$, $f_1=2$, $f_2=2$.
why it matters
Supplies the axis weights that feed the two immediate corollaries: the three weights sum to $1$, and they evaluate to $1/2$, $1/4$, $1/4$ (preferred axis twice as heavy as the others). Those facts pin the flip-count ratio in the CKM mixing-angle ansatz of the module.
In the broader framework this is the bridge from Gray-code chirality on the eight-tick octave to the weak-basis side of $V_{ij}=\langle\mathrm{weak}_i|\mathrm{mass}_j\rangle$. Mass-side suppression still comes from torsion gaps and the $J$-cost ladder; this object only handles the geometric weight of each complement axis. Without the normalization, the flip totals cannot sit next to $\varphi^{-|\Delta\tau|}$ as dimensionless factors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.