Q3_faces

formal source

 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:
 124
 125    - **Color**: from S₃ (permutations of 3 axes) → SU(3), dim 3
 126    - **Weak**: from (ℤ/2ℤ)² (reflections in 2 axes) → SU(2), dim 2
 127    - **Hypercharge**: from ℤ/2ℤ (parity of single axis) → U(1), dim 1
 128    - **Conjugate**: the residual 2-dimensional sector, dim 2
 129
 130    The total: 3 + 2 + 1 + 2 = 8 = |V(Q₃)| = 2^D. -/
 131inductive SpectralSector where
 132  | color : SpectralSector
 133  | weak : SpectralSector