rightHandedCouples

formal source

  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
 109/-- G_F relation: G_F / (ℏc)³ = √2 g² / (8 m_W²). -/
 110def gf_from_mw : ℝ := sqrt 2 * (weak_coupling_g)^2 / (8 * wBosonMass_GeV^2)
 111