A_corrected_tight
plain-language theorem explainer
The Berry-corrected Wolfenstein A parameter lies strictly between 0.818 and 0.819. Phenomenologists matching Recognition Science CKM output to PDG would cite this sandwich. The proof rewrites via the exact identity A = 9/11 and closes both inequalities by numerical normalization.
Claim. The Berry-corrected Wolfenstein parameter $A$ satisfies $0.818 < A < 0.819$.
background
In the Wolfenstein parameterization of the CKM matrix, $A$ is the leading real coefficient that sets the scale of $V_{cb}$ and related mixings. Recognition Science builds a structural value $A_{\mathrm{structural}} = \Delta\tau_{23}/\Delta\tau_{12} = 6/11$ from generation torsion on the $Q_3$ cube, then multiplies by a Berry face-flux correction $\mathrm{berryCorrection} = \mathrm{faceFlux}(12)/\mathrm{faceFlux}(23) = 3/2$.
The product is the corrected parameter $A_{\mathrm{corrected}} := A_{\mathrm{structural}} \times \mathrm{berryCorrection}$. The module proves $A_{\mathrm{corrected}} = 9/11$ exactly, starting from Gray-code flip counts $(4,2,2)$ and torsion gaps ${0,11,17}$. The local setting is closed: zero sorry, zero axioms.
Upstream, A_corrected_exact supplies the rational identity used here. The same $Q_3$ chirality package also feeds the fine-structure and baryon-asymmetry 44-factors recorded in the module header.
proof idea
Short term-mode proof. Rewrite the goal with A_corrected_exact, replacing $A_{\mathrm{corrected}}$ by the rational $9/11$. Split the conjunction and discharge each strict inequality $0.818 < 9/11$ and $9/11 < 0.819$ by norm_num.
why it matters
Closes a one-thousandth-wide numerical window around the exact RS prediction $A = 9/11 \approx 0.81818\ldots$. The module records PDG $0.826 \pm 0.013$, so the prediction sits roughly $0.6\sigma$ below the central value and well inside the $1\sigma$ band $(0.813, 0.839)$.
Together with the exact identity $A = 9/11$, this is the terminal numerical claim of the CKMExact chain: Gray flips $\to$ torsion gaps $\to$ structural $A$ $\to$ Berry correction $\to$ $9/11$. It participates in the broader 44-connection: $\mathrm{flipCount}(\mathrm{axis}0) \times \Delta\tau{12} = 4 \times 11 = 44$ also governs $\alpha^{-1}$ and $\eta_B \approx \varphi^{-44}$. No downstream dependents are recorded yet; the result stands as a self-contained PDG-facing bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.