Pith. sign in
theorem

faceFlux_23

proved
show as:
module
IndisputableMonolith.StandardModel.CKMExact
domain
StandardModel
line
133 · github
papers citing
none yet

plain-language theorem explainer

The Q₃ face spanning generation axes 1 and 2 carries face flux 4, equal to the sum of the two minor Gray-code flip counts. CKM derivations cite this as the denominator of the Berry face-flux correction that lifts structural A = 6/11 to A = 9/11. The equality is definitional (rfl).

Claim. The face flux on the generation face spanning axes $1$ and $2$ equals $4$. Explicitly, if flip counts on the three Gray-code axes are $(4,2,2)$, then the $2\to 3$ face flux is $2+2=4$.

background

Module CKMExact derives the Wolfenstein parameter $A$ from $Q_3$ geometry. The Gray-code flip counts on the three cube axes are $(4,2,2)$: axis $0$ is dominant (four flips), axes $1$ and $2$ are minor (two flips each). Face flux on a generation face is the sum of the flip counts of the two axes that span it.

Generation torsion supplies $\Delta\tau_{12}=11$ and $\Delta\tau_{23}=6$, so the structural ratio is $A_{\mathrm{structural}}=\Delta\tau_{23}/\Delta\tau_{12}=6/11$. The Berry correction multiplies by the ratio of face fluxes $\mathrm{faceFlux}(1{,}2)/\mathrm{faceFlux}(2{,}3)$. The $1\to 2$ face (axes $0,1$) has flux $4+2=6$; the present $2\to 3$ face (axes $1,2$) has flux $2+2=4$.

The same $[4,2,2]$ chirality appears in the fine-structure and baryon-asymmetry $44$-factors ($4\times 11$), tying CKM $A$ to those constants.

proof idea

One-line term proof by rfl. Once face flux is defined as the sum of the two spanning axes' flip counts, and those counts are already reduced to the numerals $2$ and $2$ on axes $1$ and $2$, the equality $2+2=4$ holds definitionally. No lemmas are invoked.

why it matters

Feeds ckmExactCert, which packages the full exact CKM certificate: structural $A$, Berry factor, corrected $A=9/11$, and the PDG $1\sigma$ check. Module derivation step 4 needs $\mathrm{faceFlux}(2{,}3)=4$ so that the correction is $6/4=3/2$ and $A_{\mathrm{corrected}}=(6/11)\times(3/2)=9/11\approx 0.818$ (PDG $0.826\pm 0.013$, within $0.6\sigma$).

Closes the minor-face half of the face-flux pair; together with the $1\to 2$ flux of $6$ it supplies the geometric $3/2$ that converts torsion ratios into the observed Wolfenstein $A$. Sits inside the broader $Q_3$ story linking Gray-code chirality, eight-tick structure, and the shared factor $44$ across $\alpha^{-1}$, $\eta_B$, and CKM.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.