s12_w
plain-language theorem explainer
s12_w aliases the up-strange CKM matrix element V_us derived from rung differences in the phi-ladder. Quark-mixing researchers cite it when assembling the Jarlskog invariant from geometric predictions of theta_ij. The definition is a direct one-line alias to the upstream V_us_pred with no further reduction.
Claim. The sine of the Cabibbo angle equals the up-strange element of the CKM matrix, $V_{us}$.
background
The CKM module derives mixing angles from rung differences tau_g = 0, 11, 17 between up and down quark generations, yielding theta_ij approximately phi to the power of minus half the rung difference. This local setting rests on the geometric proofs imported from MixingDerivation. V_us is defined as V_us_pred in the same module and as wolfenstein_lambda in the Standard Model CKM matrix.
proof idea
This is a one-line definition that directly aliases the upstream V_us from the CKM module, which itself aliases V_us_pred.
why it matters
This supplies the s12 component to the Jarlskog witness defined as the product of the three sines, which is shown positive by jarlskog_witness_pos using jarlskog_pos from MixingDerivation. It supports the derivation of the Jarlskog invariant J as a forced dimensionless output from the phi-ladder. The parent result is the positivity theorem jarlskog_witness_pos.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.