aut_order
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not enumerate group elements or prove the isomorphism to signed permutations.
- Does not extend the formula to non-integer D.
- Does not incorporate J-cost, phi-ladder, or defectDist.
- Does not address gauge-group dimensions or consciousness ground state.
Lean usage
theorem Q3_aut_order : aut_order 3 = 48 := by norm_num [aut_order, Nat.factorial]formal statement (Lean)
97def aut_order (D : ℕ) : ℕ := 2 ^ D * Nat.factorial D
proof body
Definition body.
98
99/-! ### Q₃-Specific Values (D = 3) -/
100