Standard Model Ckm Cabibbo Exact Rs

The Cabibbo angle and its status

The Cabibbo angle, named for Nicola Cabibbo's 1963 work, describes the probability that a down-type quark decays into an up-type quark of a different generation. In the Standard Model of particle physics, this mixing is encoded in the CKM matrix, and the Cabibbo angle is the dominant term for first and second generation quarks. Its measured value, from experiments like those at CERN and Fermilab, is approximately 13.04 degrees, corresponding to a sine of about 0.225.

Recognition Science (RS) proposes that physical constants emerge from a single cost function, a measure of the price reality pays for recognizing one state from another. The framework's library, a machine-checked collection of formal theorems, proves that any cost function satisfying five plain conditions must equal J(x) = (x + 1/x)/2 - 1. The module in question, CKM_Cabibbo_Exact_RS, explores whether the Cabibbo angle might follow from this cost function. Its research note suggests a formula: arcsin(J(phi)^(1/2) * phi^(-1)) = arcsin(0.344 * 0.618) = arcsin(0.213), which is close to the measured 0.225 but not exact.

What the module actually proves in Lean is far more limited. It establishes three general facts about the cost function J applied to a ratio m/e: it equals zero when m equals e, it is nonnegative for positive inputs, and a certain threshold phi - 3/2 is positive. These are properties of the cost function itself, not of the Cabibbo angle. The module defines a certificate structure that packages these three facts, and proves that this certificate exists. The docstring is explicit: the module proves nothing specific to the Cabibbo angle, because the cost function is defined without reference to quark masses or the weak force.

The gap between the research note and the formal proof is the gap between a hypothesis and a theorem. For the module to become a theorem about the Cabibbo angle, someone would need to define the quark masses m and e in the framework's own terms, deriving them from the same forcing chain that produces other constants. That step remains open. The near-match of 0.213 versus 0.225 is a prediction with a named falsifier: if the measured value stays at 0.225 with current precision, the formula as written fails.

What the module does establish is a template. It shows how the framework can package a set of cost-function properties into a reusable certificate, ready to be instantiated with subject-specific definitions. The same structure could, in principle, be filled with a real derivation of quark masses. Until then, the Cabibbo angle remains a measured number, not a derived one.

noncomputable def cert : CKMCabiboExactCert where
  cost_at_eq := domainCost_at_eq
  cost_nonneg := domainCost_nonneg
  threshold_pos := canonicalThreshold_pos

theorem domainCost_at_eq (r : ℝ) (h : r ≠ 0) : domainCost r r = 0 := by
  unfold domainCost; rw [div_self h]; exact Jcost_unit0

theorem domainCost_nonneg (m e : ℝ) (hm : 0 < m) (he : 0 < e) : 0 ≤ domainCost m e := by
  unfold domainCost; exact Jcost_nonneg (div_pos hm he)

theorem canonicalThreshold_pos : 0 < canonicalThreshold := by
  unfold canonicalThreshold; linarith [phi_gt_onePointFive]

def domainCost (m e : ℝ) : ℝ := Jcost (m / e)

What this page does not claim

The module does not derive the Cabibbo angle from the cost function. The research note's formula arcsin(0.213) is not a proved theorem. The near-match to 0.225 is not evidence of a derivation, only a hypothesis with a named falsifier.

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/StandardModel/CKM_Cabibbo_Exact_RS.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: