not_four_colors
plain-language theorem explainer
The theorem shows that the number of quark color charges in three spatial dimensions cannot equal four. Researchers deriving the standard model from recognition science would cite this to confirm that N_c equals three from the dimension-forcing step. The proof is a one-line numerical normalization that unfolds N_colors and face_pairs to evaluate the inequality directly.
Claim. For three spatial dimensions the number of color charges, equal to the number of opposite face pairs on the three-dimensional cube, is not equal to four.
background
Recognition Science derives the number of color charges from the spatial dimension D forced to equal three. The function N_colors(D) counts the color charges and equals the number of opposite face pairs on a D-cube. In three dimensions this yields exactly three colors, matching the SU(3) structure of QCD. The cube-face identification assigns one color charge to each independent spatial axis. This ledger combinatorics is shared with the generation structure, where D face-pairs determine both. Upstream, face_pairs(D) is defined as D in the ParticleGenerations module, providing the direct count of axis pairs.
proof idea
The proof is a one-line term that invokes norm_num on the definitions of N_colors and face_pairs. This reduces N_colors 3 to face_pairs 3, which equals 3, and confirms the inequality with 4 by direct computation.
why it matters
This result completes the local derivation of N_c = 3 in the QuarkColors module, which formalizes proposition P-007. It sits downstream of the dimension-forcing chain that sets D = 3 and upstream of any further particle spectrum calculations. The framework landmark is the identification of color charges with the three spatial axes via the cube ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.