pith. sign in
module module high

IndisputableMonolith.Foundation.QuarkColors

show as:
view Lean formalization →

QuarkColors module establishes that the number of color charges equals the spatial dimension D, with each independent axis of the D-cube carrying one color. Researchers deriving the Standard Model gauge group from cube symmetry cite this to connect three colors directly to D equals three. It imports DimensionForcing to fix D and ParticleGenerations for fermion context. The module defines N_colors and proves equality to D while excluding two or four colors via cube counting.

claim$N_ {colors} = D$, where the number of color charges equals the number of cube face-pairs and each independent axis of the $D$-cube carries one color.

background

This module follows DimensionForcing, which proves spatial dimension D equals three is forced by the RS framework through topological linking and self-similarity arguments. It also references ParticleGenerations, which formalizes the derivation of exactly three fermion generations. The central object is the definition of N_colors as the count of independent axes in the D-cube, matching the doc-comment that each axis carries one color in the ledger.

proof idea

The module is built from a definition of N_colors set equal to D together with short theorems. three_colors_from_D3 substitutes the D equals three result from DimensionForcing. not_two_colors and not_four_colors proceed by contradiction, showing that other counts violate the face-pair enumeration for a D-cube.

why it matters in Recognition Science

This module supplies the color count that feeds GaugeFromCube, which derives the Standard Model gauge group SU(3) times SU(2) times U(1) from the automorphism group of the 3-cube Q3. It also supports WindingCharges by fixing the independent charge count for D equals three. It closes the step from T8 (D equals three) to the three colors required for the quark sector.

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)