IsSignFlip

formal source

 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)⟩
 193
 194/-- The even sign-flip subgroup has order 2^(D-1). -/
 195def even_sign_flip_count (D : ℕ) : ℕ := 2 ^ (D - 1)
 196
 197/-- For D = 3: the even sign-flip subgroup has order 4. -/
 198theorem even_sign_flip_count_D3 : even_sign_flip_count 3 = 4 := by
 199  native_decide
 200
 201/-- **Layer 3**: The parity quotient ℤ/2ℤ.
 202    The quotient of the sign-flip group by the even subgroup.
 203    Order: 2.