A_structural_eq
plain-language theorem explainer
The structural Wolfenstein A equals exactly 6/11, the ratio of generation torsions Δτ₂₃/Δτ₁₂ from the values {0, 11, 17}. Anyone deriving CKM parameters from Q₃ geometry cites this as the uncorrected leading factor. The proof is a one-line simp-and-norm_num wrapper unfolding the three definitions.
Claim. The structural Wolfenstein parameter equals the generation-torsion ratio exactly: $A_{\mathrm{structural}} = \Delta\tau_{23}/\Delta\tau_{12} = 6/11$, where $\tau(0)=0$, $\tau(1)=11$, $\tau(2)=17$.
background
Module CKMExact derives the Wolfenstein $A$ parameter from $Q_3$ face-flux geometry and generation torsion, with zero sorry and zero axioms. The headline claim is $A_{\mathrm{corrected}}=9/11\approx 0.818$, within $0.6\sigma$ of the PDG value $0.826\pm 0.013$.
Generation torsion is the global, representation-independent assignment $\tau(0)=0$, $\tau(1)=E_{\mathrm{passive}}=11$, $\tau(2)=W=17$. The successive gaps are $\Delta\tau_{12}=\tau(1)-\tau(0)=11$ and $\Delta\tau_{23}=\tau(2)-\tau(1)=6$. The structural (uncorrected) $A$ is defined as their real ratio $A_{\mathrm{structural}}:=\Delta\tau_{23}/\Delta\tau_{12}$.
This sits between the Gray-code flip counts on the three cube axes and the later Berry face-flux correction that multiplies by $3/2$ to reach $9/11$.
proof idea
One-line wrapper. Unfold $A_{\mathrm{structural}}$, $\Delta\tau_{23}$, $\Delta\tau_{12}$, and the piecewise $\tau$ definition via simp only, then close by norm_num: the integers evaluate to $6/11$.
why it matters
Step 3 of the five-line CKMExact derivation. Downstream, A_corrected_exact multiplies this by the Berry factor $3/2$ to obtain the main theorem $A_{\mathrm{corrected}}=9/11$. Positivity (A_structural_pos), the gap-closure estimate (gap_nearly_closed), the forced factorization nine_elevenths_forced, and the certification bundle ckmExactCert all rewrite through this equality.
The factor $11$ is the same $E_{\mathrm{passive}}$ that appears in the 44-connection: $44=4\times 11$ links $\alpha^{-1}$, $\eta_B\approx\varphi^{-44}$, and CKM $A$ under shared $Q_3$ chirality. The torsion values themselves sit on the $D=3$ forcing chain (T8) via the eight-tick octave geometry that produces the Gray code $[4,2,2]$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.