not_two_colors
plain-language theorem explainer
The result establishes that the number of color charges cannot be two when spatial dimension equals three. Researchers deriving the SU(3) color structure from the Recognition Science ledger would cite it to exclude N_c=2. The proof reduces immediately to numerical evaluation of the face-pair count.
Claim. $N_c(3) = 3$ and therefore $N_c(3) ≠ 2$, where $N_c(D)$ is the number of color charges defined as the count of opposite face pairs on a D-dimensional cube.
background
The module derives N_c=3 from D=3 spatial dimensions obtained via DimensionForcing. The ledger treats the three pairs of opposite faces on a cube as three independent charge directions, with each spatial axis carrying one color charge. N_colors(D) is defined to equal face_pairs(D), and the upstream face_pairs from ParticleGenerations sets face_pairs(D) := D, so that exactly three colors appear for D=3.
proof idea
The proof is a one-line wrapper that applies norm_num to the definitions of N_colors and face_pairs. These evaluate directly to 3 when the argument is 3, rendering the inequality 3 ≠ 2 immediate.
why it matters
The declaration fills the exclusion step in P-007 for quark colors by ruling out N_c=2 (and symmetrically N_c=4) once D=3 is fixed by the forcing chain. It anchors the color count to the same face-pair combinatorics used for particle generations and the eight-tick octave. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.