Pith. sign in
module module high

IndisputableMonolith.Foundation.QuarkColors

show as:
view Lean formalization →

Equates the number of QCD color charges to the spatial dimension D of the recognition cube: each independent axis (face-pair) carries one color. With D forced to 3, exactly three colors follow, and two- or four-color alternatives are excluded. Gauge-from-cube and winding-charge modules cite this identification. The argument is definitional equality N_colors = D plus the upstream dimension-forcing chain.

claimThe number of color charges equals the number of independent face-pairs of the $D$-cube, so $N_{\mathrm{colors}}=D$. When $D=3$, there are exactly three colors; the alternatives $N_{\mathrm{colors}}=2$ and $N_{\mathrm{colors}}=4$ are ruled out.

background

Recognition Science forces spatial dimension $D=3$ (T8 in the forcing chain) from the structure of the recognition cube and the eight-tick octave. DimensionForcing collects the topological and ledger arguments that pin $D=3$; ParticleGenerations separately forces three fermion generations (P-001).

This module treats color as a ledger label on the cube: each independent axis of the $D$-cube is one color charge, so the count of colors is the count of face-pairs, equal to $D$. The DOC_COMMENT states the identification directly: number of color charges = number of cube face-pairs = $D$.

Sibling declarations package that claim as $N_{\mathrm{colors}}$, the equality $N_{\mathrm{colors}}=D$, the specialization to three colors when $D=3$, and the exclusions of two and four colors.

proof idea

Definitional core: $N_{\mathrm{colors}}$ is set equal to the cube dimension (face-pair count). The equality $N_{\mathrm{colors}}=D$ is then immediate. Three colors follow by substituting the forced value $D=3$ from DimensionForcing. The forced-three statement composes that substitution with the upstream forcing. Separate lemmas discharge the two-color and four-color cases by contradicting $D=3$. No independent analytic machinery beyond the dimension identification and the imported forcing results.

why it matters in Recognition Science

Supplies the color count that GaugeFromCube needs to extract $\mathrm{SU}(3)$ from the automorphism group of the 3-cube $Q_3$ (P-014: Standard Model gauge group from cube symmetry). WindingCharges uses the same $D=3$ color count when it replaces the ad-hoc clause independent_charge_count $D:=$ if $D=3$ then 3 else 0 with a topological winding mechanism (F-013).

In the RS chain this closes the color side of the T8 $D=3$ landmark: three spatial axes, three colors, three generations (the last from ParticleGenerations). Without the $N_{\mathrm{colors}}=D$ link, the cube-to-$\mathrm{SU}(3)$ step would be an external input rather than a forced count.

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)