pith. machine review for the scientific record. sign in
def definition def or abbrev high

N_colors

show as:
view Lean formalization →

N_colors sets the color charge count to the number of opposite face pairs on the D-cube. Gauge theorists tracing SM structure to cube geometry cite this for the N_c = 3 result at D = 3. The implementation is a direct alias to face_pairs.

claimThe number of color charges equals the number of opposite face pairs on a $D$-dimensional cube, hence $N_c(D) = D$.

background

Recognition Science forces D = 3 spatial dimensions via the unified forcing chain. The face_pairs combinator counts the D pairs of opposite faces on the D-cube; each axis corresponds to one color charge in the ledger. Module P-007 uses this to derive three colors from the same geometry that yields three generations.

proof idea

One-line definition delegating directly to face_pairs D.

why it matters in Recognition Science

This supplies N_colors 3 = 3 for the gauge_group_certificate theorem, which extracts SU(3) from the S3 factor of the 3-cube automorphism group. It completes the color sector of the gauge-generation unification. The framework landmark is the identification of color with axis permutations in D = 3.

scope and limits

formal statement (Lean)

  32def N_colors (D : ℕ) : ℕ := face_pairs D

proof body

Definition body.

  33
  34/-- For D = 3, there are exactly 3 color charges. -/

used by (9)

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.