V_ub
plain-language theorem explainer
The definition supplies the complex CKM matrix element V_ub in Wolfenstein form. Flavor physicists cite it when evaluating CP-violating observables such as the Jarlskog invariant. It is a direct one-line algebraic product of the four Wolfenstein parameters.
Claim. $V_{ub} = A λ^3 (ρ - i η)$ where $A ≈ 0.82$, $λ ≈ sin θ_C ≈ 0.227$, $ρ ≈ 0.14$, and $η ≈ 0.35$ are the Wolfenstein parameters.
background
The StandardModel.CKMMatrix module parametrizes the 3×3 CKM quark-mixing matrix using four Wolfenstein parameters that encode the three mixing angles and one CP-violating phase. Wolfenstein lambda is identified with the sine of the Cabibbo angle; the remaining parameters A, rho, and eta are assigned the fixed approximate values 0.82, 0.14, and 0.35. This construction sits downstream of the Physics.CKM module, which supplies a separate real-valued prediction V_ub_pred, and is consistent with the module-level goal of deriving CKM elements from φ-quantized angles tied to the eight-tick phase structure.
proof idea
The definition is a one-line algebraic expression that multiplies the Wolfenstein A parameter by lambda to the third power and then by the complex number (rho minus i times eta).
why it matters
The element feeds directly into the Jarlskog witness positivity theorem and the definition of the sine of the 13 mixing angle, both of which appear in downstream CKMGeometry and MixingDerivation results. It therefore supplies the concrete complex value required for the Recognition Science claim that CKM parameters emerge from φ-angles and the eight-tick octave. The module doc-comment links the construction to the paper proposition on CKM matrix elements from golden-ratio geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.