A_corrected_pos
plain-language theorem explainer
The Berry-corrected Wolfenstein A parameter is strictly positive. Anyone working the CKMExact Q₃ derivation (A = 9/11) cites this for interval membership and PDG-band lemmas. Proof rewrites to the exact fraction 9/11 and finishes by numeric evaluation.
Claim. The Berry-corrected Wolfenstein parameter $A_{\mathrm{corr}}:=A_{\mathrm{structural}}\cdot\mathrm{berryCorrection}$ equals $9/11$ and satisfies $0 < A_{\mathrm{corr}}$.
background
In the CKMExact module, the Wolfenstein $A$ is derived from $Q_3$ Gray-code geometry rather than fit to data. Flip counts on the three axes are $(4,2,2)$; generation torsion supplies $\Delta\tau_{12}=11$ and $\Delta\tau_{23}=6$. The structural ratio is $A_{\mathrm{structural}}=\Delta\tau_{23}/\Delta\tau_{12}=6/11$.
A face-flux (Berry) correction multiplies by $\mathrm{faceFlux}(12)/\mathrm{faceFlux}(23)=3/2$, so the corrected parameter is defined as $A_{\mathrm{corrected}}:=A_{\mathrm{structural}}\cdot\mathrm{berryCorrection}$. The main theorem of the module states $A_{\mathrm{corrected}}=9/11$ exactly. The present lemma only records positivity of that real number, which is needed for the tight PDG interval $(0.818,0.819)$ proved next in the same section.
proof idea
Term-mode one-liner. Rewrite the goal with A_corrected_exact (which replaces $A_{\mathrm{corrected}}$ by $9/11$), then close $0<9/11$ by norm_num. No structural lemmas about Gray code or torsion are reopened here.
why it matters
Closes the positivity half of the PDG-consistency block for the RS prediction $A=9/11\approx 0.818$ (PDG $0.826\pm 0.013$, within $0.6\sigma$). The same $Q_3$ chirality that forces $A_{\mathrm{corrected}}=9/11$ also produces the factor $44=4\times 11$ appearing in $\alpha^{-1}$ and $\eta_B\approx\varphi^{-44}$, so positivity of $A$ is a trivial but required sanity check on that shared geometric source. No downstream consumers are recorded yet; the immediate parent narrative is the fully proved CKMExact chain (structural ratio times Berry face-flux correction).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.