theorem
proved
term proof
lambda_RS_val
show as:
view Lean formalization →
formal statement (Lean)
106theorem lambda_RS_val : lambda_RS = 1 / 2 := rfl
proof body
Term-mode proof.
107
108/-- The Higgs mass squared from the Mexican hat potential: m_H² = 2λv².
109 With λ = 1/2: m_H² = v². -/