V_ts
plain-language theorem explainer
V_ts supplies the CKM matrix element for the top-to-strange transition as negative A times lambda squared in the Wolfenstein parametrization. Quark flavor physicists cite this when evaluating B-meson mixing or rare decays. The definition is a direct algebraic substitution of the two upstream Wolfenstein constants.
Claim. The CKM matrix element satisfies $V_{ts}=-Aλ^2$, where $A≈0.82$ and $λ≈0.227$ equals the sine of the Cabibbo angle.
background
The module derives CKM elements from Recognition Science using φ-quantized mixing angles tied to the eight-tick phase structure. Wolfenstein parameters enter as lambda equal to the Cabibbo sine and A a fitted scaling factor near 0.82. Upstream definitions fix these as explicit real constants for all subsequent matrix elements.
proof idea
The definition is a one-line algebraic assignment that multiplies wolfenstein_A by the square of wolfenstein_lambda and prefixes a minus sign.
why it matters
It contributes one entry to the CKM matrix construction in the StandardModel module, which targets derivation of quark mixing from RS φ-angles as stated in the PRD paper proposition. The element supports the downstream unitarity_triangle_valid theorem. This placement aligns with the T7 eight-tick octave landmark by encoding discrete phase relations into the mixing amplitudes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.