Foundation Quark Colors N Colors Eq Dim

The color count identity

In particle physics, quarks carry a property called color charge, which comes in three varieties conventionally labeled red, green, and blue. This three-valued charge is the basis of the strong force theory known as quantum chromodynamics (QCD). The declaration N_colors_eq_dim in the Recognition Science framework's machine-checked library of formal theorems states a simple identity: for any natural number D, the number of color charges N_colors(D) equals D itself. The proof is immediate from the definition, since N_colors is defined as the number of face-pairs of a D-dimensional cube, and a D-cube has exactly D pairs of opposite faces.

The framework's derivation of why quarks come in three colors proceeds in steps. First, a separate theorem forces the number of spatial dimensions to be three. Then, the framework models each independent axis of a three-dimensional cube as carrying one color charge, with each pair of opposite faces corresponding to one color. Substituting D = 3 into the identity gives N_colors(3) = 3, which matches the observed three colors of QCD. The framework also proves that for three dimensions, the color count cannot be 2 or 4, since the identity fixes it exactly at 3.

What the identity does not claim is that quarks must have three colors in any physical theory. It is a statement within the Recognition Science framework, which chooses to model color charges by cube face-pairs. The identity itself is a definitional tautology: it says the number of colors equals the number of dimensions by construction. The physical bridge from spatial dimensions to actual quark color charges is a modeling choice, not a proven fact of nature. The framework's claim is that given its own assumptions, the color count follows from the dimension count, not that nature must obey this particular bookkeeping.

/-- N_colors D = D (by definition of face_pairs). -/
theorem N_colors_eq_dim (D : ℕ) : N_colors D = D := rfl

/-- For D = 3, there are exactly 3 color charges. -/
theorem three_colors_from_D3 : N_colors 3 = 3 := by
  unfold N_colors face_pairs
  rfl

What this page does not claim

The identity does not prove that quarks have three colors in nature, only within the framework's modeling choice. The framework does not claim that color charges are literally cube faces in physical space.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/QuarkColors.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: