berry_correction_pos
plain-language theorem explainer
The Berry face-flux correction for CKM generation mixing is strictly positive. Anyone assembling the corrected Wolfenstein A from Q₃ geometry needs this sign fact when scaling the bare torsion ratio by the flux ratio. The proof rewrites the factor as 3/2 and closes the inequality by arithmetic.
Claim. The Berry correction factor, the ratio of $Q_3$ face fluxes for generation transitions $1\to 2$ over $2\to 3$, is strictly positive: $0 < \mathrm{faceFlux}(1,2)/\mathrm{faceFlux}(2,3)$.
background
The CKMExact module derives the Wolfenstein $A$ parameter from $Q_3$ cube geometry with zero sorry and zero axioms. Gray-code flip counts on axes $(0,1,2)$ are $(4,2,2)$. Generation torsion differences give $\Delta\tau_{12}=11$ and $\Delta\tau_{23}=6$, so the bare structural ratio is $A_{\mathrm{structural}}=6/11$.
The Berry correction multiplies that ratio by the face-flux ratio $\mathrm{faceFlux}(1,2)/\mathrm{faceFlux}(2,3)$. Face fluxes are built from the same flip counts, and the module records the exact value $6/4=3/2$. The corrected prediction is then $A_{\mathrm{corrected}}=(6/11)\times(3/2)=9/11\approx 0.818$, within $0.6\sigma$ of the PDG value $0.826\pm 0.013$.
Upstream, berryCorrection is defined as that real flux ratio, and berry_correction_eq proves it equals $3/2$ by simplifying through faceFlux and flipCount.
proof idea
One-line tactic proof. Rewrite the goal with berry_correction_eq, which reduces the defined flux ratio to the concrete rational $3/2$ (via simp on faceFlux and flipCount). Then norm_num discharges $0<3/2$.
why it matters
Positivity is a local arithmetic gate in the five-line derivation of $A_{\mathrm{corrected}}=9/11$ from $Q_3$ face flux. The module narrative ties the same $[4,2,2]$ Gray chirality and the composite $44=4\times 11$ into three RS landmarks: $\alpha^{-1}$ (via the $44\pi$ prefactor), the baryon-to-photon ratio $\eta_B\approx\varphi^{-44}$, and the CKM $A$ parameter. No recorded downstream dependents yet; the lemma sits as a sign check before the exact corrected-$A$ identity. It does not itself invoke the forcing chain T0–T8, but it inherits the eight-tick/$Q_3$ geometry that T7 forces.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.