sector_dim_sum

formal source

 162
 163/-- **THEOREM**: Sector dimensions sum to 8 = |V(Q₃)|.
 164    The spectral decomposition accounts for every vertex. -/
 165theorem sector_dim_sum :
 166    SpectralSector.dim .color +
 167    SpectralSector.dim .weak +
 168    SpectralSector.dim .hypercharge +
 169    SpectralSector.dim .conjugate = V 3 := by
 170  norm_num [SpectralSector.dim, V]
 171
 172/-- **THEOREM**: The gauge sector dimensions (excluding conjugate) sum to 6.
 173    This is the dimension of the "physical" representation. -/
 174theorem gauge_sector_dim :
 175    SpectralSector.dim .color +
 176    SpectralSector.dim .weak +
 177    SpectralSector.dim .hypercharge = 6 := by
 178  norm_num [SpectralSector.dim]
 179
 180/-- **THEOREM**: The residual dimension (conjugate sector) is forced:
 181    8 - 6 = 2 = dim(conjugate). -/
 182theorem conjugate_dim_forced :
 183    V 3 - (SpectralSector.dim .color +
 184            SpectralSector.dim .weak +
 185            SpectralSector.dim .hypercharge) =
 186    SpectralSector.dim .conjugate := by
 187  norm_num [V, SpectralSector.dim]
 188
 189/-- **THEOREM**: Total gauge generators: 8 + 3 + 1 = 12 = |E(Q₃)|.
 190    The gauge degrees of freedom equal the edge count of Q₃. -/
 191theorem gauge_generators_eq_edges :
 192    SpectralSector.gauge_rank .color +
 193    SpectralSector.gauge_rank .weak +
 194    SpectralSector.gauge_rank .hypercharge = E 3 := by
 195  norm_num [SpectralSector.gauge_rank, E]