Foundation Mass Weak Bases Cabibbo Largest Angle

The Cabibbo angle ranking

The Cabibbo angle is the largest of the three quark mixing angles in the Standard Model of particle physics. It measures how strongly the first and second generations of quarks mix through the weak force, and its measured value is about 13 degrees. The other two angles are smaller: the one between the second and third generations is about 2.4 degrees, and the one between the first and third is below 0.2 degrees. This hierarchy, where the 1-2 mixing dominates, is a well-known empirical pattern.

Recognition Science (RS) attempts to derive this pattern from a discrete structure called Q₃, a three-axis generation space. The framework's library, a machine-checked collection of formal theorems, contains a declaration named cabibbo_largest_angle. Its statement is simple: the natural number 11 is less than 17. The theorem proves this inequality, and through the framework's interpretation, it establishes that the torsion gap between generations 1 and 2 is smaller than the gap between generations 1 and 3. A smaller torsion gap is claimed to correspond to a larger overlap and therefore a larger mixing angle.

The theorem does not compute the Cabibbo angle's value, nor does it derive the full CKM matrix. It only establishes a qualitative ordering: the 1-2 mixing is largest because its torsion gap of 11 is smaller than the 1-3 gap of 17. The framework's docstring states this reasoning, and the theorem's proof is a trivial arithmetic fact. The actual mixing angles are said to emerge from overlap integrals between eigenstates, but those calculations are not part of this declaration.

What the theorem does provide is a structural explanation for a known hierarchy. It shows that within the RS framework, the largest mixing angle corresponds to the smallest torsion gap. This is a consistency check, not a prediction. The framework models the mass and weak bases as different decompositions of the same Q₃ space, and the mismatch between them is claimed to be the origin of the CKM matrix. The declaration supports the qualitative claim that the 1-2 angle is largest, but it does not quantify any angle.

The declaration also does not address the other two mixing angles' relative sizes beyond the 1-3 angle being smallest. The theorem vub_smallest separately establishes that 17 is greater than 11 and 6, which the framework interprets as the 1-3 mixing being smallest. The cabibbo_largest_angle theorem alone only covers the 1-2 versus 1-3 comparison. The full hierarchy, including the 2-3 angle, requires additional declarations and is not established by this single theorem.

/-- The 1-2 mixing (Cabibbo angle) is the largest because the flip-count
    difference |4 - 2| = 2 between axes 0 and 1 is the same as between
    0 and 2, but the torsion gap Δτ₁₂ = 11 is smaller than Δτ₁₃ = 17.
    Smaller torsion gap → larger overlap → larger mixing angle. -/
theorem cabibbo_largest_angle :
    (11 : ℤ).natAbs < (17 : ℤ).natAbs := by norm_num

/-- The 1-2 mixing (Cabibbo angle) is the largest because the flip-count
    difference |4 - 2| = 2 between axes 0 and 1 is the same as between
    0 and 2, but the torsion gap Δτ₁₂ = 11 is smaller than Δτ₁₃ = 17.
    Smaller torsion gap → larger overlap → larger mixing angle. -/
theorem cabibbo_largest_angle :
    (11 : ℤ).natAbs < (17 : ℤ).natAbs := by norm_num

What this page does not claim

The declaration does not compute the numerical value of the Cabibbo angle. The declaration does not derive the full CKM matrix. The declaration does not establish the relative size of the 2-3 mixing angle.

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/Foundation/MassWeakBases.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: