IsAxisPermutation

formal source

 159/-- **Layer 1**: The axis permutation subgroup S₃.
 160    Permutations of the 3 coordinate axes, with all signs positive.
 161    This corresponds to the color permutation group. -/
 162def IsAxisPermutation {D : ℕ} (g : SignedPerm D) : Prop :=
 163  ∀ i, g.signs i = 0
 164
 165/-- The number of axis permutations is D! (= 6 for D = 3). -/
 166def axis_perm_count (D : ℕ) : ℕ := Nat.factorial D
 167
 168theorem axis_perm_count_D3 : axis_perm_count 3 = 6 := by native_decide
 169
 170/-- **Layer 2**: The sign-flip subgroup (ℤ/2ℤ)^D.
 171    Sign flips of individual coordinates, with identity permutation.
 172    Order: 2^D (= 8 for D = 3). -/
 173def IsSignFlip {D : ℕ} (g : SignedPerm D) : Prop :=
 174  g.perm = Equiv.refl _
 175
 176/-- The number of sign flips is 2^D (= 8 for D = 3). -/
 177def sign_flip_count (D : ℕ) : ℕ := 2 ^ D
 178
 179theorem sign_flip_count_D3 : sign_flip_count 3 = 8 := by native_decide
 180
 181/-- **Layer 2a**: The EVEN sign-flip subgroup.
 182    Sign flips that flip an EVEN number of coordinates.
 183    Elements: {(0,0,0), (1,1,0), (1,0,1), (0,1,1)} for D = 3.
 184    Order: 2^(D-1) (= 4 for D = 3).
 185
 186    This subgroup corresponds to the SU(2) weak isospin structure. -/
 187def IsEvenSignFlip {D : ℕ} (g : SignedPerm D) : Prop :=
 188  IsSignFlip g ∧ Even (∑ i : Fin D, (g.signs i).val)
 189
 190/-- The parity of a sign-flip element: the total number of flipped signs mod 2. -/
 191def sign_parity {D : ℕ} (g : SignedPerm D) : Fin 2 :=
 192  ⟨(∑ i : Fin D, (g.signs i).val) % 2, Nat.mod_lt _ (by norm_num)⟩