V_td
plain-language theorem explainer
V_td supplies the complex (3,1) entry of the CKM matrix in the Wolfenstein parametrization to order λ³. Quark-flavor physicists cite it when evaluating CP-violating observables or unitarity triangles in the Standard Model. The definition is a direct algebraic product of the four Wolfenstein parameters A, λ, ρ, η.
Claim. $V_{td} = A λ^3 (1 - ρ - i η)$ where $A ≈ 0.82$, $λ ≈ 0.227$, $ρ ≈ 0.14$, $η ≈ 0.35$ are the Wolfenstein parameters.
background
The module derives the CKM matrix from φ-quantized mixing angles tied to the eight-tick phase structure. The Wolfenstein parametrization expands the 3×3 unitary matrix in powers of the Cabibbo angle λ, with four real parameters A, λ, ρ, η that encode the three mixing angles and one CP-violating phase. Upstream definitions fix the numerical values: wolfenstein_lambda equals the Cabibbo angle, wolfenstein_A is 0.82, wolfenstein_rho is 0.14, and wolfenstein_eta is 0.35.
proof idea
One-line definition that multiplies wolfenstein_A, wolfenstein_lambda raised to the third power, and the complex factor (1 - wolfenstein_rho - I * wolfenstein_eta).
why it matters
This definition populates the CKM matrix used by downstream theorems cp_violation_small and unitarity_triangle_valid. It implements the φ-quantized mixing angles stated in the module doc-comment for deriving the CKM matrix from Recognition Science. The construction connects to the eight-tick phase structure and the T7 octave landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.