berry_sq_eq
plain-language theorem explainer
The square of the Berry face-flux correction equals 9/4. Anyone deriving the Wolfenstein A parameter from Q₃ geometry cites this to link the flux ratio 3/2 to the colour factor N_c = 3. The proof is a one-line rewrite of the already-proved correction identity, followed by numerical normalisation.
Claim. Let $B$ be the Berry face-flux correction, the ratio of face fluxes for the generation transitions $1\to 2$ and $2\to 3$. Then $B^2 = 9/4$.
background
The module derives the Wolfenstein $A$ parameter of the CKM matrix from the geometry of the cube graph $Q_3$. Gray-code flip counts on the three axes are $(4,2,2)$; generation torsion differences are $\Delta\tau_{12}=11$ and $\Delta\tau_{23}=6$. The bare structural ratio is therefore $A_{\mathrm{structural}}=\Delta\tau_{23}/\Delta\tau_{12}=6/11$.
The Berry correction is the ratio of face fluxes seen by the mixing amplitudes $V_{us}$ ($1\to 2$) and $V_{cb}$ ($2\to 3$). By definition it equals $\mathrm{faceFlux}(1,2)/\mathrm{faceFlux}(2,3)$. The upstream identity already proves this ratio is exactly $3/2$ (from flip counts $6$ and $4$). Squaring that factor is the present claim; the doc-comment flags the link $(3/2)^2=9/4$ to the colour factor $N_c=3$.
proof idea
One-line term-mode wrapper. Rewrite the goal by the upstream equality that the Berry correction equals $3/2$, then discharge $ (3/2)^2 = 9/4 $ by norm_num. No further geometric reasoning is needed at this step.
why it matters
This identity is packaged into the certificate record that assembles every exact CKM claim in the module, and it appears as the middle conjunct of the theorem that $44$ governs three constants: the same integer $4\times 11$ that enters $\alpha^{-1}$ and $\eta_B$ also organises $A_{\mathrm{corrected}}=9/11$ once the squared Berry factor $9/4$ is in place. The module result is $A_{\mathrm{corrected}}=(6/11)\times(3/2)=9/11\approx 0.818$, within $0.6\sigma$ of the PDG value $0.826\pm 0.013$. The colour-factor reading of $9/4$ ties the flux correction to $N_c=3$, consistent with the eight-tick $Q_3$ geometry (T7) that forces three spatial axes (T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.