face_pairs

formal source

  90
  91/-- Face pairs: opposite faces sharing a normal axis. For the D-cube,
  92    the number of 2-face pair axes equals C(D,2). -/
  93def face_pairs (D : ℕ) : ℕ := D * (D - 1) / 2
  94
  95/-- Order of the hyperoctahedral group B_D = Aut(Q_D): signed
  96    permutations of D coordinate axes. |B_D| = 2^D × D!. -/
  97def aut_order (D : ℕ) : ℕ := 2 ^ D * Nat.factorial D
  98
  99/-! ### Q₃-Specific Values (D = 3) -/
 100
 101theorem Q3_vertices : V 3 = 8 := by norm_num [V]
 102theorem Q3_edges : E 3 = 12 := by norm_num [E]
 103theorem Q3_faces : F₂ 3 = 6 := by native_decide
 104theorem Q3_face_pairs : face_pairs 3 = 3 := by native_decide
 105theorem Q3_aut_order : aut_order 3 = 48 := by norm_num [aut_order, Nat.factorial]
 106
 107/-- Euler characteristic of the Q₃ surface: V + F = E + 2 (sphere).
 108    Written as V + F = E + 2 to avoid natural subtraction underflow. -/
 109theorem Q3_euler_characteristic : V 3 + F₂ 3 = E 3 + 2 := by native_decide
 110
 111/-- The Q₃ cube is self-dual: the number of vertices equals the number
 112    of 3-cells (just 1 cube), and vertices = 2^D while the dual has
 113    the same combinatorics. -/
 114theorem Q3_self_dual_vertex_count : V 3 = 2 ^ 3 := by norm_num [V]
 115
 116/-! ## Part 2: Spectral Sectors — Gauge Content from Q₃
 117
 118The automorphism group B₃ = S₃ ⋉ (ℤ/2ℤ)³ acts on ℂ⁸ (the vertex space).
 119This action decomposes into sectors whose dimensions match the Standard
 120Model gauge representations exactly. -/
 121
 122/-- The four spectral sectors of Q₃, corresponding to the layers of
 123    the B₃ = S₃ ⋉ (ℤ/2ℤ)³ decomposition: