cube_face_count

formal source

 114
 115/-- Number of faces (2-cells) of the D-cube: 2D.
 116    Equivalently: D pairs of opposite faces, each pair contributing 2 faces. -/
 117def cube_face_count (D : ℕ) : ℕ := 2 * D
 118
 119/-- For D = 3: 6 faces. -/
 120theorem cube3_face_count : cube_face_count 3 = 6 := by
 121  native_decide
 122
 123/-! ## Part 2: The Hyperoctahedral Group B₃ -/
 124
 125/-- A signed permutation on D coordinates: a permutation of Fin D together
 126    with a sign assignment (each coordinate can be flipped or not).
 127
 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,