`three_generations_from_dimension`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.ParticleGenerations
domain: Foundation
line: 51 · 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 51.

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

formal source

  48
  49    This is not a coincidence — it is forced by the same dimension
  50    argument that gives linking and spinors. -/
  51theorem three_generations_from_dimension :
  52    face_pairs Foundation.DimensionForcing.D_physical = 3 := by
  53  unfold face_pairs Foundation.DimensionForcing.D_physical
  54  rfl
  55
  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.