gauge_order_product
plain-language theorem explainer
The product of the three gauge-layer orders extracted from the 3-cube automorphism group equals the cardinality of the hyperoctahedral group B_3. Researchers tracing the Standard Model gauge factors to cube symmetry would cite the result. The proof rewrites the product via the known order of B_3 and confirms the arithmetic identity by native decision.
Claim. Let the three layers be the axis-permutation layer of order 6, the even-sign-flip subgroup of order 4, and the parity-quotient layer of order 2. Then their product equals the order of the hyperoctahedral group $B_3$ of signed permutations on three coordinates: $6×4×2=48$.
background
The module derives the Standard Model gauge group orders from the automorphism group of the 3-cube Q_3. Its vertices are {0,1}^3 and its automorphism group is the hyperoctahedral group B_3 of order 48, realized as signed permutations: any element permutes the three axes and independently flips their signs. The module decomposes B_3 into three layers whose orders multiply to 48: axis permutations (S_3, order 6), even number of sign flips ((Z/2Z)^2, order 4), and the parity quotient (order 2). Upstream, cube_aut_order states that the cardinality of SignedPerm 3 is exactly 48, obtained by rewriting to the cardinality of the product of S_3 and (Fin 3 → Fin 2).
proof idea
One-line wrapper that applies the upstream theorem cube_aut_order to replace the right-hand side by 48, then invokes native_decide to verify the arithmetic product 6×4×2 equals 48.
why it matters
The declaration closes the discrete-order accounting for the gauge factors inside the cube-symmetry derivation, directly supporting the Gauge-Generation Unification statement recorded in the module: the same Q_3 geometry supplies 3 generations from face-pairs, 3 colors from SU(3) Weyl action, and the (2,1) factors from the sign-flip subgroup and parity quotient. It realizes the explicit three-layer splitting B_3 = (Z/2Z)^3 ⋊ S_3 whose orders multiply to 48, completing the link from cube automorphisms to the discrete skeleton of SU(3)×SU(2)×U(1).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.