V_ud
plain-language theorem explainer
V_ud supplies the real CKM matrix element as the positive square root of one minus V_us squared. Researchers comparing Recognition Science quark mixing to Wolfenstein parametrization would cite this definition when checking approximate first-row unitarity. It is realized as a direct one-line algebraic wrapper around the imported V_us prediction.
Claim. The CKM matrix element is given by $V_{ud} := (1 - V_{us}^2)^{1/2}$, where $V_{us}$ is the up-strange mixing element taken from the rung-difference prediction on the phi-ladder.
background
The module derives CKM mixing angles from rung differences tau_g = 0, 11, 17 on the phi-ladder, producing theta_ij approximately phi to the minus Delta tau over 2 and the Jarlskog invariant as a forced dimensionless output. V_us is imported from the sibling definition V_us_pred, which rests on the geometric proofs in MixingDerivation. The upstream StandardModel.CKMMatrix.V_ud implements the Wolfenstein form 1 minus lambda squared over 2 to order lambda cubed, while the present definition supplies the real positive square root that enforces the approximate unitarity relation when the third element is negligible.
proof idea
The definition is a one-line wrapper that applies the real square root to the complement of V_us squared.
why it matters
This definition feeds the unitarity_triangle_valid theorem and the cp_violation_small result in StandardModel.CKMMatrix, which bound the Jarlskog invariant between zero and 10 to the minus 4. It closes the geometric derivation of CKM parameters from the eight-tick octave and phi-ladder steps T5-T7, providing the real part required for predictions and experimental comparisons. The open question remains whether the small CP phase emerges exactly from residue asymmetry without further fitting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.