V_us
plain-language theorem explainer
V_us supplies the (1,2) entry of the CKM quark-mixing matrix by direct alias to the Wolfenstein parameter λ. Quark-flavor physicists assembling Standard-Model predictions inside Recognition Science cite it when building the full 3×3 matrix or evaluating the Jarlskog invariant. The declaration is a one-line alias to wolfenstein_lambda, which itself reduces to the Cabibbo-angle definition.
Claim. The CKM matrix element $V_{us}$ is defined to equal the Wolfenstein parameter $λ$, where $λ = sin θ_C$ and $θ_C$ is the Cabibbo angle.
background
The StandardModel.CKMMatrix module derives the full CKM matrix from φ-quantized mixing angles that arise from the eight-tick phase structure. Wolfenstein parameterization is adopted so that the single real parameter λ ≈ 0.227 encodes the dominant Cabibbo mixing. Upstream, wolfenstein_lambda is introduced as the alias cabibboAngle; a parallel real-valued V_us appears in the Physics.CKM module as the predicted value V_us_pred.
proof idea
One-line definition that directly aliases wolfenstein_lambda.
why it matters
The definition feeds fifteen downstream sites, including V_ud, V_cd, s12_w, jarlskog_witness_pos, and torsion_differences. It supplies the concrete numerical input required by the CKM-from-golden-ratio-geometry program stated in the module header (PRD target). The construction sits inside the T7 eight-tick octave of the forcing chain and supplies the leading off-diagonal entry used to close the unitary triangle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.