V_ub_exp
V_ub_exp supplies the measured central value of the CKM matrix element |V_ub| as the real number 0.00369. Flavor physicists comparing the geometric prediction |V_ub| = alpha/2 to experimental data would cite this constant inside matching theorems. The declaration is a direct numerical assignment carrying no proof obligations or computational steps.
claimThe experimental central value of the CKM matrix element is defined by $V_{ub}^{exp} := 0.00369$.
background
The CKM Geometry module formalizes the T11 hypothesis that the three CKM magnitudes arise from geometric couplings on the cubic ledger. Specifically, |V_ub| is identified with the fine-structure coupling alpha/2, while |V_cb| is fixed at 1/24 and |V_us| follows from the golden projection phi^{-3} minus a radiative correction linear in alpha. The module imports alpha bounds and phi-ladder constants to support interval comparisons between these predictions and measured values.
proof idea
This declaration is a direct definition that assigns the constant 0.00369 to V_ub_exp with no lemmas or tactics applied.
why it matters in Recognition Science
V_ub_exp anchors the experimental side of the CKMElementScoreCardCert structure and the V_ub_match theorem, which confirms that the geometric prediction lies inside the quoted error bar. It thereby completes one verification step of the T11 ledger-geometry derivation of flavor mixing. The same constant is referenced by alpha_upper_bound when tightening the interval for alpha/2.
scope and limits
- Does not derive the numerical value from the phi-ladder or alpha derivation.
- Does not embed the experimental uncertainty interval.
- Does not establish relations among the three CKM elements.
- Does not incorporate higher-order radiative corrections.
Lean usage
theorem row_V_ub : abs (V_ub_pred - V_ub_exp) < V_ub_err := V_ub_matchformal statement (Lean)
54def V_ub_exp : ℝ := 0.00369