conjugate_dim_forced
plain-language theorem explainer
The declaration shows that the conjugate spectral sector of Q3 has dimension exactly 2, recovered by subtracting the gauge-sector dimensions 3 + 2 + 1 from the vertex count V(3) = 8. Model builders who reconstruct the Standard Model gauge algebra from the binary cube would cite this identity as the closing step of the dimension ledger. The proof is a one-line numerical reduction that unfolds the definitions of V and SpectralSector.dim.
Claim. $V(3) - (3 + 2 + 1) = 2$, where $V(D) = 2^D$ counts vertices of the $D$-cube and the subtracted integers are the dimensions of the color, weak, and hypercharge sectors of $Q_3$.
background
The module derives Standard Model structure from the 3-cube Q3 forced by T8. V(D) is defined as the vertex count 2^D. SpectralSector is the inductive partition of B3 symmetries into color (S3 action, dimension 3), weak (Z/2Z^2 reflections, dimension 2), hypercharge (single-axis parity, dimension 1), and conjugate (residual, dimension 2). The module doc states that these four sectors together account for the full 8 vertices while reproducing the gauge content 3 + 2 + 1 = 6.
proof idea
The proof is a one-line wrapper that applies norm_num to the definitions of V and SpectralSector.dim, reducing 8 - (3 + 2 + 1) directly to 2.
why it matters
This identity completes the gauge-sector accounting inside SpectralEmergence, confirming that the residual conjugate dimension is forced to 2 once the SU(3) × SU(2) × U(1) dimensions are assigned. It directly supports the module claim that Q3 forces the observed gauge content and the 48-element automorphism group. In the Recognition framework it follows from T8 (D = 3) and the B3 decomposition of Aut(Q3) listed in the module doc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.