ckmParameters
plain-language theorem explainer
The definition fixes the number of independent CKM parameters at four, decomposed as three mixing angles plus one CP-violating phase. Flavor physicists and weak-interaction modelers cite this count when embedding the quark-mixing matrix inside the Recognition Science ledger derivation of SU(2)_L. The entry is introduced by direct assignment of the constant 4, with the decomposition justified by the standard counting of real degrees of freedom in a 3-by-3 unitary matrix.
Claim. The Cabibbo-Kobayashi-Maskawa matrix has four independent real parameters, three mixing angles and one CP phase, so that the parameter count equals $4$.
background
The weak-force module derives SU(2)_L gauge structure from the three-dimensional ledger geometry and chiral couplings from the orientation of the eight-tick cycle. The CKM matrix appears as the description of intergenerational quark mixing required once three generations are present. Upstream phase definitions supply the discrete 8-tick angles $kπ/4$ and the unimodular factors $e^{iw}$ that furnish the complex phase in the mixing matrix.
proof idea
The declaration is a direct constant definition that assigns the natural number 4. No lemmas or tactics are invoked beyond the built-in integer literal.
why it matters
The definition supplies the integer that the downstream theorem ckm_params_3_plus_1 decomposes as $3+1$. It completes the CKM counting step inside the weak-force emergence derivation (P-019). The count connects directly to the eight-tick octave that generates the phases needed for the CP-violating term.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.