`su2Generators`

definition

show as: view math explainer →

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

used by

formal source

  61/-! ## SU(2) Structure -/
  62
  63/-- Number of SU(2) generators. -/
  64def su2Generators : ℕ := 3
  65
  66/-- W⁺, W⁻, Z⁰ (3 massive weak bosons). -/
  67def weakBosonCount : ℕ := 3
  68
  69/-- SU(2) generators correspond to 3D rotations. -/
  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

papers checked against this theorem

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