pith. sign in
module module high

IndisputableMonolith.Mathematics.CubicSymmetryGroupFromRS

show as:
view Lean formalization →

The module establishes the order of the cubic symmetry group B3 as 48 when the spatial dimension is fixed at three, matching the formula 2^D times D factorial. It supplies supporting definitions for hyperoctahedral orders and rank decompositions used in symmetry analysis. Researchers working on discrete symmetries within Recognition Science cite these objects to anchor the D=3 case from the forcing chain. The module consists of direct definitions and equality verifications.

claim$|B_3| = 2^D D! $ at $D=3$, with the hyperoctahedral group in three dimensions and associated rank decomposition functions.

background

Recognition Science fixes the number of spatial dimensions at three via the eight-tick octave in the unified forcing chain. This module introduces the cubic symmetry group B3, identified as the hyperoctahedral group whose order is given by twice the dimension factorial. It also defines rank decomposition functions that break down group elements according to their coordinate actions. The setting assumes standard group theory from the imported Mathlib library.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the symmetry group order required for the D=3 case in the Recognition Science framework. It supports parent results on the eight-tick octave and downstream applications to mass ladders by providing the discrete symmetry structure. The order 48 aligns with the hyperoctahedral group acting on three-dimensional space.

scope and limits

declarations in this module (9)