ckm_parameter_count
plain-language theorem explainer
Three generations yield three CKM mixing angles and one physical CP phase, the standard count for a 3×3 unitary with unphysical phase freedom. Cite when tying RS generation geometry on the cube to CKM parameter counting. Proof is a two-goal arithmetic check: face-pair count is definitional, and the phase formula evaluates by norm_num.
Claim. The number of opposite-face pairs on the $3$-cube equals $3$, and a $3\times 3$ unitary mixing matrix has $(3-1)(3-2)/2 = 1$ physical CP-violating phase.
background
The module MassWeakBases builds the two orthonormal bases on generation space whose overlap is the CKM matrix: mass eigenstates from CW-level coupling and torsion rungs, and weak eigenstates from the SU(2) even sign-flip action on the cube. Their mismatch forces mixing.
Upstream, face_pairs D is defined simply as $D$: on a $D$-cube, opposite faces come in exactly $D$ pairs. For $D=3$ that is three pairs, matching three generation axes.
The second conjunct is the textbook CKM phase count: an $N\times N$ unitary has $(N-1)(N-2)/2$ physical CP phases after removing unphysical rephasing freedom. Here $N=3$ gives one phase.
proof idea
Tactic proof by constructor on the conjunction. Left goal: face_pairs 3 = 3 closes by rfl because face_pairs is the identity on $\mathbb{N}$. Right goal: $(3-1)(3-2)/2 = 1$ closes by norm_num. No lemmas beyond the definition of face pairs.
why it matters
Records the classical CKM parameter census inside the RS mass/weak-basis story: three generations (three face-pair axes on $Q_3$) give three mixing angles and one CP phase. The module frames CKM as the change-of-basis between CW/torsion mass axes and SU(2) even-flip weak axes; this theorem pins the expected parameter count before any angle magnitudes are derived.
It sits with siblings such as MixingAngleData and axis-mismatch results that force nontrivial overlap. No downstream consumers are wired yet. Framework link: three generations and $D=3$ spatial structure (forcing chain T7–T8) make the $N=3$ count the only relevant case.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.