tau
plain-language theorem explainer
Generation torsion assigns integers 0, 11, 17 to the three fermion generations. CKM and mass-ladder arguments cite it as the source of the structural Wolfenstein ratio Δτ₂₃/Δτ₁₂ = 6/11. The definition is a three-clause pattern match that freezes the global Anchor values on Fin 3.
Claim. Generation torsion is the map $\tau:\{0,1,2\}\to\mathbb{N}$ with $\tau(0)=0$, $\tau(1)=11$, and $\tau(2)=17$.
background
Module CKMExact derives the Wolfenstein $A$ parameter from $Q_3$ cube geometry: Gray-code flip counts $(4,2,2)$ on the three axes, generation torsion, and a face-flux (Berry) correction. The headline identity is $A_{\mathrm{corrected}}=9/11\approx 0.818$, within $0.6\sigma$ of PDG.
Generation torsion is the global, representation-independent integer assignment $\tau(0)=0$, $\tau(1)=E_{\mathrm{passive}}=11$, $\tau(2)=W=17$ already fixed in Masses.Anchor. Here it is re-indexed on Fin 3 so that successive differences $\Delta\tau_{12}=11$ and $\Delta\tau_{23}=6$ are immediate.
Those differences feed the structural ratio $A_{\mathrm{structural}}=\Delta\tau_{23}/\Delta\tau_{12}=6/11$, later multiplied by the face-flux factor $3/2$ to obtain $9/11$. The same $11$ appears in the "44 connection" ($4\times 11$) shared with $\alpha^{-1}$ and $\eta_B$.
proof idea
Pure definition by exhaustive match on Fin 3: generation 0 maps to 0, generation 1 to 11, generation 2 to 17. No lemmas or tactics; the clauses are definitional equalities that mirror Masses.Anchor.tau on $\mathbb{N}$.
why it matters
This packaging is step 2 of the five-line CKMExact derivation. Downstream equalities deltaTau12_eq, deltaTau23_eq, A_structural_eq, and finally A_corrected_exact read the values off this map to prove $A_{\mathrm{corrected}}=(6/11)\times(3/2)=9/11$ with zero sorry.
In the broader Recognition framework the triple ${0,11,17}$ is the generation-torsion half of $Q_3$ chirality. Together with Gray flip counts $[4,2,2]$ it produces the integer 44 that also governs the fine-structure band and the baryon-to-photon ratio $\eta_B\sim\varphi^{-44}$. The definition therefore anchors the CKM $A$ prediction to the same discrete geometry that forces the eight-tick octave and three spatial dimensions elsewhere in the chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.