aut_order
plain-language theorem explainer
The definition computes the order of the automorphism group of the D-dimensional hypercube as 2^D times D factorial. Recognition Science researchers cite it to count total fermionic states once D is fixed at 3. It supplies the concrete value 48 that matches the chiral fermion multiplicity in the Standard Model. The implementation is a single closed arithmetic expression with no further reduction steps.
Claim. The order of the hyperoctahedral group $B_D$ is given by $|B_D| = 2^D D!$.
background
The Spectral Emergence module starts from the forced datum D = 3 supplied by the upstream chain (T8). The binary cube Q_D has 2^D vertices and its automorphism group is identified with the hyperoctahedral group B_D of signed coordinate permutations. The definition aut_order encodes the standard counting formula for that group order. Module documentation states that this order equals the number of chiral fermionic states once D = 3 is substituted.
proof idea
The declaration is a direct definition that writes the closed-form expression 2^D * Nat.factorial D. No lemmas or tactics are invoked; the formula is the standard order of the hyperoctahedral group B_D.
why it matters
This definition supplies the numerical anchor for all downstream fermion-counting results. It is invoked by fermions_eq_half_aut, fermion_states_eq_aut, numerological_summary, and SpectralEmergenceCert, each of which equates aut_order 3 to 48 and identifies that number with the total chiral fermion states. The module documentation presents the identity |Aut(Q_3)| = 48 as the central numerical coincidence linking the cube symmetry group to the Standard Model fermion content. It realizes the counting step that follows T8 (D = 3) and the eight-tick octave in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.