ckmElementScoreCardCert_holds
plain-language theorem explainer
The declaration certifies existence of a score card structure confirming that Recognition Science geometric predictions for the leading CKM magnitudes match PDG-style experimental values inside one-sigma error bands. Flavor physicists checking cube-geometry derivations against mixing data would cite the result when validating the Phase 2 P2-CKM predictions. The proof constructs the required record by direct substitution of the three matching theorems and three geometric derivation theorems.
Claim. There exists a certificate structure $C$ such that $|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 geometric identities $V_{us}^{pred}=$ torsion overlap minus Cabibbo radiative correction, $V_{cb}^{pred}=$ edge dual ratio, and $V_{ub}^{pred}=$ fine structure leakage.
background
The CKMElementScoreCard module assembles a certificate structure whose fields are three absolute-difference inequalities and three geometric equalities for the leading CKM elements. Module documentation states the Recognition Science predictions $V_{us}^{pred}=φ^{-3}-(3/2)α$, $V_{cb}^{pred}=1/24$, $V_{ub}^{pred}=α/2$ together with PDG-style experimental central values and 1-sigma bands; the falsifier is any future PDG update that pushes one of the three elements outside its certified inequality. Upstream theorems supply the concrete bounds (row_V_us, row_V_cb, row_V_ub) and the geometric derivations (row_vus_eq_geometry, row_vcb_eq_geometry, row_vub_eq_leakage).
proof idea
The proof is a term-mode record construction that populates the six fields of CKMElementScoreCardCert by direct reference to the six upstream row theorems: row_V_us supplies the V_us inequality, row_vus_eq_geometry supplies the corresponding geometric equality, and likewise for the cb and ub pairs.
why it matters
The theorem discharges the PARTIAL_THEOREM status recorded in the module documentation for the sigma matches of the leading CKM magnitudes. It thereby certifies the cube-geometry predictions inside the Recognition Science Phase 2 P2-CKM row and supplies the concrete witness required by the certificate structure. No downstream consumers are recorded, leaving open the question of how the certified elements will be packaged into higher-level Wolfenstein or CKMExact statements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.