three_colors_from_D3
plain-language theorem explainer
For three spatial dimensions the number of color charges equals three. Researchers deriving the SU(3) structure of QCD from Recognition Science would cite this result to link the dimension-forcing argument to the observed quark color multiplicity. The proof is a one-line wrapper that unfolds N_colors to the face-pair count and reduces by reflexivity.
Claim. In three spatial dimensions the number of color charges equals three: $N_c(3)=3$.
background
N_colors(D) is defined as the number of cube face-pairs for dimension D; each pair of opposite faces supplies one independent color charge in the ledger. The module sets this inside the P-007 derivation: DimensionForcing supplies D=3 from the eight-tick octave and spinor structure, after which the D-cube combinatorics directly yields three colors. This ledger identification is the same mechanism used for particle generations, so the color count inherits the same D dependence.
proof idea
The tactic proof unfolds N_colors to face_pairs and then applies reflexivity, reducing the goal to the definitional equality face_pairs 3 = 3.
why it matters
The declaration discharges the P-007 registry item, showing that the same dimension-forcing step (T8) that fixes D=3 also fixes the gauge-group rank of QCD at three. It therefore supplies the color multiplicity that matches the three-generation structure already obtained from the same ledger face-pair counting. No downstream theorems are recorded yet, leaving the result as a direct bridge between the forcing chain and the standard-model gauge content.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.