V_cs
plain-language theorem explainer
The charm-strange element of the CKM quark mixing matrix is defined as one minus half the square of the Wolfenstein lambda parameter. Researchers modeling weak quark decays in the Standard Model would cite this approximation when estimating flavor-changing amplitudes. The definition performs a direct algebraic substitution from the upstream Cabibbo angle.
Claim. The charm-strange CKM matrix element is given by $V_{cs} = 1 - (1/2) lambda^2$, where lambda is the Wolfenstein parameter equal to 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. Wolfenstein lambda is supplied upstream as the Cabibbo angle value, approximately 0.227, serving as the leading off-diagonal mixing parameter. Module documentation frames the target as deriving the full CKM matrix from RS, with listed approximate magnitudes matching the standard experimental pattern.
proof idea
This declaration is a one-line definition that substitutes the upstream wolfenstein lambda value into the standard second-order Wolfenstein expansion for the diagonal CKM element.
why it matters
The definition populates the CKM matrix required by the downstream unitarity triangle theorem that enforces the rho-eta bound. It advances the SM-012 derivation of CKM elements from golden ratio geometry, consistent with the T7 eight-tick octave landmark in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.