V_ud
plain-language theorem explainer
The definition supplies the (1,1) entry of the CKM matrix in Wolfenstein parametrization as one minus half the square of the Cabibbo parameter lambda. Quark-mixing and CP-violation calculations in the standard model would cite this entry when assembling the full matrix or checking leading-order unitarity. It is obtained by direct substitution of the imported wolfenstein_lambda definition.
Claim. The up-down CKM matrix element is given by $V_{ud} = 1 - (λ^2)/2$, where $λ$ is the Wolfenstein parameter equal to the sine of the Cabibbo angle.
background
In Recognition Science the CKM matrix parametrizes quark flavor mixing and is derived from φ-quantized angles tied to the eight-tick phase structure. The Wolfenstein parametrization expands the matrix in powers of λ ≈ sin θ_C ≈ 0.227. This module supplies the approximate elements to O(λ³) as shown in the displayed 3×3 form.
proof idea
The declaration is a one-line definition that directly substitutes the algebraic expression 1 - wolfenstein_lambda^2 / 2 into the complex numbers.
why it matters
This entry is used by cp_violation_small, unitarity_triangle_valid, experimentalValues and predictions. It advances the module claim that CKM parameters emerge from φ-angles in the eight-tick octave. The surrounding framework seeks to obtain the full standard model from the J-cost functional equation and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.