weakComplement_is_identity
plain-language theorem explainer
On the three spatial axes indexing generation space, the weak-basis complement map is the identity: generation i is assigned complement axis i. Anyone building the weak eigenstates from even sign-flip generators on the cube will cite this. The proof is exhaustive case analysis on Fin 3 followed by definitional equality.
Claim. For every axis index $i \in \{0,1,2\}$, the weak complement axis of $i$ equals $i$. Equivalently, the map sending each weak-basis generation to the axis not flipped by its even sign-flip generator is the identity on the three axes.
background
The module constructs two orthonormal bases on the three-dimensional generation space whose overlap is the CKM matrix. Mass eigenstates come from the CW filtration and torsion rungs ${0,11,17}$ on the $\varphi$-ladder. Weak eigenstates come from the SU(2) gauge subgroup realized as even sign flips on the cube $Q_3$ (GaugeFromCube Layer 2).
Each even flip generator $\sigma_{jk}$ flips two axes and leaves one fixed. The weak complement axis of a generation is defined to be that unflipped axis: $\sigma_{23}$ leaves axis 0, $\sigma_{13}$ leaves axis 1, $\sigma_{12}$ leaves axis 2. By that case table the assignment is already the identity map $\mathrm{Fin},3\to\mathrm{Fin},3$.
This lemma records that definitional fact so later mismatch and mixing-angle constructions can rewrite freely between generation labels and complement axes.
proof idea
Introduce $i:\mathrm{Fin},3$. Split into the three concrete values with fin_cases. On each branch the definition of the complement map returns the same numeral, so rfl closes. No external lemmas are required; the result is pure definitional unfolding of a three-line pattern match.
why it matters
The module's main narrative is that mass and weak bases assign different roles to the three axes, and that mismatch is the geometric origin of CKM mixing. The weak side of that story needs a clean identification of each generation with the axis fixed by its even flip. Establishing that the complement assignment is the identity removes bookkeeping noise before weakBasisAxis, both_bases_label_axes, and MixingAngleData compare the two decompositions of $\mathbb{C}^8$.
In the broader RS chain this sits under the eight-tick / $D=3$ cube geometry (T7–T8) and the gauge-from-cube construction: SU(2) acts by even sign flips, while the mass basis follows CW dimension and torsion. No downstream theorem currently depends on this lemma (used-by count is zero), so it is local scaffolding for the basis-mismatch section rather than a cited forcing-chain step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.