wolfensteinA
plain-language theorem explainer
The declaration supplies the Wolfenstein A parameter as the exact rational 9/11. Particle physicists checking CKM consistency or RS-derived constants against PDG bounds would cite it when certifying the Cabibbo angle proxy. It is introduced by direct assignment of the fraction with no further reduction or lemma application.
Claim. The Wolfenstein parameter $A$ is defined by the equality $A = 9/11$.
background
In the Recognition Science treatment of the CKM matrix the Wolfenstein parameters are extracted from the phi-ladder fixed point. The parameter A appears in the standard parametrization of the CKM matrix as the coefficient scaling the CP-violating phase. This definition is imported from the CKMLambdaFromPhiLadder module where it is tied to the self-similar properties of phi. The module AnomalousMagneticMomentFromRS places this constant in the context of five canonical contributions to the electron g-2 anomaly, with the structure 2/(17 pi) approximating alpha/pi. Upstream results establish the same rational value as a prediction from the phi-ladder.
proof idea
The definition is a direct rational constant assignment. No lemmas are applied; the value 9/11 is posited as the RS-native prediction for the Wolfenstein A parameter.
why it matters
This definition feeds the CKMLambdaCert structure that certifies consistency with PDG data for the Cabibbo angle and the GMTwoCert structure that counts five contributions to the anomalous magnetic moment. It closes the link between the phi-ladder (T6) and observable CKM parameters, allowing the alpha band and g-2 predictions to be checked numerically. The value 9/11 arises from the eight-tick octave structure in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.