row_V_cb
plain-language theorem explainer
The declaration certifies that the Recognition Science geometric prediction for the CKM element V_cb lies inside the experimental 1-sigma band. Flavor physicists checking geometric models of quark mixing against PDG data would cite the result when assembling certified scorecards. The proof is a one-line wrapper that directly invokes the matching theorem V_cb_match.
Claim. $|V_{cb}^{pred} - V_{cb}^{exp}| < V_{cb}^{err}$, where $V_{cb}^{pred} = 1/24$ is the geometric prediction, $V_{cb}^{exp} = 0.04182$ is the observed value, and $V_{cb}^{err} = 0.00085$ is the 1-sigma uncertainty.
background
In the CKMElementScoreCard module the row_V_cb theorem records the match for the leading CKM magnitude V_cb under Phase 2 P2-CKM. Recognition Science supplies the prediction V_cb_pred as the inverse of twice the total edge count in the cube geometry, giving exactly 1/24. The experimental inputs are the fixed PDG-style values V_cb_exp = 0.04182 and V_cb_err = 0.00085 taken from the sibling CKMGeometry module.
proof idea
The proof is a one-line wrapper that applies the theorem V_cb_match from CKMGeometry. No further tactics or reductions are performed.
why it matters
row_V_cb supplies the certified V_cb entry inside ckmElementScoreCardCert_holds, which assembles the full scorecard for the three leading CKM magnitudes. It completes the geometric-prediction step of the P2-CKM phase, where V_cb_pred is fixed by the cube geometry using the golden ratio phi and the fine-structure constant alpha. The module falsifier is any PDG update that drives |V_pred - V_exp| outside the 1-sigma band while alpha and phi remain fixed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.