RECOGNITION ENCYCLOPEDIA COMPILED 2026-08-06 · PUBLIC EDITION · SOURCES: 1 LEAN MODULE

Foundation Quark Colors

In Recognition Science, the number of quark colors is not a free parameter: it is forced to be three by the derivation of three spatial dimensions.

The color count from dimension

Recognition Science derives the structure of physics from a single ledger of recognition events. The module foundation-quark-colors applies that framework to one of the standard model's unexplained numbers: the three color charges of quantum chromodynamics. The module's starting point is a established result from elsewhere in the framework, that physical space has exactly three dimensions. The module then shows, by a definition and a short proof, that the number of color charges equals the number of spatial dimensions. Since the dimension is three, the color count is three.

The bridge from space to color runs through a cube. The framework treats the spatial dimensions as the axes of a cube, and the ledger identifies opposite faces of that cube. A cube has three pairs of opposite faces, one pair per axis. The module defines the number of colors as the number of such face-pairs, so for dimension D the color count is D. This is a definitional choice: it assigns one color charge to each independent axis of the cube, and the identification with quark color is a modeling step, not a theorem about quantum chromodynamics itself.

What the module proves in Lean is the arithmetic that follows from that definition. For the physical dimension three, the color count is exactly three. The same definition rules out two and four colors for three dimensions. These are simple, fully checked results: they do not depend on any physics axioms, only on the definition of face-pairs and the value of the physical dimension. The theorems three_colors_from_D3 and three_colors_forced both establish N_colors 3 = 3, the latter using the framework's constant for the physical dimension.

The larger claim, that this equals the SU(3) color of quantum chromodynamics, is a correspondence the framework asserts. The module's own documentation states that the gauge group rank is forced by the same dimension argument that gives three generations. What the Lean code itself establishes is narrower: given three spatial dimensions, the defined color count is three. The physical identification with the strong force's color charges is the interpretive step that connects the established arithmetic to the measured world.

MODEL N_colors · N_colors_eq_dim · IndisputableMonolith/Foundation/QuarkColors.lean

THEOREM three_colors_from_D3 · three_colors_forced · IndisputableMonolith/Foundation/QuarkColors.lean

THEOREM not_two_colors · not_four_colors · IndisputableMonolith/Foundation/QuarkColors.lean

What this page does not claim

This answer does not claim that the framework proves the existence of quarks or the SU(3) gauge symmetry of quantum chromodynamics. This answer does not claim that the physical identification between face-pairs and color charges is a established theorem rather than a modeling choice. This answer does not claim that the framework derives the fine-structure constant or any coupling strength.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND