gap_nearly_closed
plain-language theorem explainer
The Berry-corrected Wolfenstein A sits within 0.008 of the PDG central value 0.826, while the bare structural ratio 6/11 leaves a gap larger than 0.27. Anyone citing the Q₃ face-flux CKM derivation uses this to quantify that the correction closes ~97% of the leading-order discrepancy. The proof is a two-conjunct term: rewrite the structural equality and norm_num, then apply the already-proved PDG distance bound.
Claim. With $A_{\mathrm{struct}}=\Delta\tau_{23}/\Delta\tau_{12}$ the bare generation-torsion ratio and $A_{\mathrm{corr}}=A_{\mathrm{struct}}\times$ (Berry face-flux factor), one has $0.826-A_{\mathrm{struct}}>0.27$ and $|A_{\mathrm{corr}}-0.826|<0.008$.
background
In the CKMExact module the Wolfenstein parameter $A$ is derived from $Q_3$ cube geometry rather than fit. Generation torsion supplies $\Delta\tau_{12}=11$ and $\Delta\tau_{23}=6$, so the structural ratio is $A_{\mathrm{struct}}=6/11$. The Gray-code flip counts on the three axes are $(4,2,2)$; the face-flux ratio between the $1$–$2$ and $2$–$3$ sectors is $6/4=3/2$. Multiplying gives the corrected value $A_{\mathrm{corr}}=(6/11)\times(3/2)=9/11\approx 0.818$.
PDG quotes a central value $0.826\pm 0.013$. The bare $6/11\approx 0.545$ sits roughly $0.28$ below that centre; the Berry factor is meant to close almost all of that gap. Upstream, A_structural_eq pins the ratio exactly to $6/11$, and A_distance_from_pdg already proves $|9/11-0.826|<0.008$. The module claims zero sorry and zero axioms for the whole chain.
proof idea
Term-mode pair of conjuncts. Left conjunct: rewrite with A_structural_eq (so $A_{\mathrm{struct}}=6/11$) and finish by norm_num, establishing $0.826-6/11>0.27$. Right conjunct: invoke the already-proved theorem A_distance_from_pdg, which rewrites $A_{\mathrm{corr}}$ to $9/11$ via A_corrected_exact and checks the absolute-value bound by norm_num. No new arithmetic is introduced here; the declaration only packages the residual-gap claim with the PDG-distance claim.
why it matters
This is the quantitative “gap closed” statement for the CKM $A$ derivation. Downstream it is recorded inside ckmExactCert, the certificate bundle that assembles structural equality, exact corrected value $9/11$, Berry factor, and the $1\sigma$ PDG membership. Together with the module’s 44-connection (the same $4\times 11$ chirality appearing in $\alpha^{-1}$, $\eta_B\sim\varphi^{-44}$, and $A_{\mathrm{corr}}$), it ties the CKM sector to the eight-tick $Q_3$ geometry (T7) and the generation-torsion ladder. A referee reading the RS Standard-Model claims cites this to see that the Berry face-flux correction is not cosmetic: it removes about 97% of the $0.28$ leading-order discrepancy and leaves a residual well inside the PDG error bar.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.