Weinberg triangle: $\cos\theta_W = g/\sqrt{g^2+g'^2}$

Proved

ElectroweakWiki.weinberg_triangle

by Lucas · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

electroweakmathematical-physics

Let $g>0$ and $g'>0$ be the weak isospin and weak hypercharge couplings, and let $\theta_W = \arctan(g'/g)$ be the weak mixing angle. Then

\cos\theta_W = \frac{g}{\sqrt{g^2+g'^2}},\qquad \sin\theta_W = \frac{g'}{\sqrt{g^2+g'^2}}.

This is the right triangle with legs $g$ , $g'$ and hypotenuse $\sqrt{g^2+g'^2}$ drawn in the article's figure, and it is used by every later statement that involves $\theta_W$ .

Preamble

import Definitions.Def_ElectroweakWiki_defs
open Matrix

Formal statement

namespace ElectroweakWiki

theorem weinberg_triangle (g g' : ℝ) (hg : 0 < g) (hg' : 0 < g') :
    Real.cos (weinbergAngle g g') = g / Real.sqrt (g ^ 2 + g' ^ 2) ∧
      Real.sin (weinbergAngle g g') = g' / Real.sqrt (g ^ 2 + g' ^ 2) := by sorry

end ElectroweakWiki

Source

Wikipedia, "Electroweak interaction", revision oldid=1360331872, https://en.wikipedia.org/w/index.php?title=Electroweak_interaction&oldid=1360331872; Section Formulation, figure 'Weinberg's weak mixing angle θW, and relation between coupling constants g, g′, and e' (p. 2 of the PDF)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted these Lean statements (at the explicit direction of the proposal's owner), not by an independent blind auditor. The author knew the intended meaning while writing it, so it must not be mistaken for independent testimony; reviewers should check it against the Lean code themselves.

For all real numbers $g, g'$ with $g>0$ and $g'>0$ , let $\theta = \arctan(g'/g)$ . The statement asserts both

\cos\theta = \frac{g}{\sqrt{g^2+g'^2}} \quad\text{and}\quad \sin\theta = \frac{g'}{\sqrt{g^2+g'^2}},

with $\sqrt{\cdot}$ the real square root. Under the hypotheses the denominators are positive.

View graph

Weinberg triangle: cos⁡θW=g/g2+g′2\cos\theta_W = g/\sqrt{g^2+g'^2}cosθW​=g/g2+g′2​

Weinberg triangle: $\cos\theta_W = g/\sqrt{g^2+g'^2}$