cube_edge_count

formal source

 106  rw [cube_vertex_count]; norm_num
 107
 108/-- Number of edges of the D-cube: D · 2^(D-1). -/
 109def cube_edge_count (D : ℕ) : ℕ := D * 2 ^ (D - 1)
 110
 111/-- For D = 3: 12 edges. -/
 112theorem cube3_edge_count : cube_edge_count 3 = 12 := by
 113  native_decide
 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⟩