s13_w
s13_w aliases the real Wolfenstein V_ub to stand for sin θ13 in the CKM mixing angles derived from quark rung differences. Researchers assembling the Jarlskog invariant from the phi-ladder would cite this when forming the product s12_w s23_w s13_w. The definition is a direct one-line alias to the upstream V_ub_pred.
claim$s_{13}^w := |V_{ub}|$, where $V_{ub}$ is the (1,3) element of the CKM matrix obtained from rung differences on the φ-ladder between up and down quark generations.
background
The CKM module derives mixing angles θ_ij ≈ φ^{-Δτ/2} from rung differences at τ_g = 0, 11, 17 for the three generations, with the Jarlskog invariant J emerging as a forced dimensionless output. V_ub is introduced as the real approximation V_ub_pred to the Wolfenstein form A λ^3 (ρ - i η) taken from the Standard Model CKM matrix definition. This sits inside the geometric construction supplied by MixingDerivation, which supplies the underlying jarlskog_pos result used for positivity.
proof idea
One-line definition that directly aliases s13_w to V_ub, which itself expands to V_ub_pred from the same module and to the complex Wolfenstein expression from StandardModel.CKMMatrix.
why it matters in Recognition Science
This supplies the s13 factor for jarlskog_witness := s12_w * s23_w * s13_w, which approximates the Jarlskog invariant in the φ-ladder derivation of CKM phenomenology. It feeds the downstream jarlskog_witness_pos theorem, which proves strict positivity by unfolding to MixingDerivation.jarlskog_pos and matching the product V_us V_cb V_ub to the predicted edge_dual_ratio term. The placement closes the rung-difference step that forces the CP phase from residue asymmetry.
scope and limits
- Does not derive the numerical magnitude of V_ub from the φ-ladder equations.
- Does not retain the imaginary part or explicit CP phase of the full complex V_ub.
- Does not enforce full CKM unitarity or higher-order radiative corrections.
Lean usage
unfold s13_w; exact V_ubformal statement (Lean)
62noncomputable def s13_w : ℝ := V_ub
proof body
Definition body.
63