row_vub_eq_leakage
plain-language theorem explainer
The equality sets the RS geometric prediction for the CKM element |V_ub| equal to the fine-structure leakage term alpha/2. CKM phenomenologists comparing cube-derived magnitudes to PDG data would cite this when checking the V_ub row. The proof is a direct one-line wrapper invoking the upstream vub_derived theorem.
Claim. The RS-predicted CKM element satisfies $V_{ub}^{pred} = alpha/2$, where the right-hand side is the parity-split leakage between non-adjacent generations.
background
The module develops Phase 2 CKM predictions from cube geometry. V_ub_pred is defined in CKMGeometry as the fine_structure_leakage term. fine_structure_leakage itself is defined in MixingGeometry as Constants.alpha / 2 and represents the coupling between first and third generations mediated by vacuum polarization across the cube diagonal of length sqrt(3).
proof idea
This is a one-line wrapper that applies the vub_derived theorem from MixingDerivation after unfolding V_ub_pred and fine_structure_leakage.
why it matters
The result supplies the V_ub equality used inside the downstream ckmElementScoreCardCert_holds theorem that assembles the full certified score card. It completes the geometric prediction step for the P2-CKM phase, tying the alpha band and the cubic ledger for three-generation torsion overlap to the Recognition Science constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.