faceFlux
plain-language theorem explainer
Face flux between two quark generations is the sum of Gray-code flip counts on the two Q₃ axes those generations span. Anyone deriving the Wolfenstein A parameter from Q₃ geometry cites this quantity. It is a one-line definition: add the two axis flip counts (4,2,2 on axes 0,1,2).
Claim. For generations $i,j \in \{0,1,2\}$, the face flux on the $Q_3$ face spanning axes $i$ and $j$ is $N_i + N_j$, where $N_k$ is the Gray-code flip count on axis $k$ ($N_0=4$, $N_1=N_2=2$).
background
The module derives the Wolfenstein $A$ parameter from $Q_3$ geometry: the three-cube whose edges are traversed by the eight-tick Gray code. Flip counts on the three axes are fixed at $(4,2,2)$: axis 0 flips four times per cycle, axes 1 and 2 twice each.
Generations map to axes (gen 1 → axis 0, gen 2 → axis 1, gen 3 → axis 2). The face joining generations $i$ and $j$ is the square spanned by those two axes; its normal is the unused third axis. Face flux is the total number of recognition-operator transitions along the edges of that face in one 8-tick cycle.
Upstream, flipCount supplies the axis values. The structural CKM ratio comes from generation torsion $\Delta\tau_{23}/\Delta\tau_{12}=6/11$; face flux supplies the geometric correction that multiplies it.
proof idea
Pure definition: face flux of generations $i$ and $j$ is the sum of the two Gray-code flip counts on axes $i$ and $j$. No proof obligations. Concrete values follow by unfolding: face $1\to 2$ gives $4+2=6$, face $2\to 3$ gives $2+2=4$, face $1\to 3$ gives $4+2=6$.
why it matters
This is step 4 of the five-line CKMExact derivation. The Berry correction is the ratio of face fluxes $1\to 2$ over $2\to 3$, i.e. $6/4=3/2$. Multiplying the bare torsion ratio $A_{\mathrm{structural}}=6/11$ by that factor yields $A_{\mathrm{corrected}}=9/11\approx 0.818$, inside $0.6\sigma$ of the PDG value $0.826\pm 0.013$.
Downstream: berryCorrection, the equality berry_correction_eq, the three face-value lemmas, and the certificate structure CKMExactCert (0 sorry, 0 axioms) all consume face flux. The same $[4,2,2]$ chirality that sets face flux also appears in the fine-structure and baryon-asymmetry "44" identities ($4\times 11$), tying CKM mixing to the eight-tick octave and $Q_3$ geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.