pith. sign in
module module high

IndisputableMonolith.Foundation.QuarkColors

show as:
view Lean formalization →

QuarkColors equates the number of color charges to the spatial dimension D by identifying each with a face-pair of the D-cube. Researchers deriving the Standard Model gauge structure from Recognition Science cite this identification. The module supplies the definition N_colors = D together with lemmas that force exactly three colors once D is fixed at 3.

claimThe number of quark color charges equals the spatial dimension: \(N_{\rm colors} = D\).

background

This module belongs to the Foundation section of the Recognition Science formalization. It follows DimensionForcing, whose doc-comment states that spatial dimension D = 3 is forced by the RS framework through four arguments including a topological linking argument. It also follows ParticleGenerations, which formalizes the RS derivation of exactly three generations of fermions.

The central identification is that color charges correspond to the independent axes of the D-cube, with each axis carrying one color in the ledger.

proof idea

This is a definition module. It introduces the equality between color count and dimension via cube face-pairs and contains small lemmas such as three_colors_from_D3 that apply the upstream D=3 result.

why it matters in Recognition Science

The module feeds GaugeFromCube, which derives the Standard Model gauge group SU(3) × SU(2) × U(1) from the automorphism group of the 3-cube Q₃, and WindingCharges, which supplies the topological mechanism for conservation laws. It fills the explicit link from D = 3 to the three colors required for the SU(3) factor in the Recognition Science derivation of the Standard Model.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (6)