V_cd
plain-language theorem explainer
V_cd is defined as the negation of V_us, inheriting the phi-ladder prediction for the Cabibbo angle magnitude. Researchers modeling quark flavor mixing in the Recognition Science framework cite this when constructing the full CKM matrix for Jarlskog invariant or unitarity triangle calculations. The definition performs a direct sign flip with no additional lemmas or reductions.
Claim. The CKM matrix element $V_{cd}$ equals $-V_{us}$, where $V_{us}$ denotes the real-valued prediction $V_{us_pred}$ obtained from rung differences on the $phi$-ladder.
background
The CKM module derives mixing parameters from rung differences $tau_g = 0, 11, 17$ between up- and down-type quark generations, producing angles scaling as $phi^{-Delta tau / 2}$. V_us is set to V_us_pred from the MixingDerivation import, which supplies the geometric value. This V_cd then provides the required negative counterpart to match the conventional CKM structure used in StandardModel.CKMMatrix, where the corresponding definitions employ the Wolfenstein parameter lambda.
proof idea
The declaration is a one-line wrapper that negates the upstream value of V_us.
why it matters
This supplies the V_cd component used by cp_violation_small to establish that the Jarlskog invariant lies between 0 and 10^{-4}, by predictions for lambda approx (phi-1)^2/phi, and by unitarity_triangle_valid. It closes the geometric derivation of the CKM matrix from the phi-ladder, linking the T7 eight-tick period to the small observed CP violation. The parent theorems in StandardModel.CKMMatrix rely on this sign convention to reproduce the unitarity constraint.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.