pith. machine review for the scientific record. sign in
def definition def or abbrev

gf_from_mw

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 110def gf_from_mw : ℝ := sqrt 2 * (weak_coupling_g)^2 / (8 * wBosonMass_GeV^2)

proof body

Definition body.

 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. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (8)

Lean names referenced from this declaration's body.