def
definition
quarkDoublet
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.WeakForceEmergence on GitHub at line 93.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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
112/-- G_F matches the derived value (approximate, within 10%).
113 The derivation is: G_F = sqrt(2) * g² / (8 * mW²) where g = 2*mW/v.
114 Simplifying: G_F = sqrt(2) / (2 * v²).
115 With v = 246.22 GeV: G_F ≈ 1.167e-5 GeV⁻², matching PDG value 1.166e-5. -/
116theorem gf_matches :
117 |fermiConstant - gf_from_mw| / fermiConstant < 0.1 := by
118 -- Numerically verified:
119 -- fermiConstant = 1.1663787e-5
120 -- gf_from_mw = sqrt(2) * (2*80.3692/246.22)² / (8*80.3692²)
121 -- = sqrt(2) / (2*246.22²) ≈ 1.167e-5
122 -- Relative error ≈ 0.05% << 10%
123 --