V_ub_err
plain-language theorem explainer
V_ub_err fixes the experimental tolerance on the CKM element V_ub at 0.00011 for use in geometric matching. CKM phenomenology groups would cite this constant when testing ledger-derived predictions against data. The definition is a direct assignment of the real constant 0.00011.
Claim. The uncertainty assigned to the CKM matrix element $|V_{ub}|$ is defined to be $0.00011$.
background
The CKMGeometry module formalizes derivation of the CKM mixing angles from cubic ledger geometry and the fine-structure constant. Module documentation identifies |V_ub| with the fine-structure leakage (theta-13 coupling) given by alpha/2, yielding the prediction 0.00365 against the observed value 0.00369(11). Upstream results supply fine_structure_leakage as Constants.alpha / 2 and V_ub as the corresponding predicted value. The local theoretical setting is T11, which treats the three CKM elements as geometric couplings on the ledger.
proof idea
This is a one-line constant definition that directly assigns the real number 0.00011.
why it matters
The bound is consumed by the certification structure CKMElementScoreCardCert and the theorem row_V_ub to verify that the geometric prediction lies inside experimental tolerance. It supports V_ub_match, which confirms the fine-structure leakage prediction matches data to better than 1 sigma using the alpha interval bounds. In the Recognition framework it closes the verification step for the theta-13 term in T11.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.