berry_correction_eq
plain-language theorem explainer
The Berry correction that multiplies the bare CKM torsion ratio equals exactly 3/2. Anyone deriving the Wolfenstein A parameter from Q₃ Gray-code geometry cites this identity. The proof unfolds the definitions of face flux and flip counts and evaluates the resulting rational by norm_num.
Claim. The Berry correction factor equals $3/2$: the ratio of $Q_3$ face fluxes for the generation-$1\to 2$ face to the generation-$2\to 3$ face is exactly $3/2$.
background
In the CKMExact module the Wolfenstein $A$ parameter is obtained from $Q_3$ geometry rather than fit to data. The cube carries a Gray-code edge labelling whose per-axis flip counts are $(4,2,2)$ on axes $(0,1,2)$. Generations map to those axes (gen $1\mapsto$ axis $0$, gen $2\mapsto$ axis $1$, gen $3\mapsto$ axis $2$).
Face flux on the face spanning generations $i$ and $j$ is the sum of flip counts on the two spanning axes: the number of times per eight-tick cycle the recognition operator drives transitions along that face. The $1\to 2$ face therefore has flux $4+2=6$; the $2\to 3$ face has flux $2+2=4$.
The Berry correction is defined as the ratio of those two fluxes. It corrects the bare torsion prediction $A_{\mathrm{structural}}=\Delta\tau_{23}/\Delta\tau_{12}=6/11$ because $V_{us}$ sees the high-flux face while $V_{cb}$ sees the low-flux face.
proof idea
One-line wrapper. Unfold berryCorrection to the ratio of face fluxes on Fin-3 indices $\langle 0,1\rangle$ and $\langle 1,2\rangle$, unfold each faceFlux to a sum of flipCount values, reduce the piecewise definition of flipCount to the concrete naturals $4,2,2$, and finish by norm_num on the rational $6/4$.
why it matters
This is step 4 of the five-line derivation that yields $A_{\mathrm{corrected}}=9/11$. The main theorem A_corrected_exact multiplies the structural ratio $6/11$ by this $3/2$ factor and obtains $9/11\approx 0.818$, inside $0.6\sigma$ of the PDG value $0.826\pm 0.013$.
Downstream, berry_correction_pos and berry_sq_eq record positivity and the identity $(3/2)^2=9/4$ (linked in the module to the colour factor $N_c=3$). The certification bundle ckmExactCert packages the equality as berry_factor. The narrative lemmas three_halves_from_asymmetry and nine_elevenths_forced restate that every factor traces to $D=3$ via the forcing chain (T8) and the eight-tick Gray code (T7).
The same $[4,2,2]$ chirality appears in the "44 connection": $4\times 11$ governs $\alpha^{-1}$, $\eta_B\approx\varphi^{-44}$, and this CKM correction, all from one $Q_3$ geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.