row_V_ub
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 in Recognition Science
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 φ.
scope and limits
- Does not derive the numerical value of α from the Recognition functional equation.
- Does not address CP-violating phases or the full unitarity triangle.
- Does not incorporate higher-order corrections beyond the leading geometric ratio.
- Does not replace the separate Wolfenstein parameterization used elsewhere in the library.
Lean usage
example : abs (V_ub_pred - V_ub_exp) < V_ub_err := row_V_ubformal statement (Lean)
37theorem row_V_ub : abs (V_ub_pred - V_ub_exp) < V_ub_err := V_ub_match
proof body
38