V_cb_err
plain-language theorem explainer
V_cb_err supplies the experimental uncertainty 0.00085 on the CKM matrix element |V_cb|. Researchers verifying geometric derivations of mixing angles against PDG data would cite this bound when checking the edge-dual prediction. The declaration is a direct numeric assignment with no computation or lemmas.
Claim. The uncertainty on the observed value of the CKM matrix element $|V_{cb}|$ is $0.00085$.
background
The CKMGeometry module derives the three CKM matrix elements from cubic ledger geometry and the fine-structure constant. The edge-dual coupling fixes |V_cb| = 1/(2 * cube_edges 3) = 1/24 exactly. V_cb_err supplies the tolerance used to compare this rational prediction against the experimental central value 0.04182.
proof idea
Direct definition that assigns the real constant 0.00085. No lemmas, tactics, or reductions are applied.
why it matters
V_cb_err closes the experimental comparison in T11Cert and V_cb_match, confirming that the geometric prediction 1/24 lies inside the stated error. It thereby supports the T11 claim that |V_cb| arises from cube-edge geometry rather than a free parameter, feeding the CKMElementScoreCardCert structure that certifies all three mixing angles.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.