Physics Ckmelement Score Card

The CKM element score card

The CKM matrix is the standard model's table of probabilities for quarks changing flavor through the weak force. Its elements are measured quantities, not derived from first principles in conventional physics. The three largest off-diagonal magnitudes are |V_us|, |V_cb|, and |V_ub|, which control strange, charm, and bottom quark transitions respectively. Their measured values, in the Particle Data Group style, are 0.22500, 0.04182, and 0.00369, each with a 1-sigma error band.

In Recognition Science, the framework's library (a machine-checked collection of formal theorems) defines geometric quantities that predict these three magnitudes. The prediction for |V_us| is the difference between a torsion overlap and a radiative correction, for |V_cb| it is an edge dual ratio, and for |V_ub| it is a fine-structure leakage. Each prediction lands inside the measured 1-sigma interval, and the library proves this with formal theorems: the absolute difference between predicted and observed value is strictly less than the error for each element.

The module assembles these three row proofs into a single certificate structure. The certificate holds all six facts: the three inequalities against experiment and the three geometric equalities. The library proves the certificate is nonempty, meaning the whole score card is certified at once. The status is a partial theorem: the sigma matches are proved, but the Wolfenstein packings and high-level CKM exact parameters remain separate, unformalized rows.

The falsifier is concrete: a PDG update where any of the three elements leaves the proved 1-sigma inequality false, with fixed certified alpha and phi inputs, would refute the corresponding geometric prediction. This is not a claim that the CKM matrix is fully derived; it is a certified score card for three leading magnitudes, each within its measured error band, with the geometric identification made explicit and machine-checked.

theorem row_V_us : abs (V_us_pred - V_us_exp) < V_us_err := V_us_match

theorem row_V_cb : abs (V_cb_pred - V_cb_exp) < V_cb_err := V_cb_match

theorem row_V_ub : abs (V_ub_pred - V_ub_exp) < V_ub_err := V_ub_match

theorem ckmElementScoreCardCert_holds : Nonempty CKMElementScoreCardCert :=
  ⟨{ vus := row_V_us
     vcb := row_V_cb
     vub := row_V_ub
     vus_geo := row_vus_eq_geometry
     vcb_geo := row_vcb_eq_geometry
     vub_geo := row_vub_eq_leakage }⟩

theorem row_vus_eq_geometry : V_us_pred = torsion_overlap - cabibbo_radiative_correction :=
  vus_derived

theorem row_vcb_eq_geometry : V_cb_pred = edge_dual_ratio := vcb_derived

theorem row_vub_eq_leakage : V_ub_pred = fine_structure_leakage := vub_derived

What this page does not claim

This does not claim the CKM matrix is fully derived or that all elements are predicted. This does not claim the geometric predictions are derived from the forcing chain; they are definitional identifications. This does not claim the measured values are framework-derived; they are external experimental inputs.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Physics/CKMElementScoreCard.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: