`no_fourth_generation`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.ParticleGenerations
domain: Foundation
line: 59 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.ParticleGenerations on GitHub at line 59.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  56/-! ## No Fourth Generation -/
  57
  58/-- For D = 3, there cannot be 4 face-pairs (by definition). -/
  59theorem no_fourth_generation :
  60    face_pairs 3 ≠ 4 := by
  61  norm_num [face_pairs]
  62
  63/-- For D = 3, there cannot be 2 face-pairs. -/
  64theorem not_two_generations :
  65    face_pairs 3 ≠ 2 := by
  66  norm_num [face_pairs]
  67
  68end ParticleGenerations
  69end Foundation
  70end IndisputableMonolith

papers checked against this theorem

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