deltaTau12
plain-language theorem explainer
Defines the first generation torsion gap Δτ₁₂ as τ(1) − τ(0) on the three-generation ladder. Anyone deriving Wolfenstein A from Q₃ geometry cites this as the denominator of A_structural. The body is a pure difference of the local generation-torsion table entries.
Claim. Let $\tau:\{0,1,2\}\to\mathbb{N}$ be generation torsion with $\tau(0)=0$, $\tau(1)=11$, $\tau(2)=17$. Define the first torsion gap by $\Delta\tau_{12}:=\tau(1)-\tau(0)\in\mathbb{N}$.
background
The module derives the Wolfenstein CKM parameter $A$ from the cube $Q_3$ and its Gray-code chirality, with zero sorry and zero axioms. Generation torsion is the global, representation-independent assignment $\tau(0)=0$, $\tau(1)=E_{\mathrm{passive}}=11$, $\tau(2)=W=17$ (CW filtration gaps between the three particle generations).
Locally the same table is re-exported as a map on $\mathrm{Fin},3$. The Gray-code flip counts on the three axes are $(4,2,2)$; together with the torsion gaps they produce the structural ratio $A_{\mathrm{structural}}=\Delta\tau_{23}/\Delta\tau_{12}$ and the face-flux correction that yields $A_{\mathrm{corrected}}=9/11$.
Upstream, the same integers appear as Anchor torsion and (under a different name) as the tau-lepton species label; only the $\mathrm{Fin},3$ table is used here.
proof idea
Definitional, not a proof. The right-hand side evaluates the local torsion map at generations $1$ and $0$ (each index discharged by norm_num) and subtracts. Unfolding immediately gives $11-0$, which the companion lemma deltaTau12_eq records as rfl.
why it matters
This gap is the integer $11$ that sits in every CKMExact identity: $A_{\mathrm{structural}}=6/11$, $A_{\mathrm{corrected}}=9/11=(3)^2/\Delta\tau_{12}$, and the certificate fields of CKMExactCert. Downstream lemmas eleven_from_torsion and eleven_is_torsion_gap name it explicitly as the CW torsion gap between generations 1 and 2.
It also seeds the “44 connection”: $44=4\times 11=\mathrm{flipCount}(\mathrm{axis}0)\times\Delta\tau{12}$ reappears in the fine-structure formula $\alpha^{-1}=44\pi\cdot\exp(-w_8\ln\varphi/44\pi)$ and in $\eta_B\approx\varphi^{-44}$. Thus the same $Q_3$ chirality that fixes CKM $A$ also ties the octave (T7) and the $\varphi$-ladder constants to a single integer gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.