Encyclopedia Foundation Foundation Quark Colors Three Colors From D3
ARTICLE 3 claims 3 theorems
Foundation Quark Colors Three Colors From D3
A machine-checked proof derives the number of quark colors from the number of spatial dimensions, and it is a definitional identity, not a physical measurement.
Three colors from three dimensions
In particle physics, quarks carry a property called color charge, the source of the strong force. Color charge comes in three varieties, conventionally labeled red, green, and blue; the number three is an experimental fact, confirmed by decades of scattering experiments and by the rate of pion decay. The standard theory, quantum chromodynamics, simply postulates this number as the dimension of its symmetry group, SU(3).
The framework called Recognition Science attempts to derive such numbers from deeper structure. Its central idea is a ledger, a discrete record of recognition events, and a forced cost function that shapes how those events combine. From that cost function, the framework claims to derive, among other things, that physical space has three dimensions. The declaration three_colors_from_D3 then connects that spatial claim to the color count.
In Recognition Science, the derivation works by identifying each spatial axis with one independent color charge. The framework models the ledger as a three-dimensional cube; a cube has three pairs of opposite faces, and each face-pair is assigned one color. The declaration defines the number of colors as a function of dimension, N_colors(D) = D, and then proves, by unfolding definitions, that for D = 3 the count is exactly 3. It also proves that the count cannot be 2 or 4. The proof is a trivial identity: the definition of face-pairs makes the count equal to the dimension by construction.
The declaration does not measure the color count, nor does it prove that the physical strong force has three colors. It proves a conditional statement: if the framework's identification of colors with face-pairs is accepted, and if the framework's derivation of three spatial dimensions is accepted, then the color count is three. The physical bridge, from the abstract ledger to the actual quark field, is not part of this theorem. The declaration also relies on the legacy DimensionForcing result for D = 3, which the framework itself flags as needing a separate, still-open physical justification.
What the declaration does establish, within the framework, is a clean structural link: the number of colors is forced to equal the number of spatial dimensions. That link is a theorem in the machine-checked library of formal theorems, meaning the logical derivation from the definitions is verified. The remaining question, whether the ledger's face-pairs really correspond to the strong force's color charge, is a physical identification that the theorem does not address.
THEOREM three_colors_from_D3 · IndisputableMonolith/Foundation/QuarkColors.lean
/-- 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
THEOREM not_two_colors · not_four_colors · IndisputableMonolith/Foundation/QuarkColors.lean
/-- For D = 3, we cannot have 2 or 4 colors. -/
theorem not_two_colors : N_colors 3 ≠ 2 := by norm_num [N_colors, face_pairs]
theorem not_four_colors : N_colors 3 ≠ 4 := by norm_num [N_colors, face_pairs]
THEOREM N_colors_eq_dim · IndisputableMonolith/Foundation/QuarkColors.lean
/-- N_colors D = D (by definition of face_pairs). -/
theorem N_colors_eq_dim (D : ℕ) : N_colors D = D := rfl
What this page does not claim
The declaration does not measure the physical color count; it only derives a conditional identity from definitions. The declaration does not prove the physical bridge from the ledger to quantum chromodynamics; that bridge remains open. The declaration does not derive the SU(3) gauge group structure, only the number of colors as equal to the dimension.
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:
- How does the framework derive the number of spatial dimensions as three?
- What physical evidence connects the ledger's face-pairs to the strong force's color charge?
- Does the framework derive the SU(3) gauge group structure, or only the count of colors?
- What would falsify the identification of colors with face-pairs?
- How does the framework's derivation of three generations relate to the color derivation?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM three_colors_from_D3 · IndisputableMonolith/Foundation/QuarkColors.lean
/-- For D = 3, there are exactly 3 color charges. -/ theorem three_colors_from_D3 : N_colors 3 = 3 := by unfold N_colors face_pairs rflThe declaration defines the number of colors as a function of dimension, N_colors(D) = D, and then proves, by unfolding definitions, that for D = 3 the count is exactly 3. three_colors_from_D3 · IndisputableMonolith/Foundation/QuarkColors.leanTHEOREM not_two_colors · not_four_colors · IndisputableMonolith/Foundation/QuarkColors.lean
/-- For D = 3, we cannot have 2 or 4 colors. -/ theorem not_two_colors : N_colors 3 ≠ 2 := by norm_num [N_colors, face_pairs]theorem not_four_colors : N_colors 3 ≠ 4 := by norm_num [N_colors, face_pairs]It also proves that the count cannot be 2 or 4. not_two_colors · not_four_colors · IndisputableMonolith/Foundation/QuarkColors.leanTHEOREM N_colors_eq_dim · IndisputableMonolith/Foundation/QuarkColors.lean
/-- N_colors D = D (by definition of face_pairs). -/ theorem N_colors_eq_dim (D : ℕ) : N_colors D = D := rflThe proof is a trivial identity: the definition of face-pairs makes the count equal to the dimension by construction. N_colors_eq_dim · IndisputableMonolith/Foundation/QuarkColors.lean