flip_ratio_21
plain-language theorem explainer
On the canonical 3-bit Gray-code 8-tick cycle, axis 0 flips twice as often as axis 1: the flip-count ratio is exactly 2. Flavor-mixing and CP-violation arguments in RS cite this 2:1 split together with the torsion gap Δτ₁₂ = 11 when fixing the Cabibbo angle. The proof is a one-shot native decision on the finite flip multiset.
Claim. Let $N(b)$ be the number of times bit $b\in\{0,1,2\}$ flips along the directed 8-tick Gray-code cycle on the 3-cube. Then $N(0)/N(1)=2$.
background
The module studies the canonical Gray-code walk on $Q_3$, the path $[0,1,3,2,6,7,5,4]$ whose successive bit flips are $[0,1,0,2,0,1,0,2]$. That directed 8-tick operator is the recognition cycle; face-pairs of the cube are identified with particle generations.
The J-cost obeys $J(x)=J(1/x)$, so particle↔antiparticle exchange is symmetric (CPT). Chirality arises instead from the walk: bit 0 flips four times while bits 1 and 2 each flip twice, breaking $S_3$ axis permutation. The flip-count function $N(b)$ simply tallies occurrences of each bit in the flip list.
Upstream, $N$ is the list-count of the flipped-bit sequence; sibling facts already record $N(0)=4$ and $N(1)=2$. The present ratio packages that 4:2 split for later angle formulae.
proof idea
Pure finite computation. After unfolding the definition of the per-bit flip count as the number of times each index appears in the fixed length-8 flip list, both numerator and denominator are concrete natural numbers, and native_decide checks the equality $N(0)/N(1)=2$ by evaluation. No algebraic lemmas beyond the definition are required.
why it matters
Module doc places this 4:2:2 pattern at the geometric origin of CP violation and flavor mixing: different generations couple to different flip counts over one eight-tick octave (T7). The declaration's own comment states that the 2:1 axis-0/axis-1 ratio, together with the torsion gap $\Delta\tau_{12}=11$, determines the Cabibbo angle.
It sits beside the flip-asymmetry vector $\Delta=(4/3,-2/3,-2/3)$, the chirality certificate, and the generation-coupling asymmetry results. J-symmetry (hence CPT) remains intact; only the directed Gray path breaks CP. No downstream Lean dependents are wired yet, so the ratio is presently a cited numeric input rather than a proof dependency.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.