SignedPerm
SignedPerm D encodes the hyperoctahedral group B_D as a permutation of Fin D together with an independent sign flip on each coordinate. Researchers deriving the Standard Model gauge group from the 3-cube automorphism group cite this structure to isolate the S_3 layer for SU(3) and the even-sign-flip subgroup for SU(2) x U(1). The definition is a direct product equipped with a Fintype instance obtained by equivalence to the product of permutations and sign maps.
claimA signed permutation on $D$ coordinates is a pair consisting of a permutation $σ$ of the set $Fin D$ and a sign map $ε : Fin D → {0,1}$ (representing $+1$ or $-1$). The group acts on vectors in $ℤ^D$ by $x ↦ (ε_1 x_{σ(1)}, …, ε_D x_{σ(D)})$. This realizes the hyperoctahedral group $B_D$ of order $2^D D!$.
background
Module GaugeFromCube derives the Standard Model gauge group SU(3) × SU(2) × U(1) from the automorphism group of the 3-cube Q_3. SignedPerm D supplies the concrete group object B_D whose three-layer decomposition (axis permutations, even sign flips, and full sign flips) maps onto the gauge factors. The module doc-comment states that B_3 = (ℤ/2ℤ)^3 ⋊ S_3 has order 48 and acts on ℤ^3 by signed permutations of the coordinate axes.
proof idea
The structure is introduced with fields perm : Equiv.Perm (Fin D) and signs : Fin D → Fin 2, deriving DecidableEq. The Fintype instance is a one-line wrapper that applies Fintype.ofEquiv to the product Equiv.Perm (Fin D) × (Fin D → Fin 2), supplying explicit toFun, invFun, and identity left/right inverses.
why it matters in Recognition Science
This definition supplies the group object used by downstream results cube_aut_order (which proves |SignedPerm 3| = 48) and gauge_group_certificate (which certifies the SM gauge ranks (3,2,1) from the cube). It fills the P-014 step by providing the hyperoctahedral group whose S_3 layer yields the color structure and whose even-sign-flip subgroup yields the weak-isospin structure, consistent with D = 3 spatial dimensions.
scope and limits
- Does not compute the cardinality of SignedPerm D.
- Does not establish any isomorphism to SU(3) × SU(2) × U(1).
- Does not define the action on fermion or gauge fields.
- Does not address the embedding of the layers into the gauge algebra.
formal statement (Lean)
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) :=
proof body
Definition body.
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!. -/