`three_colors_forced`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.QuarkColors
domain: Foundation
line: 49 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.QuarkColors on GitHub at line 49.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  46
  47    This matches SU(3) color in QCD. The gauge group rank is forced
  48    by the same dimension argument that gives 3 generations. -/
  49theorem three_colors_forced :
  50    N_colors DimensionForcing.D_physical = 3 := by
  51  unfold N_colors DimensionForcing.D_physical face_pairs
  52  rfl
  53
  54/-! ## Structural Theorems -/
  55
  56/-- N_colors D = D (by definition of face_pairs). -/
  57theorem N_colors_eq_dim (D : ℕ) : N_colors D = D := rfl
  58
  59/-- For D = 3, we cannot have 2 or 4 colors. -/
  60theorem not_two_colors : N_colors 3 ≠ 2 := by norm_num [N_colors, face_pairs]
  61theorem not_four_colors : N_colors 3 ≠ 4 := by norm_num [N_colors, face_pairs]
  62
  63end QuarkColors
  64end Foundation
  65end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.