row_V_ub
plain-language theorem explainer
The declaration establishes that the RS-predicted CKM element V_ub equals half the fine-structure constant and lies inside the experimental 1-sigma band around the PDG central value 0.00369. CKM phenomenology analyses would cite the row when testing geometric predictions against measured magnitudes. The proof is a direct one-line wrapper that invokes the matching theorem already proved in the geometry module.
Claim. $|V_{ub}^{pred} - V_{ub}^{exp}| < V_{ub}^{err}$, where $V_{ub}^{pred} = α/2$, $V_{ub}^{exp} = 0.00369$, and $V_{ub}^{err} = 0.00011$.
background
The module treats the three leading CKM magnitudes as geometric ratios extracted from the Recognition Science cube. V_ub_pred is defined as fine_structure_leakage, which equals α/2. The experimental anchor is the constant V_ub_exp = 0.00369 together with the 1-sigma tolerance V_ub_err = 0.00011 taken from PDG-style averages. Upstream, V_ub_match records the numerical verification that the interval (0.003645, 0.003655) produced by the certified α bounds sits inside the error band.
proof idea
One-line wrapper that applies V_ub_match from CKMGeometry. The tactic block inside V_ub_match uses the alpha lower and upper bounds together with linarith to confirm the absolute difference is strictly less than the error term.
why it matters
The row is collected by ckmElementScoreCardCert_holds into the full CKMElementScoreCardCert certificate that bundles the three magnitude checks. It supplies the V_ub entry required by the module-level falsifier: any future PDG update that pushes the experimental value outside the proved inequality would refute the fine_structure_leakage prediction. The result therefore closes one cell of the Phase-2 CKM scorecard under the fixed RS inputs for α and φ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.