V_cb
plain-language theorem explainer
The definition sets the CKM matrix element V_cb to the product of Wolfenstein parameters A and lambda squared. Particle physicists deriving quark mixing angles from Recognition Science would cite this when linking the eight-tick phase structure to experimental CKM values. The construction is a direct one-line definition that multiplies the imported constants.
Claim. The CKM matrix element $V_{cb}$ equals $A lambda^2$, where $A approx 0.82$ is the Wolfenstein parameter and $lambda = sin theta_C approx 0.227$ is the sine of the Cabibbo angle.
background
The module derives CKM matrix elements from phi-quantized mixing angles tied to the eight-tick phase structure in Recognition Science. The Wolfenstein parameterization approximates the 3x3 unitary matrix with four parameters, and this definition supplies the (2,3) element magnitude. Upstream, wolfenstein_lambda is defined as cabibboAngle and wolfenstein_A as the constant 0.82.
proof idea
This is a one-line definition that multiplies the Wolfenstein A parameter by the square of the lambda parameter.
why it matters
This definition supplies the V_cb value used in downstream results such as the Jarlskog witness positivity theorem and the T11 certificate for geometric origin from cube edges. It fills the SM-012 target of deriving CKM elements from phi-angles in the eight-tick structure. It connects to the broader RS derivation of Standard Model parameters via the Recognition Composition Law and D=3 spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.