CKMElementScoreCardCert
plain-language theorem explainer
This structure bundles the three one-sigma inequalities |V_us_pred - V_us_exp| < V_us_err, |V_cb_pred - V_cb_exp| < V_cb_err and |V_ub_pred - V_ub_exp| < V_ub_err together with the geometric equalities that define the predictions. A flavor physicist or model builder checking Recognition Science against PDG data would cite the certificate when verifying consistency of the phi-ladder CKM magnitudes. The definition is a plain structure that packages the six relations with no additional proof obligations.
Claim. The structure consists of the three inequalities $|V_{us}^{pred}-V_{us}^{exp}|<V_{us}^{err}$, $|V_{cb}^{pred}-V_{cb}^{exp}|<V_{cb}^{err}$, $|V_{ub}^{pred}-V_{ub}^{exp}|<V_{ub}^{err}$ together with the identifications $V_{us}^{pred}=$ torsion overlap minus Cabibbo radiative correction, $V_{cb}^{pred}=$ edge dual ratio, and $V_{ub}^{pred}=$ fine structure leakage, where the error bounds are the constants $V_{us}^{err}=0.00035$, $V_{cb}^{err}=0.00085$, $V_{ub}^{err}=0.00011$ and the experimental central values are $V_{us}^{exp}=0.22500$, $V_{cb}^{exp}=0.04182$, $V_{ub}^{exp}=0.00369$.
background
The module implements Phase 2 of the Recognition Science program for CKM magnitudes. It imports the geometric predictions from CKMGeometry, where V_cb_pred is defined as the inverse of twice the total edge count (1/24), V_ub_pred as half the fine-structure constant, and V_us_pred as the golden projection minus a radiative correction. The experimental anchors and one-sigma bands are supplied as the constants V_us_err, V_cb_err, V_ub_err and the corresponding exp values. The local falsifier is any PDG update that pushes one of the three elements outside its certified 1-sigma band while keeping the fixed alpha and phi inputs.
proof idea
The declaration is a structure definition with no proof body. It simply declares the six fields that must be supplied to inhabit the type. The downstream theorem ckmElementScoreCardCert_holds populates the structure by applying the three row lemmas row_V_us, row_V_cb, row_V_ub for the inequalities and the three equality lemmas row_vus_eq_geometry, row_vcb_eq_geometry, row_vub_eq_leakage for the geometric identifications.
why it matters
The structure supplies the concrete certificate required by ckmElementScoreCardCert_holds, thereby closing the P2-CKM row of the Recognition Science program. It realizes the geometric predictions V_cb_pred = 1/24 and V_ub_pred = alpha/2 that descend from the cube geometry and the phi-ladder fixed point. The construction remains partial because Wolfenstein parameters and the full CKMExact treatment are handled in separate modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.