rs_V_ub
plain-language theorem explainer
rs_V_ub defines the CKM matrix element |V_ub| as the cube of the Cabibbo parameter in the Recognition Science framework. Particle physicists checking quark mixing hierarchies from torsion geometry would cite this when verifying structural bounds on the full CKM matrix. The definition is a direct power operation on the upstream cabibbo_parameter with no additional lemmas.
Claim. The CKM matrix element satisfies $|V_{ub}| := (φ^{-11})^3$, where $φ^{-11}$ is the Cabibbo parameter obtained from the torsion difference of 11 between the first two generations.
background
The module derives CKM elements from φ-geometry and the generation torsion schedule {0, 11, 17} on the Q3 cube, with mixing arising from torsion mismatch between up-type and down-type sectors. The upstream cabibbo_parameter is defined directly as φ^{-11}, matching the relation sin(θ_C) ≈ φ^{-(τ1 - τ0)} = φ^{-11} stated in the module documentation. This supplies the base value for the three rs_V_* definitions that populate the CKMCert structure.
proof idea
One-line definition that applies the cabibbo_parameter and raises the result to the third power. No tactics or lemmas beyond the definition of the parameter are required.
why it matters
This supplies the smallest element needed by the downstream CKMCert structure, ckm_hierarchy theorem, and ckm_unitarity_structural theorem to verify the inequalities rs_V_ub < rs_V_cb < rs_V_us and the sum-of-squares bound. It completes the set of CKM elements derived from the torsion schedule {0, 11, 17} and the φ-geometry approach described in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.