ckmExactCert
plain-language theorem explainer
Bundles the fully proved Wolfenstein-A package from Q₃ geometry into one certificate: structural A = 6/11, Berry-corrected A = 9/11, PDG 1σ membership, residual distance < 0.008, the 44-link, and Gray-code flip symmetries. Anyone citing the RS CKM exact result or the shared 44 chirality with α and η_B points here. Construction is a structure literal wiring already-proved field theorems.
Claim. There is a certificate whose fields assert: structural Wolfenstein $A$ equals $6/11$; Berry-corrected $A$ equals $9/11$; the Berry factor equals $3/2$ (and its square $9/4$); $A_{\mathrm{corr}}$ lies in the PDG $1\sigma$ interval $(0.813,0.839)$ with $|A_{\mathrm{corr}}-0.826|<0.008$; the leading-order gap is nearly closed; $\mathrm{flipCount}(0)\cdot\Delta\tau_{12}=44$; axis-0 flips are twice axis-1 flips with axes 1 and 2 symmetric; $\lambda_{\mathrm{RS}}$ sits in its stated interval; and the $(1,2)$ and $(2,3)$ face fluxes take their geometric values.
background
Module CKMExact derives the Wolfenstein parameter $A$ from first principles of the cube graph $Q_3$, not from a fit. Gray-code edge flips on the three axes give counts $(4,2,2)$. Generation torsion values ${0,11,17}$ supply $\Delta\tau_{12}=11$ and $\Delta\tau_{23}=6$, so the bare ratio is $A_{\mathrm{structural}}=\Delta\tau_{23}/\Delta\tau_{12}=6/11$.
Face fluxes on the generation planes correct that bare ratio: $\mathrm{faceFlux}(12)/\mathrm{faceFlux}(23)=6/4=3/2$. The product $(6/11)\times(3/2)=9/11$ is the corrected prediction. PDG quotes $0.826\pm 0.013$; $9/11\approx 0.818$ sits inside $1\sigma$ with residual under $0.008$.
The same $Q_3$ chirality produces the integer 44 as $\mathrm{flipCount}(\mathrm{axis}0)\times\Delta\tau{12}$, which also appears in the RS expressions for $\alpha^{-1}$ and $\eta_B\approx\varphi^{-44}$. The certificate structure packages every proved equality and inequality that witnesses this chain.
proof idea
One structure literal. Each field is filled by a named theorem already proved in the module: $A_{\mathrm{structural}}=6/11$ and $A_{\mathrm{corrected}}=9/11$ (the latter a one-line simp plus ring from the structural and Berry equalities); Berry factor $3/2$ and square $9/4$ by direct norm_num on face-flux definitions; PDG band and distance by rewriting to $9/11$ and norm_num; gap-closed, forty-four, Gray asymmetry and axis-1/2 symmetry, $\lambda$ interval, and the two face-flux identities by their respective lemmas. No new reasoning occurs at the certificate site.
why it matters
This is the export handle for the module's main claim: Wolfenstein $A=9/11$ from $Q_3$ geometry with zero sorry and zero axioms, inside the PDG $1\sigma$ band. It freezes the five-line derivation (Gray flips $\to$ torsion ratios $\to$ face-flux Berry factor $\to$ $9/11$) and the 44-connection that ties CKM $A$ to the same chirality governing $\alpha^{-1}=44\pi\cdot\exp(-w_8\ln\varphi/44\pi)$ and $\eta_B\approx\varphi^{-44}$.
In the broader RS ladder the result sits downstream of eight-tick/$Q_3$ structure (T7) and generation torsion, and supplies a Standard-Model observable fixed by recognition geometry rather than free Yukawa inputs. No downstream consumers are wired yet; the certificate is the stable citation point for any later CKM or mixing-angle development that needs the exact $A$ package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.