`weak_bosons_eq_generators`

proved

show as: view math explainer →

module: IndisputableMonolith.Physics.WeakForceEmergence
domain: Physics
line: 73 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.WeakForceEmergence on GitHub at line 73.

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

  70theorem su2_from_3d : su2Generators = 3 := rfl
  71
  72/-- Weak bosons = SU(2) generators. -/
  73theorem weak_bosons_eq_generators : weakBosonCount = su2Generators := rfl
  74
  75/-! ## Chirality -/
  76
  77/-- Left-handed chirality couples to weak force. -/
  78def leftHandedCouples : Bool := true
  79
  80/-- Right-handed chirality does NOT couple to SU(2)_L. -/
  81def rightHandedCouples : Bool := false
  82
  83/-- Parity violation: L ≠ R. -/
  84theorem parity_violation : leftHandedCouples ≠ rightHandedCouples := by
  85  decide
  86
  87/-! ## Weak Isospin Doublets -/
  88
  89/-- Lepton doublet: (νe, e⁻). -/
  90def leptonDoublet : ℕ := 2
  91
  92/-- Quark doublet: (u, d). -/
  93def quarkDoublet : ℕ := 2
  94
  95/-- Each generation has 2 isospin doublets. -/
  96def doubletsPerGeneration : ℕ := 2
  97
  98/-- Total doublets for 3 generations. -/
  99def totalDoublets : ℕ := 3 * doubletsPerGeneration
 100
 101/-! ## Range and Strength -/
 102
 103/-- Weak interaction range is ~10⁻³ fm. -/

papers checked against this theorem

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