IndisputableMonolith.Mathematics.CubicSymmetryGroupFromRS
This module derives the order of the B3 cubic symmetry group as 48, matching 2^D * D! at D=3 from Recognition Science. Researchers linking the forcing chain to discrete symmetries would cite these results. The module assembles combinatorial lemmas on hyperoctahedral orders and rank decompositions to reach the equality.
claim$|B_3| = 2^D imes D! ext{ at } D=3$
background
Recognition Science forces D=3 spatial dimensions via T8 in the unified forcing chain. This module translates that constraint into the order of the hyperoctahedral group B3, also called the cubic symmetry group.
It introduces supporting definitions including b3Order for group cardinality, hyperoctahedralOrder, rankDecomposition, rank_sum, rank_length, and CubicSymmetryCert as a certificate object. The single import is Mathlib for group-theoretic primitives.
proof idea
This is a definition module containing lemmas rather than one central proof. It builds the result through a sequence of definitions (CubicSymmetryCert, hyperoctahedral_D3) followed by direct equalities (b3Order_eq_48) computed from rank decompositions and factorial identities.
why it matters in Recognition Science
The module confirms the discrete symmetry order required by T8 (D=3) and T7 (eight-tick octave) in the Recognition framework. It supplies the B3 cardinality used in downstream symmetry arguments, though no explicit used_by edges are recorded here.
scope and limits
- Does not compute group orders for D other than 3.
- Does not address continuous or Lie-group symmetries.
- Does not derive the group presentation, only its order.
- Does not connect the order to mass formulas or the phi-ladder.