`totalCarriers`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.StandardModelGroupStructure
domain: Physics
line: 45 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.StandardModelGroupStructure on GitHub at line 45.

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

  42theorem w_boson_count : wBosonCount = 3 := by decide
  43
  44/-- Total force carriers: 8 + 3 + 1 = 12 (before EWSB). -/
  45def totalCarriers : ℕ := gluonCount + wBosonCount + rankU1
  46theorem total_carriers_eq : totalCarriers = 12 := by decide
  47
  48structure SMGroupCert where
  49  five_types : Fintype.card SMGaugeBosonType = 5
  50  rank_decomp : rankSU3 + rankSU2 + rankU1 = 6
  51  gluon_8 : gluonCount = 8
  52  total_12 : totalCarriers = 12
  53
  54def smGroupCert : SMGroupCert where
  55  five_types := smGaugeBosonCount
  56  rank_decomp := totalRank
  57  gluon_8 := gluon_count
  58  total_12 := total_carriers_eq
  59
  60end IndisputableMonolith.Physics.StandardModelGroupStructure

papers checked against this theorem

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