generation_coupling_asymmetry
plain-language theorem explainer
Generation 1 (axis 0) is driven twice as often per 8-tick Gray cycle as generations 2 and 3: flip counts satisfy n₀ = 2 n₁ and n₀ = 2 n₂. Flavor-mixing and CKM analyses cite this as the kinematic source of mass/weak eigenstate misalignment. The proof is a two-goal native decision on the fixed Gray flip schedule.
Claim. Let $n_g$ be the number of bit flips on the axis associated to generation $g\in\{0,1,2\}$ during one canonical 3-bit Gray cycle on the cube. Then $n_0 = 2 n_1$ and $n_0 = 2 n_2$.
background
The module studies the canonical 3-bit Gray walk on $Q_3$, the path $[0,1,3,2,6,7,5,4]$ with flip pattern $[0,1,0,2,0,1,0,2]$. That schedule flips bit 0 four times and bits 1 and 2 twice each, breaking $S_3$ axis symmetry. Face-pairs of the cube are identified with particle generations, so each generation inherits the flip count of its axis.
generationFlipCount is exactly the per-axis flip count: generation $g$ is "actively driven" once per flip of its axis. The J-cost remains particle/antiparticle symmetric ($J(x)=J(1/x)$), so CPT is preserved while the directed walk supplies chirality. The local claim isolates the 2:1 coupling ratios among the three generations that later feed Cabibbo-scale mixing.
proof idea
Split the conjunction with constructor, then discharge each equality by native_decide. Both sides are closed natural-number terms once generationFlipCount is unfolded to the fixed Gray flip counts (4 on axis 0, 2 on axes 1 and 2), so kernel computation finishes the proof with no further lemmas.
why it matters
This is main result (5) of GrayCodeChirality: different generations see different flip counts, the kinematic origin of flavor mixing (CKM/PMNS). Downstream, large_cabibbo_from_coupling_ratio quotes the first conjunct as the reason the 1–2 mixing angle is large relative to 2–3 mixing. The same conjunct is packaged into chiralityCert.asymmetry, the master certificate that also records cycle chirality, CPT preservation, and the raw [4,2,2] flip vector.
In the RS chain this sits on the eight-tick octave (T7) and the directed recognition operator on $Q_3$: the 4:2:2 split is the concrete breaking of axis permutation symmetry that forces mass and weak eigenstates out of alignment, while J-symmetry keeps CPT intact. Combined with the torsion gap $\Delta\tau_{12}=11$ it is the stated input to the Cabibbo angle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.