Q3_aut_order_eq
plain-language theorem explainer
The equality establishes that the automorphism group order of the three-dimensional hypercube equals 3! times 2 to the power 3. Researchers modeling lattice symmetries or spectral corrections in Recognition Science cite this when bounding configuration counts under the Q3 unit cell. The proof is a one-line wrapper that unfolds the two definitions and applies native decision to verify the numerical match.
Claim. The order of the automorphism group of the 3-cube satisfies $|Aut(Q_3)| = 3! · 2^3$.
background
The CubeSpectrum module formalizes combinatorial and spectral properties of the 3-cube Q3, the unit cell of Z^3, which has 8 vertices, 12 edges and 6 faces. Its graph Laplacian eigenvalues are {0, 2, 2, 2, 4, 4, 4, 6} and its automorphism group is S4 × Z2^3 of order 48. Q3_degree is the constant 3; Q3_aut_order is the constant 48, presented as the concrete instance of the general formula |Aut(Q_D)| = D! · 2^D for the semidirect product S_D ⋊ Z2^D.
proof idea
The proof is a one-line wrapper that unfolds Q3_aut_order and Q3_degree, then invokes native_decide to confirm the numerical identity 48 = 6 · 8.
why it matters
This supplies the explicit symmetry factor used for configuration reduction in the eta2 correction inside the CubeSpectrum module. It instantiates the general Aut(Q_D) formula that appears in the upstream SpectralEmergence result proving aut_order 3 = 48, and supports the spectral formalism for the Z^3 unit cell that underpins critical-exponent corrections in Recognition Science.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.