Verification Ckmcert

The CKM certificate

The CKM matrix describes how quarks change flavor through the weak force, a standard piece of particle physics. The CKM matrix is a 3 by 3 table of complex numbers whose entries control the probability of transitions between quark generations. Physicists measure these entries in experiments and check that they satisfy unitarity, meaning the rows and columns behave like a proper rotation in complex space.

In Recognition Science, the framework models quark mixing as a geometric consequence of cube edges, not as free parameters. The module called ckmcert is a machine-checked certificate: a single object that packages the framework's experimentally checkable CKM claims. It mirrors a similar certificate for the neutrino sector, bundling the relevant statements so a verifier can inspect them as one unit.

The certificate contains eight components. Four of them assert that specific CKM entries, V_cb, V_ub, and V_us, match measured values. The other four assert bounds on the CP-violating phase alpha and on phi_inv3, a framework-internal constant related to the golden ratio. The certificate does not prove these values; it packages them as claims that experiments can confirm or refute.

What this establishes in plain language is a hard-falsifiable target. The framework says: if you measure the CKM parameters and they fall outside these bounds, the geometric origin story is wrong. The certificate makes that bet explicit and machine-checkable, so the comparison against experimental data is a genuine test, not a loose analogy.

structure Cert where
  -- V_cb: pure cube topology + PDG match
  vcb_geometric_origin : V_cb_geom = 1 / (2 * cube_edges 3)
  vcb_match : abs (V_cb_pred - V_cb_exp) < V_cb_err

  -- α bounds (proved from interval certificate)
  alpha_lower_bound : (0.00729 : ℝ) < alpha
  alpha_upper_bound : alpha < (0.00731 : ℝ)

  -- φ^(-3) bounds (needed for Cabibbo)
  phi_inv3_lower_bound : (0.2360 : ℝ) < phi ^ (-3 : ℤ)
  phi_inv3_upper_bound : phi ^ (-3 : ℤ) < (0.2361 : ℝ)

  -- V_ub / V_us: PDG matches
  vub_match : abs (V_ub_pred - V_ub_exp) < V_ub_err
  vus_match : abs (V_us_pred - V_us_exp) < V_us_err

def cert : Cert where
  vcb_geometric_origin := V_cb_from_cube_edges
  vcb_match := V_cb_match
  alpha_lower_bound := CKMGeometry.alpha_lower_bound
  alpha_upper_bound := CKMGeometry.alpha_upper_bound
  phi_inv3_lower_bound := CKMGeometry.phi_inv3_lower_bound
  phi_inv3_upper_bound := CKMGeometry.phi_inv3_upper_bound
  vub_match := V_ub_match
  vus_match := V_us_match

What this page does not claim

The certificate does not prove that the CKM entries equal the measured values; it packages them as falsifiable claims. The framework's geometric origin for V_cb is not derived in this module; it is assumed as input.

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/Verification/CKMCert.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: