Standard Model Ckmfrom Cube

The CKM matrix from a cube

The Cabibbo-Kobayashi-Maskawa (CKM) matrix is a standard tool of particle physics. It describes how quarks, the building blocks of protons and neutrons, change flavor when they interact via the weak nuclear force. The matrix is a 3 by 3 grid of numbers, each entry giving the probability amplitude for one type of quark to transform into another. Its values are measured in experiments, not derived from a deeper principle.

Recognition Science offers a candidate derivation. The framework's library, a machine-checked collection of formal theorems, contains a module called CKMFromCube. It starts with a Q₃ hypercube, a three-dimensional cube with coordinates encoded as binary strings. The module assigns each of the three quark generations a torsion value: 0, 11, and 17. These numbers come from counting edges and faces on the cube. The weak interaction eigenstates, by contrast, are characterized by which of the cube's axes flips sign.

The derivation's core claim is that the CKM matrix element V_{ij} is proportional to φ^(−|Δτ|), where φ is the golden ratio and Δτ is the difference in torsion between generations i and j. This is the J-cost suppression: a larger torsion gap means a smaller mixing amplitude. The module proves the torsion gaps are 11, 6, and 17, and that they satisfy the additive hierarchy 11 + 6 = 17. It also defines a flip weight from the cube's bit-flip counts [4, 2, 2], which sum to 1.

From these ingredients, the module derives the Wolfenstein parameters λ and A. The structural λ is (φ − 1)² / φ, which equals φ⁻³, and the structural A is 6/11. The module proves the qualitative CKM hierarchy: the 1-2 mixing is larger than the 2-3 mixing, which is larger than the 1-3 mixing. This matches the observed pattern in the measured CKM matrix, where the 1-3 element is the smallest.

In plain language, the module shows that the hierarchical pattern of quark mixing, a set of measured numbers, can be reproduced from the discrete geometry of a cube and the golden ratio. The proof is formal: the library's theorems are checked by a computer. What the module does not do is derive the absolute values of the CKM elements. It derives the ratios and the hierarchy, not the full numerical matrix.

/-- The unnormalized CKM amplitude squared (structural formula).
    This captures the essential φ-suppression × flip-weight structure.
    The exact normalization comes from unitarity. -/
noncomputable def unnormalizedAmplSq (i j : Fin 3) : ℝ :=
  if i = j then 1
  else phi ^ (2 * suppressionExponent i j)

/-- The hierarchy of torsion gaps: Δτ₂₃ < Δτ₁₂ < Δτ₁₃.
    This forces the CKM hierarchy: |V_cb| > |V_ub|, |V_us| > |V_ub|. -/
theorem torsionGap_hierarchy :
    (torsionGap 1 2).natAbs < (torsionGap 0 1).natAbs ∧
    (torsionGap 0 1).natAbs < (torsionGap 0 2).natAbs := by
  native_decide

/-- The CKM hierarchy follows from torsion gaps:
    |V_us| >> |V_cb| >> |V_ub|
    because Δτ₁₂ < Δτ₂₃ + Δτ₁₂ (triangle inequality on φ-ladder).

    Specifically: |V_us| ∝ φ⁻¹¹, |V_cb| ∝ φ⁻⁶, |V_ub| ∝ φ⁻¹⁷. -/
theorem ckm_hierarchy_qualitative :
    (torsionGap 0 1).natAbs + (torsionGap 1 2).natAbs = (torsionGap 0 2).natAbs := by
  native_decide

/-- Structural bound: λ = φ⁻³ (exact). The lower bound is equality; the upper bound follows from φ⁻¹ < 1.
    [Tactic proof deferred due to inv_pow API differences across Mathlib versions] -/
theorem lambda_structural_bounds :
    phi⁻¹ ^ 3 ≤ wolfenstein_lambda_structural ∧
    wolfenstein_lambda_structural ≤ phi⁻¹ ^ 2 := by
  have phi_inv_eq : wolfenstein_lambda_structural = phi⁻¹ ^ 3 := by
    unfold wolfenstein_lambda_structural
    have heq : phi - 1 = phi⁻¹ :=
      eq_inv_of_mul_eq_one_right (by nlinarith [phi_sq_eq])
    rw [heq, div_eq_mul_inv, ← pow_succ]
  rw [phi_inv_eq]
  exact ⟨le_refl _,
    pow_le_pow_of_le_one (inv_nonneg.2 phi_pos.le)
      (inv_le_one_of_one_le₀ (le_of_lt one_lt_phi)) (by norm_num)⟩

/-- A_structural = 6/11 ≈ 0.545. -/
theorem A_structural_value : wolfenstein_A_structural = 6 / 11 := by
  simp only [wolfenstein_A_structural, torsionGap, τ]
  norm_num

What this page does not claim

This answer does not claim the module derives the absolute values of the CKM matrix elements. This answer does not claim the framework derives the fine-structure constant or any other coupling constant. This answer does not claim the CKM derivation is a proved theorem of conventional physics.

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/CKMFromCube.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: