evenFlipGenerator
plain-language theorem explainer
Defines the three independent even sign-flip generators on the 3-cube Q₃: each index in {0,1,2} selects a pair of axes to flip simultaneously. Anyone building the weak eigenbasis from the SU(2) gauge action on cube vertices will cite this table. The body is a pure case split on the generator index, returning a Boolean mask on the three axes.
Claim. A map $g \mapsto m_g$ from generator labels $g \in \{0,1,2\}$ to Boolean masks $m_g : \{0,1,2\} \to \{\mathrm{true},\mathrm{false}\}$ on the three spatial axes of $Q_3$, with $m_0$ true exactly on axes $\{0,1\}$, $m_1$ true exactly on $\{0,2\}$, and $m_2$ true exactly on $\{1,2\}$. Each mask therefore flips exactly two axes (an even sign flip).
background
The module constructs two orthonormal bases on the three-generation space whose overlap is the CKM matrix. Mass eigenstates come from the CW filtration and torsion rungs on the φ-ladder. Weak eigenstates come from the SU(2) gauge subgroup action realized as even sign flips on the vertices of the 3-cube $Q_3$ (the Layer-2 gauge structure from GaugeFromCube).
An even sign flip means flipping exactly two coordinate bits at once, preserving the parity of the Hamming weight. The three independent such generators are the natural basis for that SU(2) action on vertex states. Downstream, each generator is turned into a concrete XOR mask on Fin 8 vertex labels.
Upstream flip is the single-bit Gray-code tick on a face configuration; the present table packages the two-bit (even) analogues needed for the weak basis rather than the eight-tick traversal.
proof idea
Pure definition by cases on Fin 3. Index 0 returns the predicate true on axes 0 and 1; index 1 on axes 0 and 2; index 2 on axes 1 and 2. No lemmas are invoked; the body is the lookup table itself.
why it matters
This table is the combinatorial seed of the weak basis in Recognition Science. It is consumed immediately by evenFlipOnVertex, which builds the XOR mask (if axes 0 then 1 else 0) + (if axes 1 then 2 else 0) + (if axes 2 then 4 else 0) and applies it to any vertex in Fin 8.
That action supplies the SU(2) irrep structure whose eigenaxes are compared with the mass-basis axes (massBasisAxis / weakBasisAxis). The documented mismatch between those axis assignments forces nontrivial mixing and feeds MixingAngleData, the structured CKM overlap data of the module.
In the broader framework this sits under the eight-tick / $D=3$ cube geometry (T7–T8): the same $Q_3$ that carries the octave also carries the even-flip SU(2) that defines weak eigenstates, so mass–weak mismatch is forced by two different decompositions of $\mathbb{C}^8$ rather than by an external Yukawa sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.