def
definition
weakRange_fm
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.WeakForceEmergence on GitHub at line 59.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
56def hbar_c_GeV_fm : ℝ := 0.197327
57
58/-- Weak interaction range (fm). -/
59def weakRange_fm : ℝ := hbar_c_GeV_fm / wBosonMass_GeV
60
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⁻). -/