V_cb
plain-language theorem explainer
The definition supplies the Wolfenstein parametrization for the CKM matrix element V_cb as the product of parameter A and lambda squared. Quark flavor physicists and RS model builders cite this when matching geometric predictions to experimental mixing data. It is a direct one-line algebraic definition using the imported Wolfenstein constants.
Claim. The CKM matrix element $V_{cb}$ equals $A lambda^2$, where $A approx 0.82$ is the Wolfenstein parameter and $lambda approx 0.227$ equals the sine of the Cabibbo angle.
background
The StandardModel.CKMMatrix module constructs the CKM matrix from phi-quantized mixing angles tied to the eight-tick phase structure. Wolfenstein parameters supply the conventional approximation to the matrix elements, with lambda defined as the Cabibbo angle and A fixed at 0.82. This V_cb definition multiplies those two constants. Upstream, the Physics.CKM module supplies a separate predicted V_cb from other RS considerations, while the module documentation targets derivation of the full CKM matrix from Recognition Science.
proof idea
One-line definition that multiplies the Wolfenstein A parameter by the square of the lambda parameter.
why it matters
This definition feeds the Jarlskog witness positivity theorem, the s23_w sine definition, the T11Cert geometric certificate linking V_cb to cube edges, and the V_cb_from_cube_edges theorem. It supports the paper proposition on CKM matrix from golden ratio geometry by supplying the standard parametrization that RS derivations must match. The construction sits inside the eight-tick octave and D=3 framework landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.