sign_parity
plain-language theorem explainer
sign_parity extracts the parity of sign flips for any signed permutation on D coordinates by summing the indicator values modulo 2. Gauge derivations from hyperoctahedral groups reference it when isolating the even-flip kernel that supplies the (Z/2Z)^{D-1} factor for SU(2) × U(1) at D=3. The definition performs the finite sum over Fin D and reduces modulo 2, with an immediate numerical bound to land in Fin 2.
Claim. For a signed permutation $g$ on $D$ coordinates (a permutation of the axes together with a sign assignment $s :$ Fin $D$ to Fin 2), the parity is the element of Fin 2 given by $((∑_i s(i)) mod 2)$.
background
The module derives SU(3) × SU(2) × U(1) from the automorphism group B_3 of the 3-cube Q_3. SignedPerm D encodes the hyperoctahedral group B_D, which acts on Z^D by signed coordinate permutations: each element consists of an axis permutation in S_D together with an independent sign flip for each coordinate. The parity map is the homomorphism ε : (Z/2Z)^D → Z/2Z whose kernel is the even sign-flip subgroup of order 2^{D-1}.
proof idea
This is a direct definition that builds the Fin 2 element from the sum of the sign values modulo 2. It applies summation over the finite index set Fin D and uses Nat.mod_lt with a norm_num tactic to certify that the remainder lies strictly below 2.
why it matters
The definition supplies the parity homomorphism needed to carve out the even sign-flip subgroup inside B_D. For D=3 this subgroup is isomorphic to (Z/2Z)^2 and furnishes the Weyl-group layer for SU(2) × U(1), completing the three-layer decomposition of the cube automorphism group that already accounts for the S_3 factor of SU(3). It therefore closes the algebraic step that extracts the full discrete gauge structure from cube symmetry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.