Foundation Mass Weak Bases

Two bases, one cube

In the Recognition Science framework, which models physical structure from a discrete record of recognition events, the mass and weak bases are two different ways of labeling the same three generations of quarks. The mass basis groups quarks by how they couple to the framework's cost structure, while the weak basis groups them by how they transform under a gauge symmetry. The CKM matrix, which describes how quarks change flavor in weak interactions, is the change-of-basis matrix between these two labelings.

The framework's library, a machine-checked collection of formal theorems, defines both bases on a three-axis structure called Q₃, an eight-vertex cube. The mass basis assigns each generation an axis based on a flip count: generation 2, with 11 passive edges, prefers axis 0 because it has the most flips (4), while generation 3, with 17 passive subcells, takes axes 1 and 2. The weak basis instead assigns each generation to an even sign-flip generator: generation 1 pairs with σ₂₃, generation 2 with σ₁₃, and generation 3 with σ₁₂. These generators flip two axes at once, and each generation's complement axis labels it in the weak basis.

The key result is the mismatch. Although both bases label the axes identically, the theorem both_bases_label_axes proves the axis assignments coincide, the internal structure differs. Mass states are eigenstates of the J-cost operator weighted by flip counts [4,2,2], while weak states are eigenstates of the even sign-flip generators. This difference in internal structure, even with matching labels, is what forces mixing. The precise CKM elements come from overlap integrals between these differently-structured eigenstates, computed in a separate module.

The module also records structural mixing data: flip counts [4,2,2], torsion values {0,11,17}, face count 6, edge count 12, and a recognition angle θ₀ = arccos(1/4). From these, it derives qualitative predictions: the 1-2 mixing (Cabibbo angle) is largest because the torsion gap 11 is smaller than 17, while the 1-3 mixing (V_ub) is smallest because its gap is largest. The hierarchy |V_ub| << |V_cb| << |V_us| follows from the torsion gap hierarchy. The parameter count matches a 3×3 unitary matrix: three mixing angles and one CP phase.

What this establishes is that the framework's single cube structure, with no free parameters, produces both the mass and weak bases and predicts the observed mixing hierarchy. The mass basis comes from the cost-minimizing coupling structure, the weak basis from the gauge subgroup action, and their mismatch is not an accident but a forced consequence of the geometry.

/-- The mass-basis "preferred axis" for each generation:
    Gen 1 → no preference (ground), Gen 2 → axis 0, Gen 3 → axes {1,2}.

    For the purpose of computing overlaps, we assign Gen 1 the
    "residual axis" not used by the flip-count ordering, which in the
    symmetric (bits 1,2 equal) case gives a democratic combination. -/
def massBasisAxis : Fin 3 → Fin 3
  | ⟨0, _⟩ => 0  -- Gen 1: driven most by axis 0 (4 flips → lightest)
  | ⟨1, _⟩ => 1  -- Gen 2: next
  | ⟨2, _⟩ => 2  -- Gen 3: heaviest generation

/-- The mass basis axis assignment for each generation.

    The assignment is determined by the CW excitation ordering:
    - Gen 1: ground state (no excitation) → coupled to all axes equally
    - Gen 2: edge excitation → preferentially couples to the axis with
      the most flips (axis 0, 4 flips) because it minimizes J-cost
    - Gen 3: face+edge excitation → couples to remaining axes (1,2)

    Concretely: the edge-dressed generation (gen 2) has torsion 11 =
    passive_field_edges. The axis that provides the most "passive edge
    exposure" per cycle is the one flipped most: axis 0 (4 flips).
    The face-dressed generation (gen 3) gets the residual axes.

    This assigns gen1↔ground, gen2↔axis0, gen3↔axes{1,2}. -/
inductive MassBasisAssignment
  | gen1_ground   : MassBasisAssignment
  | gen2_axis0    : MassBasisAssignment
  | gen3_axes12   : MassBasisAssignment
  deriving DecidableEq, Repr

/-- The weak basis assigns each generation to the SU(2) doublet that is
    "most aligned" with the corresponding even sign-flip generator.

    The natural pairing is:
    - Gen 1 (down-type) ↔ σ₂₃ (flips axes 1,2)
    - Gen 2 (charm-type) ↔ σ₁₃ (flips axes 0,2)
    - Gen 3 (top-type) ↔ σ₁₂ (flips axes 0,1)

    This assignment comes from the Weyl group structure: each generator
    acts on the complement of one axis, and the "complement axis" labels
    the generation in the weak basis. -/
inductive WeakBasisAssignment
  | gen1_sigma23 : WeakBasisAssignment  -- complement axis = 0
  | gen2_sigma13 : WeakBasisAssignment  -- complement axis = 1
  | gen3_sigma12 : WeakBasisAssignment  -- complement axis = 2
  deriving DecidableEq, Repr

/-- The mass and weak axis assignments are BOTH the identity for this
    simple axis labeling. The actual mixing comes from the INTERNAL
    structure: the mass states are eigenstates of the J-cost operator
    weighted by flip counts [4,2,2], while the weak states are
    eigenstates of the even-sign-flip generators. These have different
    internal structure even when the axis labels coincide.

    The precise CKM matrix elements come from the overlap integrals
    between these differently-structured eigenstates (see CKMFromCube). -/
theorem both_bases_label_axes : ∀ i, massBasisAxis i = weakBasisAxis i := by
  intro i; fin_cases i <;> rfl

/-- 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

This module does not compute the numerical CKM matrix elements. The axis labels coinciding does not mean the bases are the same; the internal structure differs. The framework does not derive the fine-structure constant or other Standard Model couplings here.

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: