SignedPerm

formal source

 128    This is the hyperoctahedral group B_D, the automorphism group of the
 129    D-cube. It acts on ℤ^D by x ↦ (ε₁ · x_{σ(1)}, ..., ε_D · x_{σ(D)})
 130    where σ ∈ S_D is the permutation and εᵢ ∈ {±1} are the signs. -/
 131structure SignedPerm (D : ℕ) where
 132  perm : Equiv.Perm (Fin D)
 133  signs : Fin D → Fin 2
 134  deriving DecidableEq
 135
 136instance (D : ℕ) : Fintype (SignedPerm D) :=
 137  Fintype.ofEquiv (Equiv.Perm (Fin D) × (Fin D → Fin 2))
 138    { toFun := fun ⟨p, s⟩ => ⟨p, s⟩
 139      invFun := fun ⟨p, s⟩ => ⟨p, s⟩
 140      left_inv := fun ⟨_, _⟩ => rfl
 141      right_inv := fun ⟨_, _⟩ => rfl }
 142
 143/-- The order of the hyperoctahedral group B_D is 2^D · D!. -/
 144theorem signed_perm_card (D : ℕ) :
 145    Fintype.card (SignedPerm D) = 2 ^ D * Nat.factorial D := by
 146  rw [Fintype.ofEquiv_card]
 147  simp [SignedPerm, Fintype.card_prod,
 148        Fintype.card_perm, Fintype.card_fun, Fintype.card_fin]
 149  ring
 150
 151/-- **THEOREM**: |Aut(Q₃)| = |B₃| = 48.
 152    The automorphism group of the 3-cube has order 48. -/
 153theorem cube_aut_order : Fintype.card (SignedPerm 3) = 48 := by
 154  rw [signed_perm_card]
 155  norm_num
 156
 157/-! ## Part 3: The Three-Layer Decomposition -/
 158
 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. -/