V_us_err
plain-language theorem explainer
V_us_err supplies the one-sigma experimental uncertainty on the CKM matrix element |V_us| as the real number 0.00067. Particle physicists checking geometric predictions for mixing angles against measured values would cite this bound to certify agreement. The declaration is a direct numeric assignment with no reduction or lemmas.
Claim. The experimental uncertainty on the Cabibbo-Kobayashi-Maskawa matrix element $|V_{us}|$ is the real number $0.00067$.
background
The CKMGeometry module formalizes T11, deriving the three CKM angles from cubic ledger geometry and the fine-structure constant. The element |V_us| (theta_12, Cabibbo angle) follows the golden projection formula |V_us| = phi^{-3} - (3/2) alpha, yielding the prediction 0.2251 against the measured central value 0.2250(7). The error bound is the accepted experimental tolerance used to test whether the geometric value lies inside one sigma.
proof idea
This declaration is a direct numeric definition that assigns the literal real number 0.00067. No lemmas are applied and no tactics are invoked.
why it matters
The bound feeds the certification structure CKMElementScoreCardCert and the theorem row_V_us, both of which close the verification that the geometric prediction for |V_us| matches data within tolerance. It completes the T11 loop for the golden projection formula, consistent with the phi-ladder and alpha derivation steps in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.