wolfensteinA
plain-language theorem explainer
The Wolfenstein A parameter is supplied as the rational 9/11. Particle physicists fitting CKM elements or computing anomalous magnetic moments would cite this RS prediction. The definition is a direct assignment that downstream theorems unfold to verify PDG agreement within one sigma.
Claim. The Wolfenstein parameter $A$ equals $9/11$.
background
In the CKM Wolfenstein parameterization the parameter A sets the scale of the mixing hierarchy. Recognition Science fixes A = 9/11 ≈ 0.818 from the phi-ladder construction, placing it inside the PDG interval 0.826 ± 0.013. The module documentation states this value is proved in GaugeFromCube and enters alpha_s and g-2 calculations.
proof idea
Direct definition that assigns the rational constant 9/11.
why it matters
The definition supplies the fixed value required by CKMLambdaCert and GMTwoCert. It implements the RS prediction A = 9/11 stated in the module documentation and is shown inside the PDG 1σ band by wolfensteinA_in_pdg_band. The value connects to the phi-ladder and the alpha band in the T0-T8 chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.