s12_w
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the numerical value of V_us from the forcing chain.
- Does not verify agreement with experimental data.
- Does not extend to other CKM elements or phases.
Lean usage
noncomputable def jarlskog_witness : ℝ := s12_w * s23_w * s13_wformal statement (Lean)
60noncomputable def s12_w : ℝ := V_us