ckmDimension
plain-language theorem explainer
CKM dimension is set to the natural number 3, matching the three quark generations whose mixing is governed by a unitary matrix. Physicists deriving weak interaction predictions or counting independent CKM parameters (three angles plus one phase) would reference this value. The definition is a direct constant assignment with no computation or lemmas.
Claim. The Cabibbo-Kobayashi-Maskawa matrix is a $3 times 3$ unitary matrix.
background
The module derives the weak nuclear force from ledger geometry in Recognition Science, producing SU(2)_L symmetry with three generators, chiral left-handed couplings from the eight-tick cycle orientation, and massive W and Z bosons. One listed prediction is that the CKM matrix describes quark mixing. Upstream definitions supply supporting structures: the eight-tick phase (periodic with period 2 pi) for orientation and chirality, independent spatial semantics for voxel evolution without neighbor coupling, and independent coupled axes for distinct primitives.
proof idea
Direct definition that assigns the constant natural number 3. No lemmas or tactics are invoked; the body is a simple equality to the numeral three.
why it matters
The definition supplies the dimension required for the CKM matrix prediction listed in the weak force emergence derivation. It is consistent with the three spatial dimensions forced by the T8 step of the unified forcing chain. The entry closes a small gap in the module's enumeration of weak-interaction observables while leaving open how the three generations themselves arise from the phi-ladder or eight-tick structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.