A_corrected
plain-language theorem explainer
Defines the Berry-corrected Wolfenstein A parameter as the product of the bare generation-torsion ratio and the face-flux correction. Anyone matching CKM A to PDG cites this quantity; the main theorem then proves it equals exactly 9/11. The definition is a one-line product of two already-constructed real scalars.
Claim. The Berry-corrected Wolfenstein parameter is $A_{\mathrm{corr}} := A_{\mathrm{struct}} \cdot B$, where $A_{\mathrm{struct}} = \Delta\tau_{23}/\Delta\tau_{12}$ is the bare torsion ratio and $B = F_{12}/F_{23}$ is the ratio of $Q_3$ face fluxes for the $1\to 2$ and $2\to 3$ mixings. Numerically this is $(6/11)\times(3/2)=9/11$.
background
Module CKMExact derives the Wolfenstein $A$ parameter from $Q_3$ geometry (the 3-cube Gray-code skeleton forced by eight-tick recognition). The Gray code on the cube has flip counts $[4,2,2]$ on the three axes; generation torsion supplies $\Delta\tau_{12}=11$ and $\Delta\tau_{23}=6$.
The structural (bare) prediction is the torsion ratio $A_{\mathrm{struct}}=\Delta\tau_{23}/\Delta\tau_{12}=6/11$. That under-shoots PDG $A\approx 0.826$ by about $0.28$. The missing factor is a Berry-type face-flux correction: the $1\to 2$ mixing sees the high-flux face and the $2\to 3$ mixing the low-flux face, so $B=F_{12}/F_{23}=6/4=3/2$.
This definition multiplies those two scalars. The same $Q_3$ chirality (flip count $4$ times torsion $11$) appears in the fine-structure and baryon-asymmetry formulae, giving the module's "44 connection."
proof idea
Pure definitional abbreviation: $A_{\mathrm{corr}}$ is the product of the two upstream defs A_structural and berryCorrection. No tactics. Downstream exactness (A_corrected_exact) rewrites with A_structural_eq and berry_correction_eq, then closes by ring to $9/11$.
why it matters
Central object of CKMExact: the main theorem proves $A_{\mathrm{corr}}=9/11\approx 0.818$, inside the PDG $1\sigma$ band $0.826\pm 0.013$ (about $0.6\sigma$). Downstream lemmas establish positivity, the tight interval $(0.818,0.819)$, distance to PDG central value $<0.008$, and the colour rewrite $A_{\mathrm{corr}}=N_c^2/\Delta\tau_{12}$ with $N_c=3=\dim Q_3$.
It feeds the gauge/Standard-Model bridge certificate in the unified forcing chain (after T8 forces $D=3$), routing cube geometry into CKM phenomenology. The factor $9/11$ is the CKM face of the same $[4,2,2]\times$ torsion structure that produces $\alpha^{-1}$ and $\eta_B\sim\varphi^{-44}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.