`leftHandedCouples`

definition

show as: view math explainer →

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

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

used by

parity_violation IndisputableMonolith.Physics.WeakForceEmergence

formal source

  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. -/
 104theorem weak_range_short : weakRange_fm < 0.01 := by
 105  -- 0.197327 / 80.3692 ≈ 0.00245 fm < 0.01
 106  simp only [weakRange_fm, hbar_c_GeV_fm, wBosonMass_GeV]
 107  norm_num
 108

papers checked against this theorem

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