berryCorrection
plain-language theorem explainer
The Berry correction is the ratio of Q₃ face fluxes on the generation-1–2 and 2–3 faces, equal to 3/2. Anyone deriving the Wolfenstein A parameter from Recognition Science cube geometry cites this factor. It is introduced by a direct definition: high-flux face over low-flux face from Gray-code flip counts.
Claim. The Berry correction is the real number equal to the ratio of face fluxes on the generation faces $1\to 2$ and $2\to 3$. Face flux between generations $i$ and $j$ is the sum of Gray-code flip counts on the two spanning axes (generation $k$ maps to axis $k-1$). Explicitly the value is $6/4 = 3/2$.
background
The CKMExact module derives the Wolfenstein $A$ parameter from first principles of the $Q_3$ cube. Axes carry Gray-code flip counts $(4,2,2)$ for axes $(0,1,2)$, with generation $1\mapsto$ axis $0$, $2\mapsto 1$, $3\mapsto 2$.
Face flux between generations $i$ and $j$ is the total flip count on the two spanning axes: the number of times per eight-tick cycle the recognition operator drives transitions on that face. The $1\to 2$ face (axes $0,1$) has flux $4+2=6$; the $2\to 3$ face (axes $1,2$) has flux $2+2=4$. The high-flux face includes the dominant axis $0$.
Mixing $V_{us}$ ($1\to 2$) sees the high-flux face; $V_{cb}$ ($2\to 3$) sees the low-flux face. Their flux ratio corrects the bare torsion prediction $A_{\mathrm{structural}}=\Delta\tau_{23}/\Delta\tau_{12}=6/11$.
proof idea
Pure definition: the real is the quotient of two face-flux values, with $\mathrm{Fin},3$ indices $\langle 0\rangle,\langle 1\rangle$ in the numerator and $\langle 1\rangle,\langle 2\rangle$ in the denominator. Face flux itself is the sum of the two axis flip counts. No tactic proof; the numerical identity $3/2$ is discharged later by simplification and norm_num.
why it matters
This factor is the geometric correction that turns structural torsion into the physical Wolfenstein $A$. Downstream, $A_{\mathrm{corrected}}=A_{\mathrm{structural}}\times$ (Berry correction) $=(6/11)\times(3/2)=9/11\approx 0.818$, within $0.6\sigma$ of PDG $0.826\pm 0.013$.
It is a field of the zero-sorry certificate CKMExactCert (berry factor and its square $9/4$). The square identity is noted as connecting to the colour factor $N_c=3$. Module-level, the same $Q_3$ chirality $[4,2,2]\times$ generation torsion that produces this $3/2$ also governs the "44 connection": $44=4\times 11$ appears in $\alpha^{-1}$, $\eta_B\approx\varphi^{-44}$, and $A_{\mathrm{corrected}}=9/11$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.