pith. machine review for the scientific record. sign in
theorem proved term proof

higgsMassSq_simplifies

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)

 112theorem higgsMassSq_simplifies (v : ℝ) :
 113    higgsMassSq_over_vev v = v^2 := by

proof body

Term-mode proof.

 114  unfold higgsMassSq_over_vev lambda_RS; ring
 115
 116/-- The W-boson mass squared: m_W² = g²v²/4 where g is the SU(2) coupling.
 117    In RS: g² = 4 sin²θ_W · (mZ/v)² where sin²θ_W = (3-φ)/6 (proved elsewhere). -/

depends on (10)

Lean names referenced from this declaration's body.