V_ub_match
plain-language theorem explainer
V_ub_match establishes that the CKM element predicted as half the fine-structure constant lies inside the experimental one-sigma interval around 0.00369. Flavor physicists comparing Recognition Science ledger geometry to PDG data would cite the bound when checking T11 predictions. The proof obtains the alpha interval bounds, simplifies the target definitions, and reduces the absolute-value claim to two linear-arithmetic goals.
Claim. $|V_{ub, pred} - 0.00369| < 0.00011$, where $V_{ub, pred} = α/2$ and $α$ is the fine-structure constant.
background
The CKMGeometry module derives the three CKM magnitudes from cubic-ledger couplings. Theta-13 is identified with the fine-structure leakage: |V_ub| equals alpha over 2. The experimental central value and error are hard-coded as 0.00369 and 0.00011. Alpha itself is imported from Constants.Alpha as the reciprocal of the derived alphaInv.
proof idea
The tactic proof pulls in alpha_lower_bound and alpha_upper_bound. It simplifies the goal with the definitions of V_ub_pred, V_ub_exp, V_ub_err and fine_structure_leakage. Two linarith steps confirm alpha/2 lies inside (0.003645, 0.003655). The absolute-value inequality is rewritten and discharged by constructor plus linarith on each side.
why it matters
The result supplies the V_ub row of CKMElementScoreCard.row_V_ub. It closes the numeric check for the T11 hypothesis that |V_ub| = alpha/2 matches observation to better than one sigma. In the broader framework the bound links the J-uniqueness derivation of alpha to CKM phenomenology; the parent theorem row_V_ub simply invokes this match.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.