`not_two_generations`

proved

show as: view math explainer →

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

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

face_pairs IndisputableMonolith.Foundation.ParticleGenerations
face_pairs IndisputableMonolith.Foundation.SpectralEmergence

formal source

  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.